Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency

DOI10.1007/978-3-319-43144-4_4zbMath1478.68050OpenAlexW2416645316MaRDI QIDQ2829245

Christine Rizkallah, Corey Lewis, June Andronick, Daniel Matichuk, 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

Mathematics Subject Classification ID

Theory of operating systems (68N25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Toward compositional verification of interruptible OS kernels and device drivers

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Poly/ML
• FreeRTOS
• GitHub

Cites Work

• Unnamed Item
• Certifying low-level programs with hardware interrupts and preemptive threads
• Using formal reasoning on a model of tasks for FreeRTOS
• An axiomatic proof technique for parallel programs
• Isabelle/HOL. A proof assistant for higher-order logic
• Modular verification of preemptive OS kernels

This page was built for publication: Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency