A Formalisation of Smallfoot in HOL

DOI10.1007/978-3-642-03359-9_32zbMath1252.68266OpenAlexW29700130MaRDI QIDQ3183546

Thomas Tuerk

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_32

Mathematics Subject Classification ID

Related Items (5)

Proof tactics for assertions in separation logic ⋮ Reasoning about memory layouts ⋮ Function extraction ⋮ Reasoning about Assignments in Recursive Data Structures ⋮ Automated Cyclic Entailment Proofs in Separation Logic

Uses Software

• cminor
• Smallfoot

Cites Work

• Unnamed Item
• A semantics for concurrent separation logic
• Types, bytes, and separation logic
• Separation Logic for Small-Step cminor
• Computer Science Logic
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: A Formalisation of Smallfoot in HOL