Operating System Verification
Formal Verification of C Systems Code : Structured Types, Separation Logic and Theorem Proving
Formal Memory Models for the Verification of Low-Level Operating-System Code
Model Checking Dynamic Memory Allocation in Operating Systems
Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads
Proving Fairness and Implementation Correctness of a Microkernel Scheduler
Balancing the Load : Leveraging a Semantics Stack for Systems Verification