Separation logic is a widely adopted formalism to verify programs manipulating dynamic data structures. Entailment checking of separation logic constitutes a crucial step for the verification of such programs. In general this problem is undecidable, hence only incomplete decision procedures are provided in most state-of-the-art tools. In this paper, we define a linearly compositional fragment of separation logic with inductive definitions, where traditional shape properties for linear data structures, as well as data constraints, e.g., the sortedness property and size constraints, can be specified in a unified framework. We provide complete decision procedures for both the satisfiability and the entailment problem, which are in NP and ΠP3 respectively.
CITATION STYLE
Gu, X., Chen, T., & Wu, Z. (2016). A complete decision procedure for linearly compositional separation logic with data constraints. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9706, pp. 532–549). Springer Verlag. https://doi.org/10.1007/978-3-319-40229-1_36
Mendeley helps you to discover research relevant for your work.