Operating system verification---an overview

DOI10.1007/s12046-009-0002-4zbMath1192.68432OpenAlexW2019404692MaRDI QIDQ1040002

Gerwin Klein

Publication date: 23 November 2009

Published in: Sādhanā (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s12046-009-0002-4

zbMATH Keywords

theorem provingoperating systemsformal software verification

Mathematics Subject Classification ID

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

Related Items

Proving fairness and implementation correctness of a microkernel scheduler, Formal memory models for the verification of low-level operating-system code, Balancing the load. Leveraging a semantics stack for systems verification, Types, Maps and Separation Logic, Optimisation of maintenance concept choice using risk-decision factor – a case study, System-level non-interference of constant-time cryptography. I: Model, Verifying feedforward neural networks for classification in Isabelle/HOL, Using formal reasoning on a model of tasks for FreeRTOS, A Vindication of Program Verification, On theorem prover-based testing, Concerned with the unprivileged: user programs in kernel refinement, A formalization of multi-tape Turing machines, seL4 Enforces Integrity, Social processes, program verification and all that

Uses Software

• ACL2
• veriSoft
• Isabelle/HOL
• PVS
• Haskell
• HOL Light
• NQTHM
• Specware
• Kit
• EROS
• Archive Formal Proofs
• TAME
• Verified Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Certifying low-level programs with hardware interrupts and preemptive threads
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• Isabelle/HOL. A proof assistant for higher-order logic
• TAME: Using PVS strategies for special-purpose theorem proving
• Creating high confidence in a separation kernel
• Types, bytes, and separation logic
• Proving that programs eventually do something good
• Using XCAP to Certify Realistic Systems Code: Machine Context Management
• Secure Microkernels, State Monads and Scalable Refinement
• Specification and verification of the UCLA Unix security kernel
• Proof techniques for hierarchically structured programs
• A Linear Time Algorithm for Deciding Subject Security
• A model for verification of data security in operating systems
• The B-Book
• Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
• Formal certification of a compiler back-end or
• Integration of a Software Model Checker into Isabelle
• A Unified Memory Model for Pointers
• Formal Pervasive Verification of a Paging Mechanism
• Theorem Proving in Higher Order Logics
• Correct Hardware Design and Verification Methods
• Programming semantics for multiprogrammed computations
• An axiomatic basis for computer programming
• The nucleus of a multiprogramming system
• Logic for Programming, Artificial Intelligence, and Reasoning