A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
DOI10.1007/978-3-319-40229-1_36zbMath1475.68185OpenAlexW2341060778MaRDI QIDQ2817951
Zhilin Wu, Xincai Gu, Taolue Chen
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-40229-1_36
Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (6)
Uses Software
Cites Work
- Unnamed Item
- On the almighty wand
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Quantitative separation logic and programs with lists
- Compositional Entailment Checking for a Fragment of Separation Logic
- Tractable Reasoning in a Fragment of Separation Logic
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives
- Deciding Entailments in Inductive Separation Logic with Tree Automata
- On Automated Lemma Generation for Separation Logic with Inductive Definitions
- A decision procedure for satisfiability in separation logic with inductive predicates
- Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data
- The Tree Width of Separation Logic with Recursive Definitions
- Automated Cyclic Entailment Proofs in Separation Logic
- Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
- Foundations for Decision Problems in Separation Logic with General Inductive Predicates
- Programming Languages and Systems
- Fast LCF-Style Proof Reconstruction for Z3
This page was built for publication: A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
