Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477643zbMATH OpenOpenAlexFDO

Authors Mauro Gargano, Mark A. Hillebrand, Dirk C. Leinenbach, Wolfgang J. Paul

Publication date 6 July 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 3854401
• Operating system verification---an overview
• scientific article; zbMATH DE number 1751915
• From a proven correct microkernel to trustworthy large systems
• Toward compositional verification of interruptible OS kernels and device drivers

Cited in

(18)

• On the correctness of upper layers of automotive systems
• Operating system verification---an overview
• Toward compositional verification of interruptible OS kernels and device drivers
• Experience report: seL4, formally verifying a high-performance microkernel
• From a proven correct microkernel to trustworthy large systems
• scientific article; zbMATH DE number 3845012 (Why is no real title available?)
• Formal models of operating system kernels
• Secure Microkernels, State Monads and Scalable Refinement
• scientific article; zbMATH DE number 1751915 (Why is no real title available?)
• SOME RESULTS ON (PRE)KERNEL CATCHERS AND THE COINCIDENCE OF THE KERNEL WITH PREKERNEL
• Modular verification of preemptive OS kernels
• Correct Hardware Design and Verification Methods
• Formal refinement for operating systems kernels.
• Towards applying the composition principle to verify a microkernel operating system
• Concerned with the unprivileged: user programs in kernel refinement
• Certifying low-level programs with hardware interrupts and preemptive threads
• Proving fairness and implementation correctness of a microkernel scheduler
• Balancing the load. Leveraging a semantics stack for systems verification

This page was built for publication: Theorem Proving in Higher Order Logics

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