Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
DOI10.1007/978-3-319-43144-4_4zbMATH Open1478.68050OpenAlexW2416645316MaRDI QIDQ2829245FDOQ2829245
Authors: June Andronick, Corey Lewis, Daniel Matichuk, Christine Rizkallah, Carroll Morgan 
Publication date: 27 October 2016
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_4
Recommendations
- Toward compositional verification of interruptible OS kernels and device drivers
- Modular verification of preemptive OS kernels
- Certifying low-level programs with hardware interrupts and preemptive threads
- Modular verification of preemptive OS kernels
- Proving fairness and implementation correctness of a microkernel scheduler
Theory of operating systems (68N25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Isabelle/HOL. A proof assistant for higher-order logic
- An axiomatic proof technique for parallel programs
- Certifying low-level programs with hardware interrupts and preemptive threads
- Title not available (Why is that?)
- Using formal reasoning on a model of tasks for FreeRTOS
- Modular verification of preemptive OS kernels
Cited In (6)
- Modular verification of preemptive OS kernels
- An intuitive formal proof for deadline driven scheduler
- Toward compositional verification of interruptible OS kernels and device drivers
- Certifying low-level programs with hardware interrupts and preemptive threads
- Using formal reasoning on a model of tasks for FreeRTOS
- Proving fairness and implementation correctness of a microkernel scheduler
Uses Software
This page was built for publication: Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829245)
