1. Operating System Verification

   • Gerwin Klein
   • Ralf Huuck
   • Bastian Schlich

   EditorialNotes 17 March 2009 Pages: 123 - 124

2. Formal Verification of C Systems Code

   • Harvey Tuch

   OriginalPaper 02 April 2009 Pages: 125 - 187

3. Formal Memory Models for the Verification of Low-Level Operating-System Code

   • Hendrik Tews
   • Marcus Völp
   • Tjark Weber

   OriginalPaper 23 April 2009 Pages: 189 - 227

4. Model Checking Dynamic Memory Allocation in Operating Systems

   • María del Mar Gallardo
   • Pedro Merino
   • David Sanán

   OriginalPaper 27 March 2009 Pages: 229 - 264

5. Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code

   • Syrine Tlili
   • Mourad Debbabi

   OriginalPaper 21 March 2009 Pages: 265 - 300

6. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads

   • Xinyu Feng
   • Zhong Shao
   • Yuan Dong

   OriginalPaper 20 March 2009 Pages: 301 - 347

7. Proving Fairness and Implementation Correctness of a Microkernel Scheduler

   • Matthias Daum
   • Jan Dörrenbächer
   • Burkhart Wolff

   OriginalPaper 05 May 2009 Pages: 349 - 388

8. Balancing the Load

   • Eyad Alkassar
   • Mark A. Hillebrand
   • Alexandra Tsyban

   OriginalPaper 28 March 2009 Pages: 389 - 454