Journal of Automated Reasoning (JAR), Volume 42

Volume 42, Number 1, January 2009

• Osman Hasan, Sofiène Tahar:
  Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. 1-33
  
• C. A. Johnson:
  Computing Only Minimal Answers in Disjunctive Deductive Databases. 35-76
  
• Marko Samer, Stefan Szeider:
  Backdoor Sets of Quantified Boolean Formulas. 77-97
  
• Magnus Björk:
  First Order Stålmarck. 99-122
  

Volume 42, Numbers 2-4, April 2009

• Gerwin Klein, Ralf Huuck, Bastian Schlich:
  Operating System Verification. 123-124
  
• Harvey Tuch:
  Formal Verification of C Systems Code. 125-187
  
• Hendrik Tews, Marcus Völp, Tjark Weber:
  Formal Memory Models for the Verification of Low-Level Operating-System Code. 189-227
  
• María-del-Mar Gallardo, Pedro Merino, David Sanán:
  Model Checking Dynamic Memory Allocation in Operating Systems. 229-264
  
• Syrine Tlili, Mourad Debbabi:
  Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code. 265-300
  
• Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong:
  Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. 301-347
  
• Matthias Daum, Jan Dörrenbächer, Burkhart Wolff:
  Proving Fairness and Implementation Correctness of a Microkernel Scheduler. 349-388
  
• Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert Schirmer, Artem Starostin, Alexandra Tsyban:
  Balancing the Load. 389-454