From a Proven Correct Microkernel to Trustworthy Large Systems

DOI10.1007/978-3-642-18070-5_1zbMath1308.68034OpenAlexW2100514137MaRDI QIDQ3067529

June Andronick

Publication date: 21 January 2011

Published in: Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-18070-5_1

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Uses Software

• Isabelle/HOL
• seL4

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Types, bytes, and separation logic
• Programming semantics for multiprogrammed computations

This page was built for publication: From a Proven Correct Microkernel to Trustworthy Large Systems