Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-40627-0_24
Title: Constraint-based program reasoning with heaps and separation
Authors: Duck, G.J.
Jaffar, J. 
Koh, N.C.H.
Keywords: Constraint Handling Rules
Heap Manipulating Programs
Satisfiability Modulo Theories
Separation Logic
Symbolic Execution
Issue Date: 2013
Source: Duck, G.J.,Jaffar, J.,Koh, N.C.H. (2013). Constraint-based program reasoning with heaps and separation. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8124 LNCS : 282-298. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-40627-0_24
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.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/78067
ISBN: 9783642406263
ISSN: 03029743
DOI: 10.1007/978-3-642-40627-0_24
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

5
checked on Feb 20, 2018

Page view(s)

22
checked on Feb 23, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.