Tableaux and resource graphs for separation logic

DOI10.1093/LOGCOM/EXN066MaRDI QIDQ3406689zbMATH OpenOpenAlexFDO

Authors 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 provingseparation logictableauxcountermodels

Mathematics Subject Classification ID

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

Recommendations

• Modular tableaux calculi for separation theories
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Models and Separation Logics for Resource Trees
• The semantics of BI and resource tableaux
• Transitive Separation Logic

Cited in

(20)

• Automated theorem proving for assertions in separation logic with all connectives
• On the almighty wand
• Separation logics and modalities: a survey
• Reasoning about sequences of memory states
• A complete axiomatisation for quantifier-free separation logic
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Models and Separation Logics for Resource Trees
• A logic of separating modalities
• Resource separation in dynamic logic of propositional assignments
• Modular labelled sequent calculi for abstract separation logics
• Expressive completeness of separation logic with two variables and no separating conjunction
• Resource graphs and countermodels in resource logics
• Modular tableaux calculi for separation theories
• Graphical models of separation logic
• A modal BI logic for dynamic resource properties
• Separation logic with one quantified variable
• Completeness for a first-order abstract separation logic
• On the Almighty Wand
• scientific article; zbMATH DE number 6970800 (Why is no real title available?)
• The logic of separation logic: models and proofs

Describes a project that uses

Uses Software

• Smallfoot

This page was built for publication: Tableaux and resource graphs for separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3406689)