Constraint-based program reasoning with heaps and separation
Duck, G.J. Jaffar, J. Koh, N.C.H.
Duck, G.J.
Koh, N.C.H.
Citations
Altmetric:
Alternative Title
Abstract
This paper introduces a constraint language H for finite partial maps (a.k.a. heaps) that incorporates the notion of separation from Separation Logic. We use H to build an extension of Hoare Logic for reasoning over heap manipulating programs using (constraint-based) symbolic execution. We present a sound and complete algorithm for solving quantifier-free (QF) H-formulae based on heap element propagation. An implementation of the H-solver has been integrated into a Satisfiability Modulo Theories (SMT) framework. We experimentally evaluate the implementation against Verification Conditions (VCs) generated from symbolic execution of large (heap manipulating) programs. In particular, we mitigate the path explosion problem using subsumption via interpolation - made possible by the constraint-based encoding. © 2013 Springer-Verlag.
Keywords
Constraint Handling Rules, Heap Manipulating Programs, Satisfiability Modulo Theories, Separation Logic, Symbolic Execution
Source Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher
Series/Report No.
Collections
Rights
Date
2013
DOI
10.1007/978-3-642-40627-0_24
Type
Conference Paper