Towards applying the composition principle to verify a microkernel operating system

DOI10.1007/BFB0105408MaRDI QIDQ6567716zbMATH OpenFDO

Authors Mark R. Heckman, Cui Zhang, Brian R. Becker, Dave Peticolas, Karl Levitt, Ronald A. Olsson

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105408

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Toward compositional verification of interruptible OS kernels and device drivers
• An experiment in program composition and proof
• A modeling concept for formal verification of OS-based compositional software
• From a proven correct microkernel to trustworthy large systems
• Theorem Proving in Higher Order Logics

Cites work

• Application of the composition principle to unity-like specifications
• scientific article; zbMATH DE number 2185703 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• The existence of refinement mappings

This page was built for publication: Towards applying the composition principle to verify a microkernel operating system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6567716)