Toward compositional verification of interruptible OS kernels and device drivers
DOI10.1007/S10817-017-9446-0zbMATH Open1451.68170OpenAlexW2781213257MaRDI QIDQ1663225FDOQ1663225
Authors: Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu 
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-017-9446-0
Recommendations
- Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
- Theorem Proving in Higher Order Logics
- Formal memory models for the verification of low-level operating-system code
- From a proven correct microkernel to trustworthy large systems
- Operating system verification---an overview
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Dafny: an automatic program verifier for functional correctness
- Isabelle. A generic theorem prover
- Forward and backward simulations. I. Untimed Systems
- CONCUR 2004 - Concurrency Theory
- Mechanized semantics for the clight subset of the C language
- Certifying low-level programs with hardware interrupts and preemptive threads
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Toward compositional verification of interruptible OS kernels and device drivers
- Deep specifications and certified abstraction layers
- Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
Cited In (12)
- Theorem Proving in Higher Order Logics
- Modular verification of preemptive OS kernels
- Towards applying the composition principle to verify a microkernel operating system
- Safe functional systems through integrity types and verified assembly
- A modeling concept for formal verification of OS-based compositional software
- Modular verification of preemptive OS kernels
- Toward compositional verification of interruptible OS kernels and device drivers
- Certifying low-level programs with hardware interrupts and preemptive threads
- Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
- Noninterference for operating system kernels
- Formally verifying exceptions for low-level code with separation logic
- Deep specifications and certified abstraction layers
Uses Software
This page was built for publication: Toward compositional verification of interruptible OS kernels and device drivers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663225)
