Types, Maps and Separation Logic

DOI10.1007/978-3-642-03359-9_20MaRDI QIDQ3183535zbMATH OpenOpenAlexFDO

Authors Rafal Kolanski, Gerwin Klein

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)

Recommendations

• Types, bytes, and separation logic
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Computer Science Logic
• High-level separation logic for low-level code
• Separation Logic for Higher-Order Store

Cites work

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

Cited in

(11)

• Formal reasoning under cached address translation
• Recognizability, hypergraph operations, and logical types
• Types and coalgebraic structure
• Concerned with the unprivileged: user programs in kernel refinement
• Type logics and pregroups
• Abstracting Allocation
• Logical Mappings
• Frame rules from answer types for code pointers
• High-level separation logic for low-level code
• Types, bytes, and separation logic
• Hoare type theory, polymorphism and separation

Describes a project that uses

Uses Software

• Isabelle/HOL
• KeY-C
• Isabelle

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

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