Output details
11 - Computer Science and Informatics
Queen Mary University of London
Scalable shape analysis for systems code
<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.