Expressive completeness of separation logic with two variables and no separating conjunction
From MaRDI portal
Recommendations
- Expressive completeness of separation logic with two variables and no separating conjunction
- Two-Variable Separation Logic and Its Inner Circle
- Completeness and expressiveness of pointer program verification by separation logic
- Separation logic with one quantified variable
- Separation logic with one quantified variable
Cites work
- A Marriage of Rely/Guarantee and Separation Logic
- A Modal Logic for Chopping Intervals
- A Proof of Kamp's theorem
- A proof system for separation logic with magic wand
- Automated theorem proving for assertions in separation logic with all connectives
- Computer Science Logic
- Deciding local theory extensions via E-matching
- Expressive completeness of separation logic with two variables and no separating conjunction
- Expressiveness and complexity of graph logic
- Foundations for decision problems in separation logic with general inductive predicates
- scientific article; zbMATH DE number 3827831 (Why is no real title available?)
- scientific article; zbMATH DE number 747023 (Why is no real title available?)
- scientific article; zbMATH DE number 618821 (Why is no real title available?)
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- scientific article; zbMATH DE number 1841824 (Why is no real title available?)
- Impossibility of an algorithm for the decision problem in finite classes
- Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness
- Metric propositional neighborhood logics: expressiveness, decidability, and undecidability
- Nondeterministic phase semantics and the undecidability of Boolean BI
- On the almighty wand
- On the Decision Problem for Two-Variable First-Order Logic
- On the Expressive Power of Graph Logic
- Proof search for propositional abstract separation logics via labelled sequents
- Quantitative separation logic and programs with lists
- Reasoning about heap manipulating programs using automata techniques
- Separating Graph Logic from MSO
- Separation logic modulo theories
- Separation logic with one quantified variable
- Static Analysis
- Tableaux and resource graphs for separation logic
- Temporal logic can be more expressive
- Ten Years of Hoare's Logic: A Survey—Part I
- The tree width of separation logic with recursive definitions
- Tractable Reasoning in a Fragment of Separation Logic
- Two-variable logic on data trees and XML reasoning
- Two-Variable Separation Logic and Its Inner Circle
- Undecidability of propositional separation logic and its neighbours
- Undecidability results on two-variable logics
Cited in
(14)- Semipositivity in separation logic with two variables
- Reasoning about block-based cloud storage systems via separation logic
- Separation logic and logics with team semantics
- Separation logic with one quantified variable
- Completeness and expressiveness of pointer program verification by separation logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- Two-Variable Separation Logic and Its Inner Circle
- Completeness for a first-order abstract separation logic
- Expressive completeness of separation logic with two variables and no separating conjunction
- On temporal and separation logics
- Tractability of separation logic with inductive definitions: beyond lists
- The logic of separation logic: models and proofs
- Expressive completeness of separation logic in block-based cloud storage systems
- Expressiveness results for an inductive logic of separated relations
This page was built for publication: Expressive completeness of separation logic with two variables and no separating conjunction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277913)
