Brain, Martin, David, Cristina, Kroening, Daniel and Schrammel, Peter (2014) Model and proof generation for heap-manipulating prrograms. In: Shao, Zhong (ed.) Programming Languages and Systems. Lecture Notes in Computer Science, 8410 . Springer, pp. 432-452. ISBN 9783642548321

PDF - Submitted Version Restricted to SRO admin only Download (404kB)

Abstract

Existing heap analysis techniques lack the ability to supply counterexamples in case of property violations. This hinders diagnosis, prevents test-case generation and is a barrier to the use of these tools among non-experts. We present a verification technique for reasoning about aliasing and reachability in the heap which uses ACDCL (a combination of the well-known CDCL SAT algorithm and abstract interpretation) to perform interleaved proof generation and model construction. Abstraction provides us with a tractable way of reasoning about heaps; ACDCL adds the ability to search for a model in an efficient way. We present a prototype tool and demonstrate a number of examples for which we are able to obtain useful concrete counterexamples.

Item Type:	Book Section
Keywords:	software verification, heap analysis, separation logic, conflict driven clause learning
Schools and Departments:	School of Engineering and Informatics > Informatics
Subjects:	Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User:	Peter Schrammel
Date Deposited:	09 May 2016 10:09
Last Modified:	09 May 2016 10:09
URI:	http://srodev.sussex.ac.uk/id/eprint/59923

View download statistics for this item

📧 Request an update