| 2004 | PlayGame: A Platform for Diagnostic Games. | Li Tan |
| 2004 | Range Allocation for Separation Logic. | Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli |
| 2004 | Statistical Model Checking of Black-Box Probabilistic Systems. | Koushik Sen, Mahesh Viswanathan, Gul Agha |
| 2004 | GSTE Is Partitioned Model Checking. | Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi |
| 2004 | Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings. | Claus Schrter, Victor Khomenko |
| 2004 | Static Program Analysis via 3-Valued Logic. | Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2004 | Deductive Verification of Pipelined Machines Using First-Order Quantification. | Sandip Ray, Warren A. Hunt Jr. |
| 2004 | A Toolset for Modelling and Verification of GALS Systems. | S. Ramesh, Sampada Sonalkar, Vijay D'Silva, Naveen Chandra, B. Vijayalakshmi |
| 2004 | Global Model-Checking of Infinite-State Systems. | Nir Piterman, Moshe Y. Vardi |
| 2004 | The HiVy Tool Set. | Paula J. Pingree, Erich Mikk |
| 2004 | Rob Tristan Gerth: 1956?2003. | John O'Leary, Marly Roncken |
| 2004 | An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking. | Kedar S. Namjoshi |
| 2004 | An Experimental Evaluation of Ground Decision Procedures. | Leonardo Mendona de Moura, Harald Rue |
| 2004 | SAL 2. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari |
| 2004 | Why Model Checking Can Improve WCET Analysis. | Alexander Metzner |
| 2004 | Symbolic Model Checking of Non-regular Properties. | Martin Lange |
| 2004 | The UCLID Decision Procedure. | Shuvendu K. Lahiri, Sanjit A. Seshia |
| 2004 | Indexed Predicate Discovery for Unbounded System Verification. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2004 | Abstraction-Based Satisfiability Solving of Presburger Arithmetic. | Daniel Kroening, Jol Ouaknine, Sanjit A. Seshia, Ofer Strichman |
| 2004 | CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. | HoonSang Jin, Mohammad Awedh, Fabio Somenzi |
| 2004 | Functional Dependency for Verification Reduction. | Jie-Hong Roland Jiang, Robert K. Brayton |
| 2004 | Verification via Structure Simulation. | Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | Mechanical Mathematical Methods for Microprocessor Verification. | Warren A. Hunt Jr. |
| 2004 | Understanding Counterexamples with explain. | Alex Groce, Daniel Kroening, Flavio Lerda |
| 2004 | The Mec 5 Model-Checker. | Alain Griffault, Aymeric Vincent |