| 2006 | A Fast Linear-Arithmetic Solver for DPLL(T). Bruno Dutertre, Leonardo Mendonça de Moura |
| 2006 | Abstraction for Shape Analysis with Fast and Precise Transformers. Tal Lev-Ami, Neil Immerman, Shmuel Sagiv |
| 2006 | Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. Grigore Rosu, Saddek Bensalem |
| 2006 | Antichains: A New Algorithm for Checking Universality of Finite Automata. Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin |
| 2006 | Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. Rachel Tzoref, Orna Grumberg |
| 2006 | Automatic Termination Proofs for Programs with Shape-Shifting Heaps. Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2006 | Bounded Model Checking for Weak Alternating Büchi Automata. Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala |
| 2006 | Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
| 2006 | CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. Koushik Sen, Gul Agha |
| 2006 | Causal Atomicity. Azadeh Farzan, P. Madhusudan |
| 2006 | Check It Out: On the Efficient Formal Verification of Live Sequence Charts. Jochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke |
| 2006 | Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. Pavel Krcál, Wang Yi |
| 2006 | Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings Thomas Ball, Robert B. Jones |
| 2006 | Counterexamples with Loops for Predicate Abstraction. Daniel Kroening, Georg Weissenbacher |
| 2006 | Deriving Small Unsatisfiable Cores with Dominators. Roman Gershman, Maya Koifman, Ofer Strichman |
| 2006 | DiVinE - A Tool for Distributed Verification. Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek |
| 2006 | Don't Care Words with an Application to the Automata-Based Approach for Real Addition. Jochen Eisinger, Felix Klaedtke |
| 2006 | EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. Flavio M. de Paula, Alan J. Hu |
| 2006 | FAST Extended Release. Sébastien Bardin, Jérôme Leroux, Gérald Point |
| 2006 | Fast and Generalized Polynomial Time Memory Consistency Verification. Amitabha Roy, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang |
| 2006 | Formal Specifications on Industrial-Strength Code-From Myth to Reality. Manuvir Das |
| 2006 | Formal Verification of a Lazy Concurrent List-Based Set Algorithm. Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir |
| 2006 | I Think I Voted: E-Voting vs. Democracy. David L. Dill |
| 2006 | Improving Pushdown System Model Checking. Akash Lal, Thomas W. Reps |
| 2006 | LEVER: A Tool for Learning Based Verification. Abhay Vardhan, Mahesh Viswanathan |
| 2006 | Languages of Nested Trees. Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
| 2006 | Lazy Abstraction with Interpolants. Kenneth L. McMillan |
| 2006 | Lazy Shape Analysis. Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz |
| 2006 | Lookahead Widening. Denis Gopan, Thomas W. Reps |
| 2006 | Minimizing Generalized Büchi Automata. Sudeep Juvekar, Nir Piterman |
| 2006 | Model Checking Multithreaded Programs with Asynchronous Atomic Methods. Koushik Sen, Mahesh Viswanathan |
| 2006 | Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs. David Harel |
| 2006 | Programs with Lists Are Counter Automata. Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar |
| 2006 | Repair of Boolean Programs with an Application to C. Andreas Griesmayer, Roderick Bloem, Byron Cook |
| 2006 | SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation. Jan-Willem Roorda, Koen Claessen |
| 2006 | SMT Techniques for Fast Predicate Abstraction. Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras |
| 2006 | Safraless Compositional Synthesis. Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2006 | Some Complexity Results for SystemVerilog Assertions. Doron Bustan, John Havlicek |
| 2006 | Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. Vineet Kahlon, Aarti Gupta, Nishant Sinha |
| 2006 | Symmetry Reduction for Probabilistic Model Checking. Marta Z. Kwiatkowska, Gethin Norman, David Parker |
| 2006 | Termination Analysis with Calling Context Graphs. Panagiotis Manolios, Daron Vroon |
| 2006 | Termination of Integer Linear Programs. Mark Braverman |
| 2006 | Terminator: Beyond Safety. Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2006 | The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover. Kenneth Roe |
| 2006 | The Ideal of Verified Software. Tony Hoare |
| 2006 | The Power of Hybrid Acceleration. Bernard Boigelot, Frédéric Herbreteau |
| 2006 | Ticc: A Tool for Interface Compatibility and Composition. B. Thomas Adler, Luca de Alfaro, Leandro Dias da Silva, Marco Faella, Axel Legay, Vishwanath Raman, Pritam Roy |
| 2006 | Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang |
| 2006 | Yasm: A Software Model-Checker for Verification and Refutation. Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2006 | cascade: C Assertion Checker and Deductive Engine. Nikhil Sethi, Clark W. Barrett |