Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMATH Open1152.68423OpenAlexW2484880499MaRDI QIDQ5477643FDOQ5477643

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

Recommendations

• scientific article
• 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

Mathematics Subject Classification ID

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

Cited In (16)

• Modular verification of preemptive OS kernels
• Balancing the load. Leveraging a semantics stack for systems verification
• SOME RESULTS ON (PRE)KERNEL CATCHERS AND THE COINCIDENCE OF THE KERNEL WITH PREKERNEL
• Correct Hardware Design and Verification Methods
• Concerned with the unprivileged: user programs in kernel refinement
• Certifying low-level programs with hardware interrupts and preemptive threads
• Title not available (Why is that?)
• Formal models of operating system kernels
• Operating system verification---an overview
• Title not available (Why is that?)
• On the correctness of upper layers of automotive systems
• Formal refinement for operating systems kernels.
• From a proven correct microkernel to trustworthy large systems
• Proving fairness and implementation correctness of a microkernel scheduler
• Experience report: seL4, formally verifying a high-performance microkernel
• Secure Microkernels, State Monads and Scalable Refinement

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)