Compositional entailment checking for a fragment of separation logic
From MaRDI portal
Recommendations
- Compositional entailment checking for a fragment of separation logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Compositional invariant checking for overlaid and nested linked lists
- Deciding entailments in inductive separation logic with tree automata
Cites work
- scientific article; zbMATH DE number 3819693 (Why is no real title available?)
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- A complete decision procedure for linearly compositional separation logic with data constraints
- A decision procedure for satisfiability in separation logic with inductive predicates
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- BI as an assertion language for mutable data structures
- Compositional entailment checking for a fragment of separation logic
- Compositional invariant checking for overlaid and nested linked lists
- Deciding entailments in inductive separation logic with tree automata
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- On automated lemma generation for separation logic with inductive definitions
- Satisfiability modulo heap-based programs
- Separation logic modulo theories
- Shape Analysis for Composite Data Structures
- The tree width of separation logic with recursive definitions
- Tractable Reasoning in a Fragment of Separation Logic
- VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata
Cited in
(14)- Compositional satisfiability solving in separation logic
- Foundations for entailment checking in quantitative separation logic
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Make flows small again: revisiting the flow framework
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- Local reasoning for global graph properties
- A proof procedure for separation logic with inductive definitions and data
- Accurate invariant checking for programs manipulating lists and arrays with infinite data
- An efficient cyclic entailment procedure in a fragment of separation logic
- Compositional entailment checking for a fragment of separation logic
- Tractable Reasoning in a Fragment of Separation Logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- Compositional invariant checking for overlaid and nested linked lists
- Deciding entailments in inductive separation logic with tree automata
This page was built for publication: Compositional entailment checking for a fragment of separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1688543)
