Separation logic has become a stock formalism for reasoning about programs with dynamic memory allocation. We introduce a variant of separation logic that supports lists and trees as well as inductive constraints on the data stored in these structures. We prove that this logic has the small model property, meaning that for each satisfiable formula there is a small domain in which the formula is satisfiable. As a consequence, the satisfiability and entailment problems for our fragment are in NP and coNP, respectively. Leveraging this result, we describe a polynomial SMT encoding that allows us to decide satisfiability and entailment for our separation logic.
CITATION STYLE
Katelaan, J., Jovanović, D., & Weissenbacher, G. (2018). A Separation Logic with Data: Small Models and Automation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 455–471). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_30
Mendeley helps you to discover research relevant for your work.