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

DOI10.1007/978-3-319-43144-4_4zbMATH Open1478.68050OpenAlexW2416645316MaRDI QIDQ2829245FDOQ2829245

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)

Cites Work

• Title not available (Why is that?)
• 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
• Using formal reasoning on a model of tasks for FreeRTOS
• Modular verification of preemptive OS kernels

Cited In (1)

• Toward compositional verification of interruptible OS kernels and device drivers

Uses Software

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

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)