Model and proof generation for heap-manipulating prrograms

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

[img] 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
Q Science > QA Mathematics > QA0076 Computer software
Depositing User: Peter Schrammel
Date Deposited: 09 May 2016 10:09
Last Modified: 09 May 2016 10:09
URI: http://sro.sussex.ac.uk/id/eprint/59923

View download statistics for this item

📧 Request an update