Backwards and forwards with separation logic

DOI10.1007/978-3-319-94821-8_5MaRDI QIDQ1791147zbMATH OpenOpenAlexFDO

Authors Callum Bannister, Peter Höfner, Gerwin Klein

Publication date 4 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94821-8_5

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Computer Science Logic
• False failure: creating failure models for separation logic
• Program Verification with Separation Logic
• A proof system for separation logic with magic wand
• Separation Logic Tutorial

Cited in

(5)

• False failure: creating failure models for separation logic
• Effect algebras, Girard quantales and complementation in separation logic
• Computer Science Logic
• Algebraic Methodology and Software Technology
• Dynamic separation logic

Describes a project that uses

Uses Software

• Charge!
• Coq
• VeriSmall
• Dafny
• Isabelle/HOL
• HOL
• VeriFast

This page was built for publication: Backwards and forwards with separation logic

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