Recommendations
Cites work
- scientific article; zbMATH DE number 1612488 (Why is no real title available?)
- scientific article; zbMATH DE number 439891 (Why is no real title available?)
- scientific article; zbMATH DE number 2127501 (Why is no real title available?)
- scientific article; zbMATH DE number 46740 (Why is no real title available?)
- scientific article; zbMATH DE number 193479 (Why is no real title available?)
- scientific article; zbMATH DE number 1285682 (Why is no real title available?)
- scientific article; zbMATH DE number 2123258 (Why is no real title available?)
- scientific article; zbMATH DE number 830949 (Why is no real title available?)
- scientific article; zbMATH DE number 3410595 (Why is no real title available?)
- A Linear Time Algorithm for Deciding Subject Security
- A Unified Memory Model for Pointers
- A model for verification of data security in operating systems
- An axiomatic basis for computer programming
- Certifying low-level programs with hardware interrupts and preemptive threads
- Correct Hardware Design and Verification Methods
- Creating high confidence in a separation kernel
- Formal Pervasive Verification of a Paging Mechanism
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Integration of a Software Model Checker into Isabelle
- 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
- Logic for Programming, Artificial Intelligence, and Reasoning
- Programming semantics for multiprogrammed computations
- Proof techniques for hierarchically structured programs
- Proving that programs eventually do something good
- Secure Microkernels, State Monads and Scalable Refinement
- Specification and verification of the UCLA Unix security kernel
- TAME: Using PVS strategies for special-purpose theorem proving
- The B-Book
- The existence of refinement mappings
- The nucleus of a multiprogramming system
- Theorem Proving in Higher Order Logics
- Types, bytes, and separation logic
- Using XCAP to Certify Realistic Systems Code: Machine Context Management
- Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
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
- Concerned with the unprivileged: user programs in kernel refinement
- Verifying feedforward neural networks for classification in Isabelle/HOL
- 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
- scientific article; zbMATH DE number 3854401 (Why is no real title available?)
- 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
Describes a project that uses
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)
