The logic of separation logic: models and proofs

DOI10.1007/978-3-031-43513-3_22MaRDI QIDQ6541164zbMATH OpenFDO

Authors Frank S. de Boer, Hans-Dieter A. Hiep, Stijn De Gouw

Publication date 17 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43513-3_22

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• 30 years of research and development around Coq
• A complete axiomatisation for quantifier-free separation logic
• A decision procedure for separation logic in SMT
• Completeness for a first-order abstract separation logic
• Completeness in the theory of types
• Expressive completeness of separation logic with two variables and no separating conjunction
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 824731 (Why is no real title available?)
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• On the almighty wand
• Predicativity and Feferman
• Second-Order Logic and Foundations of Mathematics
• Static Analysis
• Tableaux and resource graphs for separation logic
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• The completeness of the first-order functional calculus
• The semantics and proof theory of the logic of bunched implications
• Viper: a verification infrastructure for permission-based reasoning

Cited in

(1)

• First-order hybrid separation logic

This page was built for publication: The logic of separation logic: models and proofs

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