Certifying low-level programs with hardware interrupts and preemptive threads

DOI10.1007/S10817-009-9118-9MaRDI QIDQ835764zbMATH OpenOpenAlexFDO

Authors Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong

Publication date 31 August 2009

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-009-9118-9

zbMATH Keywords

modularityseparation logichardware interruptsoperating system verificationpreemptive threadssynchronization primitivesthread libraries

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Theory of operating systems (68N25)

Recommendations

• Toward compositional verification of interruptible OS kernels and device drivers
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• Modular verification of preemptive OS kernels
• Modular verification of preemptive OS kernels
• Formally verifying exceptions for low-level code with separation logic

Cites work

• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 1420791 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A Tutorial on Satisfiability Modulo Theories
• A syntactic approach to type soundness
• A typed interrupt calculus
• An axiomatic basis for computer programming
• BI as an assertion language for mutable data structures
• CONCUR 2004 - Concurrency Theory
• CONCUR 2004 - Concurrency Theory
• Local Reasoning for Storable Locks and Threads
• Modular verification of concurrent assembly code with dynamic thread creation and termination
• Monitors
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• Oracle Semantics for Concurrent Separation Logic
• Permission accounting in separation logic
• Separation and information hiding
• Stack-based typed assembly language
• Tentative steps toward a development method for interfering programs
• Theorem Proving in Higher Order Logics
• Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts
• Using XCAP to Certify Realistic Systems Code: Machine Context Management

Cited in

(7)

• Modular verification of preemptive OS kernels
• System-level non-interference of constant-time cryptography. I: Model
• Trace-based verification of imperative programs with I/O
• Toward compositional verification of interruptible OS kernels and device drivers
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• Operating system verification---an overview
• Formally verifying exceptions for low-level code with separation logic

Describes a project that uses

Uses Software

• TALx86
• Kit
• Smallfoot
• veriSoft
• Coq

This page was built for publication: Certifying low-level programs with hardware interrupts and preemptive threads

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