Toward compositional verification of interruptible OS kernels and device drivers

DOI10.1007/S10817-017-9446-0zbMATH Open1451.68170OpenAlexW2781213257MaRDI QIDQ1663225FDOQ1663225

Joshua Lockerman, Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu

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

zbMATH Keywords

modularityprogram verificationinterruptsabstraction layercertified OS kernelsdevice drivers

Mathematics Subject Classification ID

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 (3)

• Modular verification of preemptive OS kernels
• Toward compositional verification of interruptible OS kernels and device drivers
• Formally verifying exceptions for low-level code with separation logic

Uses Software

• Coq
• Dafny
• Isabelle
• SLAM
• z3
• CompCert
• seL4
• CertiKOS

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)