| 2006 | Model Checking Multithreaded Programs with Asynchronous Atomic Methods. | Koushik Sen, Mahesh Viswanathan |
| 2006 | CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. | Koushik Sen, Gul Agha |
| 2006 | Fast and Generalized Polynomial Time Memory Consistency Verification. | Amitabha Roy, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang |
| 2006 | Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. | Grigore Rosu, Saddek Bensalem |
| 2006 | SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation. | Jan-Willem Roorda, Koen Claessen |
| 2006 | The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover. | Kenneth Roe |
| 2006 | EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. | Flavio M. de Paula, Alan J. Hu |
| 2006 | Lazy Abstraction with Interpolants. | Kenneth L. McMillan |
| 2006 | Termination Analysis with Calling Context Graphs. | Panagiotis Manolios, Daron Vroon |
| 2006 | Abstraction for Shape Analysis with Fast and Precise Transformers. | Tal Lev-Ami, Neil Immerman, Shmuel Sagiv |
| 2006 | Improving Pushdown System Model Checking. | Akash Lal, Thomas W. Reps |
| 2006 | SMT Techniques for Fast Predicate Abstraction. | Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras |
| 2006 | Symmetry Reduction for Probabilistic Model Checking. | Marta Z. Kwiatkowska, Gethin Norman, David Parker |
| 2006 | Safraless Compositional Synthesis. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2006 | Counterexamples with Loops for Predicate Abstraction. | Daniel Kroening, Georg Weissenbacher |
| 2006 | Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. | Pavel Krcl, Wang Yi |
| 2006 | Check It Out: On the Efficient Formal Verification of Live Sequence Charts. | Jochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke |
| 2006 | Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. | Vineet Kahlon, Aarti Gupta, Nishant Sinha |
| 2006 | Minimizing Generalized Bchi Automata. | Sudeep Juvekar, Nir Piterman |
| 2006 | Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. | Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang |
| 2006 | The Ideal of Verified Software. | Tony Hoare |
| 2006 | Bounded Model Checking for Weak Alternating Bchi Automata. | Keijo Heljanko, Tommi A. Junttila, Misa Keinnen, Martin Lange, Timo Latvala |
| 2006 | Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs. | David Harel |
| 2006 | Yasm: A Software Model-Checker for Verification and Refutation. | Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2006 | Repair of Boolean Programs with an Application to C. | Andreas Griesmayer, Roderick Bloem, Byron Cook |