Mechanised Separation Algebra

DOI10.1007/978-3-642-32347-8_22MaRDI QIDQ2914753zbMATH OpenOpenAlexFDO

Authors Gerwin Klein, Rafal Kolanski, Andrew Boyton

Publication date 20 September 2012

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_22

zbMATH Keywords

separation logicIsabelle

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of operating systems (68N25)

Recommendations

• Separable Algebras
• scientific article; zbMATH DE number 1522515
• Separable semigroup algebras
• Separable algebroids
• Separation of semialgebraic sets
• Separability in algebra and category theory
• Completely separating algebras
• Algebraic separation logic
• Recursively separable enumerated algebras
• scientific article; zbMATH DE number 3074929

Cited in

(12)

• Trinity algebra and its application to machine decompositions
• Refinement to imperative HOL
• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
• Refinement to Imperative/HOL
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• A generalised union of rely-guarantee and separation logic using permission algebras
• Higher-order separation logic in Isabelle/HOLCF
• A program construction and verification tool for separation logic
• Proof tactics for assertions in separation logic
• A formal C memory model for separation logic
• Towards algebraic separation logic
• Types, bytes, and separation logic

Describes a project that uses

Uses Software

• seL4
• Isabelle/HOL

This page was built for publication: Mechanised Separation Algebra

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