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

Mathematics Subject Classification ID

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)

Compositional entailment checking for a fragment of separation logic ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Strong-separation logic ⋮ Compositional satisfiability solving in separation logic ⋮ Unnamed Item ⋮ Reasoning about block-based cloud storage systems via separation logic

Uses Software

• HIP
• Infer
• GRASShopper
• Slide

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