| 2004 | A Formal Reduction for Lock-Free Parallel Algorithms. Hui Gao, Wim H. Hesselink |
| 2004 | A Toolset for Modelling and Verification of GALS Systems. S. Ramesh, Sampada Sonalkar, Vijay D'Silva, Naveen Chandra, B. Vijayalakshmi |
| 2004 | Abstract Regular Model Checking. Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar |
| 2004 | Abstraction-Based Satisfiability Solving of Presburger Arithmetic. Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman |
| 2004 | An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking. Kedar S. Namjoshi |
| 2004 | An Experimental Evaluation of Ground Decision Procedures. Leonardo Mendonça de Moura, Harald Rueß |
| 2004 | Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values. Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang |
| 2004 | CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. Clark W. Barrett, Sergey Berezin |
| 2004 | CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. HoonSang Jin, Mohammad Awedh, Fabio Somenzi |
| 2004 | Compositional Specification and Model Checking in GSTE. Jin Yang, Carl-Johan H. Seger |
| 2004 | Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings Rajeev Alur, Doron A. Peled |
| 2004 | DPLL( T): Fast Decision Procedures. Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2004 | Deductive Verification of Pipelined Machines Using First-Order Quantification. Sandip Ray, Warren A. Hunt Jr. |
| 2004 | Efficient Modeling of Embedded Memories in Bounded Model Checking. Malay K. Ganai, Aarti Gupta, Pranav Ashar |
| 2004 | Formal Analysis of Java Programs in JavaFAN. Azadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu |
| 2004 | Functional Dependency for Verification Reduction. Jie-Hong Roland Jiang, Robert K. Brayton |
| 2004 | GSTE Is Partitioned Model Checking. Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi |
| 2004 | Global Model-Checking of Infinite-State Systems. Nir Piterman, Moshe Y. Vardi |
| 2004 | Image Computation in Infinite State Model Checking. Alain Finkel, Jérôme Leroux |
| 2004 | Indexed Predicate Discovery for Unbounded System Verification. Shuvendu K. Lahiri, Randal E. Bryant |
| 2004 | JNuke: Efficient Dynamic Analysis for Java. Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller |
| 2004 | MCK: Model Checking the Logic of Knowledge. Peter Gammie, Ron van der Meyden |
| 2004 | Mechanical Mathematical Methods for Microprocessor Verification. Warren A. Hunt Jr. |
| 2004 | ObsSlice: A Timed Automata Slicer Based on Observers. Víctor A. Braberman, Diego Garbervetsky, Alfredo Olivero |
| 2004 | Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings. Claus Schröter, Victor Khomenko |
| 2004 | PlayGame: A Platform for Diagnostic Games. Li Tan |
| 2004 | Proving More Properties with Bounded Model Checking. Mohammad Awedh, Fabio Somenzi |
| 2004 | QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj |
| 2004 | Range Allocation for Separation Logic. Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli |
| 2004 | Regular Model Checking for LTL(MSO). Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso, Mayank Saksena |
| 2004 | Rob Tristan Gerth: 1956?2003. John O'Leary, Marly Roncken |
| 2004 | SAL 2. Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari |
| 2004 | Static Program Analysis via 3-Valued Logic. Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2004 | Statistical Model Checking of Black-Box Probabilistic Systems. Koushik Sen, Mahesh Viswanathan, Gul Agha |
| 2004 | Stuck-Free Conformance. Cédric Fournet, C. A. R. Hoare, Sriram K. Rajamani, Jakob Rehof |
| 2004 | Symbolic Model Checking of Non-regular Properties. Martin Lange |
| 2004 | Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures. Farn Wang |
| 2004 | Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. Amit Goel, Randal E. Bryant |
| 2004 | Termination of Linear Programs. Ashish Tiwari |
| 2004 | The HiVy Tool Set. Paula J. Pingree, Erich Mikk |
| 2004 | The Mec 5 Model-Checker. Alain Griffault, Aymeric Vincent |
| 2004 | The UCLID Decision Procedure. Shuvendu K. Lahiri, Sanjit A. Seshia |
| 2004 | Understanding Counterexamples with explain. Alex Groce, Daniel Kroening, Flavio Lerda |
| 2004 | Using Interface Refinement to Integrate Formal Verification into the Design Cycle. Jacob Chang, Sergey Berezin, David L. Dill |
| 2004 | Verification of an Advanced mips-Type Out-of-Order Execution Algorithm. Tamarah Arons |
| 2004 | Verification via Structure Simulation. Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | Verifying omega-Regular Properties of Markov Chains. Doron Bustan, Sasha Rubin, Moshe Y. Vardi |
| 2004 | WSAT: A Tool for Formal Analysis of Web Services. Xiang Fu, Tevfik Bultan, Jianwen Su |
| 2004 | Why Model Checking Can Improve WCET Analysis. Alexander Metzner |
| 2004 | Widening Arithmetic Automata. Constantinos Bartzis, Tevfik Bultan |
| 2004 | Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang |
| 2004 | Zing: A Model Checker for Concurrent Software. Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie |