Types, Maps and Separation Logic

DOI10.1007/978-3-642-03359-9_20zbMath1252.03079OpenAlexW1494673397MaRDI QIDQ3183535

Gerwin Klein, Rafal Kolanski

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_20

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70)

Related Items (2)

Formal reasoning under cached address translation ⋮ Concerned with the unprivileged: user programs in kernel refinement

Uses Software

• Isabelle
• KeY-C
• Isabelle/HOL

Cites Work

• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Formal memory models for the verification of low-level operating-system code
• Operating system verification---an overview
• Types, bytes, and separation logic
• BI as an assertion language for mutable data structures
• Permission accounting in separation logic
• Computer Science Logic
• Formal Pervasive Verification of a Paging Mechanism
• Correct Hardware Design and Verification Methods
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Types, Maps and Separation Logic