You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: Queen Mary University of London » Outputs » Detail

Output details

11 - Computer Science and Informatics

Queen Mary University of London

Return to search Previous output Next output

Output 59 of 83 in the submission

Output title

Scalable shape analysis for systems code

Type

E - Conference contribution

DOI

10.1007/978-3-540-70545-1_36

Name of conference/published proceedings

Computer Aided Verification, 20th International Conference, CAV

Volume number

5123

Issue number

First page of article

385

ISSN of proceedings

Year of publication

2008

URL

http://link.springer.com/chapter/10.1007/978-3-540-70545-1_36

Number of additional authors

Additional information

<11>The accurate treatment of mutable data is an outstanding problem in automatic program verification, with scalability hampered by potential bugs-at-a-distance resulting from pointer aliasing. This paper achieved a milestone: the first automatic proofs of pointer integrity - including absence of null dereferences, double-frees and memory leaks - in entire industrial systems programs (Linux and Windows device drivers with up to 10k lines of code). This work had direct influence in several other projects including Microsoft SLAyer and Monoidics INFER. According to Microsoft Academic Search, this is the most cited paper in this 2008 conference. Space Invader has been released open source.

Interdisciplinary

Cross-referral requested

Research group

None

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract