| 2005 | Symmetry Reduction in SAT-Based Model Checking. | Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip |
| 2005 | On Statistical Model Checking of Stochastic Systems. | Koushik Sen, Mahesh Viswanathan, Gul Agha |
| 2005 | Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
| 2005 | Bounded Model Checking of Concurrent Programs. | Ishai Rabinovitz, Orna Grumberg |
| 2005 | Algorithmic Algebraic Model Checking I: Challenges from Systems Biology. | Carla Piazza, Marco Antoniotti, Venkatesh Mysore, Alberto Policriti, Franz Winkler, Bud Mishra |
| 2005 | TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems. | Enric Pastor, Marco A. Pea, Marc Sol |
| 2005 | Concrete Model Checking with Abstract Matching and Refinement. | Corina S. Pasareanu, Radek Pelnek, Willem Visser |
| 2005 | The Orchids Intrusion Detection Tool. | Julien Olivain, Jean Goubault-Larrecq |
| 2005 | DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. | Robert Nieuwenhuis, Albert Oliveras |
| 2005 | Randomized Algorithms for Program Analysis and Verification. | George C. Necula, Sumit Gulwani |
| 2005 | Compositional Analysis of Floating-Point Linear Numerical Filters. | David Monniaux |
| 2005 | Yet Another Decision Procedure for Equality Logic. | Orly Meir, Ofer Strichman |
| 2005 | Data Structure Specifications via Local Equality Axioms. | Scott McPeak, George C. Necula |
| 2005 | Abstraction Refinement via Inductive Learning. | Alexey Loginov, Thomas W. Reps, Shmuel Sagiv |
| 2005 | Extended Weighted Pushdown Systems. | Akash Lal, Thomas W. Reps, Gogul Balakrishnan |
| 2005 | Predicate Abstraction via Symbolic Decision Procedures. | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
| 2005 | Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants. | Roope Kaivola |
| 2005 | Reasoning About Threads Communicating via Locks. | Vineet Kahlon, Franjo Ivancic, Aarti Gupta |
| 2005 | Program Repair as a Game. | Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem |
| 2005 | Interpolant-Based Transition Relation Approximation. | Ranjit Jhala, Kenneth L. McMillan |
| 2005 | F-Soft: Software Verification Platform. | Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar |
| 2005 | Incremental and Complete Bounded Model Checking for Full PLTL. | Keijo Heljanko, Tommi A. Junttila, Timo Latvala |
| 2005 | Abstraction Refinement for Bounded Model Checking. | Anubhav Gupta, Ofer Strichman |
| 2005 | Expand, Enlarge and Check... Made Efficient. | Gilles Geeraerts, Jean-Franois Raskin, Laurent Van Begin |
| 2005 | Romeo: A Tool for Analyzing Time Petri Nets. | Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier H. Roux |