1. A Mechanical Analysis of Program Verification Strategies

   • Sandip Ray
   • Warren A. Hunt Jr.
   • J. Strother Moore

   OriginalPaper 14 March 2008 Pages: 245 - 269

2. A Mechanized Proof of the Basic Perturbation Lemma

   • Jesús Aransay
   • Clemens Ballarin
   • Julio Rubio

   OriginalPaper 16 January 2008 Pages: 271 - 292

3. Rewriting with Equivalence Relations in ACL2

   • Bishop Brock
   • Matt Kaufmann
   • J Strother Moore

   OriginalPaper 15 January 2008 Pages: 293 - 306

4. Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves

   • Laurence Rideau
   • Bernard Paul Serpette
   • Xavier Leroy

   OriginalPaper 12 January 2008 Pages: 307 - 326

5. Nominal Techniques in Isabelle/HOL

   • Christian Urban

   OriginalPaper 14 March 2008 Pages: 327 - 356

6. A Resolution-Based Decision Procedure for \(\boldsymbol{\mathcal{SHOIQ}}\)

   • Yevgeny Kazakov
   • Boris Motik

   Erratum 18 March 2008 Pages: 357 - 357