Compositional entailment checking for a fragment of separation logic
From MaRDI portal
Publication:1688543
DOI10.1007/s10703-017-0289-4zbMath1377.68073OpenAlexW46575596MaRDI QIDQ1688543
Constantin Enea, Ondřej Lengál, Tomáš Vojnar, Mihaela Sighireanu
Publication date: 8 January 2018
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-017-0289-4
Formal languages and automata (68Q45) Logic in computer science (03B70) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Local Reasoning for Global Graph Properties, A proof procedure for separation logic with inductive definitions and data, An efficient cyclic entailment procedure in a fragment of separation logic, Compositional satisfiability solving in separation logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Compositional Entailment Checking for a Fragment of Separation Logic
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
- VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata
- Separation Logic Modulo Theories
- Tractable Reasoning in a Fragment of Separation Logic
- Deciding Entailments in Inductive Separation Logic with Tree Automata
- On Automated Lemma Generation for Separation Logic with Inductive Definitions
- Satisfiability Modulo Heap-Based Programs
- A decision procedure for satisfiability in separation logic with inductive predicates
- The Tree Width of Separation Logic with Recursive Definitions
- BI as an assertion language for mutable data structures
- Compositional Invariant Checking for Overlaid and Nested Linked Lists
- Shape Analysis for Composite Data Structures
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
