Toward compositional verification of interruptible OS kernels and device drivers

DOI10.1007/s10817-017-9446-0zbMath1451.68170OpenAlexW2781213257MaRDI QIDQ1663225

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)

Related Items

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

Cites Work

• 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
• Isabelle. A generic theorem prover
• Toward compositional verification of interruptible OS kernels and device drivers
• Forward and backward simulations. I. Untimed Systems
• Mechanized semantics for the clight subset of the C language
• Deep Specifications and Certified Abstraction Layers
• Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency
• Dafny: An Automatic Program Verifier for Functional Correctness
• CONCUR 2004 - Concurrency Theory