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. © 2014 Springer-Verlag.
CITATION STYLE
Brain, M., David, C., Kroening, D., & Schrammel, P. (2014). Model and proof generation for heap-manipulating programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8410 LNCS, pp. 432–452). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_23
Mendeley helps you to discover research relevant for your work.