Proving fairness and implementation correctness of a microkernel scheduler

DOI10.1007/s10817-009-9119-8zbMath1191.68409OpenAlexW2051735657MaRDI QIDQ835766

Jan Dörrenbächer, Matthias Daum, Burkhart Wolff

Publication date: 31 August 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9119-8

zbMATH Keywords

formal verificationIsabelle/HOLinteractive theorem provingmicrokernel

Mathematics Subject Classification ID

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

Related Items

Balancing the load. Leveraging a semantics stack for systems verification, HOL-Boogie -- an interactive prover-backend for the verifying C compiler

Uses Software

• ACL2
• HOL-Boogie
• Isabelle
• veriSoft
• Isabelle/HOL
• KRAKATOA
• Why3
• Caduceus
• ETPS
• Boogie

Cites Work

• Balancing the load. Leveraging a semantics stack for systems verification
• Verifying a signature architecture: a comparative case study
• Operating system verification---an overview
• Isabelle/HOL. A proof assistant for higher-order logic
• An introduction to mathematical logic and type theory: To truth through proof.
• Using XCAP to Certify Realistic Systems Code: Machine Context Management
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Secure Microkernels, State Monads and Scalable Refinement
• Realistic Worst-Case Execution Time Analysis in the Context of Pervasive System Verification
• Formal Pervasive Verification of a Paging Mechanism
• Logic for Programming, Artificial Intelligence, and Reasoning
• A formulation of the simple theory of types