Secure Microkernels, State Monads and Scalable Refinement

DOI10.1007/978-3-540-71067-7_16zbMath1165.68454OpenAlexW2146530476MaRDI QIDQ3543657

Gerwin Klein, David Cock, Thomas D. Sewell

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_16

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (9)

Eisbach: a proof method language for Isabelle ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ A Hoare Logic for the State Monad ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model ⋮ Concerned with the unprivileged: user programs in kernel refinement ⋮ seL4 Enforces Integrity ⋮ A Framework for the Automatic Formal Verification of Refinement from Cogent to C ⋮ Operating system verification---an overview ⋮ Cogent: uniqueness types and certifying compilation

Uses Software

• Isabelle/HOL
• Haskell
• Kit

Cites Work

• A principled approach to operating system construction in Haskell
• Types, bytes, and separation logic
• Specification and verification of the UCLA Unix security kernel
• Guarded commands, nondeterminacy and formal derivation of programs
• Data Refinement
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• The logic of demand in Haskell

This page was built for publication: Secure Microkernels, State Monads and Scalable Refinement