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