Practical Tactics for Separation Logic

DOI10.1007/978-3-642-03359-9_24zbMath1252.68261OpenAlexW169519546MaRDI QIDQ3183539

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)

Related Items

LINCX: A Linear Logical Framework with First-Class Contexts ⋮ A Machine-Checked Framework for Relational Separation Logic

Uses Software

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

Cites Work

• Unnamed Item
• Linear logic
• Proving pointer programs in higher-order logic
• Types, bytes, and separation logic
• Local reasoning about a copying garbage collector
• Separation Logic for Small-Step cminor
• Imperative Functional Programming with Isabelle/HOL
• Compositional shape analysis by means of bi-abduction
• Automated verification of practical garbage collectors
• Formal certification of a compiler back-end or
• Theorem Proving in Higher Order Logics
• A nonrecursive list compacting algorithm

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