Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2016
Abstract
In this work, we present a semi-decision procedure for a fragment of separation logic with user-defined predicates and Presburger arithmetic. To check the satisfiability of a formula, our procedure iteratively unfolds the formula and examines the derived disjuncts. In each iteration, it searches for a proof of either satisfiability or unsatisfiability. Our procedure is further enhanced with automatically inferred invariants as well as detection of cyclic proof. We also identify a syntactically restricted fragment of the logic for which our procedure is terminating and thus complete. This decidable fragment is relatively expressive as it can capture a range of sophisticated data structures with non-trivial pure properties, such as size, sortedness and near-balanced. We have implemented the proposed solver and a new system for verifying heap-based programs. We have evaluated our system on benchmark programs from a software verification competition.
Keywords
Decision procedures, Satisfiability, Separation logic, Inductive predicates, Cyclic proofs
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 28th International Conference, CAV 2016, Toronto, Canada, July 17–23
Volume
9779
First Page
382
Last Page
404
ISBN
9783319415277
Identifier
10.1007/978-3-319-41528-4_21
Publisher
Springer Link
City or Country
Toronto, Canada
Citation
LE, Quang Loc; SUN, Jun; and CHIN, Wei-Ngan.
Satisfiability modulo heap-based programs. (2016). Proceedings of the 28th International Conference, CAV 2016, Toronto, Canada, July 17–23. 9779, 382-404.
Available at: https://ink.library.smu.edu.sg/sis_research/4937
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-319-41528-4_21