Operating system verification---an overview
From MaRDI portal
Publication:1040002
DOI10.1007/s12046-009-0002-4zbMath1192.68432OpenAlexW2019404692MaRDI QIDQ1040002
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
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
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
