Modular verification of preemptive OS kernels

DOI10.1017/S0956796813000075MaRDI QIDQ5398329zbMATH OpenFDO

Authors Alexey Gotsman, Hongseok Yang

Publication date 27 February 2014

Published in Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Theory of operating systems (68N25)

Recommendations

• Modular verification of preemptive OS kernels
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• Certifying low-level programs with hardware interrupts and preemptive threads
• Toward compositional verification of interruptible OS kernels and device drivers
• Theorem Proving in Higher Order Logics

Cited in

(4)

• SOME RESULTS ON (PRE)KERNEL CATCHERS AND THE COINCIDENCE OF THE KERNEL WITH PREKERNEL
• Modular verification of preemptive OS kernels
• Certifying low-level programs with hardware interrupts and preemptive threads
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency

This page was built for publication: Modular verification of preemptive OS kernels

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