From separation logic to first-order logic

DOI10.1007/978-3-540-31982-5_25MaRDI QIDQ5705900zbMATH OpenOpenAlexFDO

Authors Cristiano Calcagno, Philippa Gardner, Matthew Hague

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b106850

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Data structures (68P05)

Recommendations

• A decidable fragment of separation logic
• Transitive Separation Logic
• A separation logic with data: small models and automation
• A decision procedure for separation logic in SMT
• Separation logic with one quantified variable

Cited in

(17)

• Verify heaps via unified model checking
• Extended transitive separation logic
• Completeness and expressiveness of pointer program verification by separation logic
• A logic of reachable patterns in linked data-structures
• Transitive Separation Logic
• On the Almighty Wand
• A Spatial Equational Logic for the Applied π-Calculus
• scientific article; zbMATH DE number 1078591 (Why is no real title available?)
• Separation logics and modalities: a survey
• A first-order logic with frames
• On temporal and separation logics
• A complete axiomatisation for quantifier-free separation logic
• Program Verification with Separation Logic
• Reasoning about sequences of memory states
• Representation of Peano arithmetic in separation logic
• Expressiveness results for an inductive logic of separated relations
• Encoding Peano arithmetic in a minimal fragment of separation logic

This page was built for publication: From separation logic to first-order logic

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