Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
7-2017
Abstract
We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.
Keywords
Decidability, Inductive predicates, Satisfiability solving, Separation logic
Discipline
Software Engineering | Theory and Algorithms
Research Areas
Software and Cyber-Physical Systems
Publication
Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28: Proceedings
Volume
10427
First Page
497
Last Page
517
ISBN
9783319633893
Identifier
10.1007/978-3-319-63390-9_26
Publisher
Springer
City or Country
Cham
Citation
LE, Quang Loc; TATSUTA, Makoto; SUN, Jun; and CHIN, Wei-Ngan.
A decidable fragment in separation logic with inductive predicates and arithmetic. (2017). Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28: Proceedings. 10427, 497-517.
Available at: https://ink.library.smu.edu.sg/sis_research/4702
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-63390-9_26