Certifying low-level programs with hardware interrupts and preemptive threads

DOI10.1007/s10817-009-9118-9zbMath1191.68176OpenAlexW2150401476MaRDI QIDQ835764

Yuan Dong, Zhong Shao, Xinyu Feng, Yu Guo

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

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

Related Items (6)

Toward compositional verification of interruptible OS kernels and device drivers ⋮ Formally verifying exceptions for low-level code with separation logic ⋮ System-level non-interference of constant-time cryptography. I: Model ⋮ Trace-based verification of imperative programs with I/O ⋮ Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency ⋮ Operating system verification---an overview

Uses Software

• Coq
• veriSoft
• Smallfoot
• Kit
• TALx86

Cites Work

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

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