Practical Tactics for Separation Logic

DOI10.1007/978-3-642-03359-9_24MaRDI QIDQ3183539zbMATH OpenOpenAlexFDO

Authors Andrew Mccreight

Publication date 20 October 2009

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

Full work available at URL https://doi.org/10.1007/978-3-642-03359-9_24

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Proof tactics for assertions in separation logic
• Computer Science Logic
• Program logics for certified compilers
• Charge! A framework for higher-order separation logic in Coq
• Separation Logic for Small-Step cminor

Cites work

• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• A nonrecursive list compacting algorithm
• Automated verification of practical garbage collectors
• Compositional shape analysis by means of bi-abduction
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Imperative Functional Programming with Isabelle/HOL
• Linear logic
• Local reasoning about a copying garbage collector
• Proving pointer programs in higher-order logic
• Separation Logic for Small-Step cminor
• Theorem Proving in Higher Order Logics
• Types, bytes, and separation logic

Cited in

(11)

• \textsc{Lincx}: a linear logical framework with first-class contexts
• Concise outlines for a complex logic: a proof outline checker for TaDA
• Separation Logic for Small-Step cminor
• Program logics for certified compilers
• Interactive matching logic proofs in Coq
• Charge! A framework for higher-order separation logic in Coq
• scientific article; zbMATH DE number 7233822 (Why is no real title available?)
• Certificates and Separation Logic
• Proof tactics for assertions in separation logic
• A machine-checked framework for relational separation logic
• Structuring the verification of heap-manipulating programs

Describes a project that uses

Uses Software

• Smallfoot
• cminor
• CompCert
• Caduceus
• Why3
• KRAKATOA
• Coq

This page was built for publication: Practical Tactics for Separation Logic

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