Tableaux and Resource Graphs for Separation Logic

DOI10.1093/logcom/exn066zbMath1193.03061OpenAlexW2131238121MaRDI QIDQ3406689

Didier Galmiche, Daniel Méry

Publication date: 19 February 2010

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/c3211cd6e08dadd64a86447f7b549c21b0ad7809

zbMATH Keywords

theorem provingtableauxseparation logiccountermodels

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35)

Related Items

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction, A logic of separating modalities, Automated Theorem Proving for Assertions in Separation Logic with All Connectives, A Modal BI Logic for Dynamic Resource Properties, Completeness for a First-Order Abstract Separation Logic, Separation logic with one quantified variable, Separation logics and modalities: a survey, On the almighty wand, Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic, Reasoning about sequences of memory states, On the Almighty Wand, Unnamed Item, Unnamed Item

Uses Software

• Smallfoot