Operating System Verification
Formal Verification of C Systems Code
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