Operating system verification---an overview
From MaRDI portal
Publication:1040002
DOI10.1007/S12046-009-0002-4zbMATH Open1192.68432OpenAlexW2019404692MaRDI QIDQ1040002FDOQ1040002
Authors: 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
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Cites Work
- TAME: Using PVS strategies for special-purpose theorem proving
- Isabelle/HOL. A proof assistant for higher-order logic
- The existence of refinement mappings
- An axiomatic basis for computer programming
- Title not available (Why is that?)
- The B-Book
- Secure Microkernels, State Monads and Scalable Refinement
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Types, bytes, and separation logic
- Using XCAP to Certify Realistic Systems Code: Machine Context Management
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Title not available (Why is that?)
- Title not available (Why is that?)
- Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
- Certifying low-level programs with hardware interrupts and preemptive threads
- Logic for Programming, Artificial Intelligence, and Reasoning
- A Linear Time Algorithm for Deciding Subject Security
- Proving that programs eventually do something good
- A Unified Memory Model for Pointers
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
- Title not available (Why is that?)
- Specification and verification of the UCLA Unix security kernel
- Integration of a Software Model Checker into Isabelle
- Formal Pervasive Verification of a Paging Mechanism
- Theorem Proving in Higher Order Logics
- Correct Hardware Design and Verification Methods
- The nucleus of a multiprogramming system
- Creating high confidence in a separation kernel
- Proof techniques for hierarchically structured programs
- A model for verification of data security in operating systems
- Title not available (Why is that?)
- Programming semantics for multiprogrammed computations
Cited In (22)
- Formal Pervasive Verification of a Paging Mechanism
- Theorem Proving in Higher Order Logics
- Balancing the load. Leveraging a semantics stack for systems verification
- Formal memory models for the verification of low-level operating-system code
- Social processes, program verification and all that
- A modeling concept for formal verification of OS-based compositional software
- A formalization of multi-tape Turing machines
- System-level non-interference of constant-time cryptography. I: Model
- Verifying feedforward neural networks for classification in Isabelle/HOL
- Concerned with the unprivileged: user programs in kernel refinement
- Toward compositional verification of interruptible OS kernels and device drivers
- On theorem prover-based testing
- Using formal reasoning on a model of tasks for FreeRTOS
- seL4 enforces integrity
- Optimisation of maintenance concept choice using risk-decision factor -- a case study
- Title not available (Why is that?)
- Verifying distributed systems: the operational approach
- Proving fairness and implementation correctness of a microkernel scheduler
- Experience report: seL4, formally verifying a high-performance microkernel
- A vindication of program verification
- Using XCAP to Certify Realistic Systems Code: Machine Context Management
- Types, Maps and Separation Logic
Uses Software
This page was built for publication: Operating system verification---an overview
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1040002)
