| 2004 | Monotonic Abstraction-Refinement for CTL. | Sharon Shoham, Orna Grumberg |
| 2004 | Online Efficient Predictive Safety Analysis of Multithreaded Programs. | Koushik Sen, Grigore Rosu, Gul Agha |
| 2004 | Automated Generation of a Progress Measure for the Sweep-Line Method. | Karsten Schmidt |
| 2004 | Checking Strong Specifications Using an Extensible Software Model Checking Framework. | Robby, Edwin Rodrguez, Matthew B. Dwyer, John Hatcliff |
| 2004 | Minimal Assignments for Bounded Model Checking. | Kavita Ravi, Fabio Somenzi |
| 2004 | Resource-Optimal Scheduling Using Priced Timed Automata. | Jacob Illum Rasmussen, Kim Guldstrand Larsen, K. Subramani |
| 2004 | Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases. | Kairong Qian, Albert Nymeyer |
| 2004 | CoPS - Checker of Persistent Security. | Carla Piazza, Enrico Pivato, Sabina Rossi |
| 2004 | The Succinct Solver Suite. | Flemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, Ren Rydhof Hansen, Henrik Pilegaard, Helmut Seidl |
| 2004 | MetaGame: An Animation Tool for Model-Checking Games. | Markus Mller-Olm, Haiseung Yoo |
| 2004 | An Interpolating Theorem Prover. | Kenneth L. McMillan |
| 2004 | Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method. | Thomas Mailund, Michael Westergaard |
| 2004 | A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata. | Denis Lugiez, Peter Niebert, Sarah Zennou |
| 2004 | Binding-Time Analysis for MetaML via Type Inference and Constraint Solving. | Nathan Linger, Tim Sheard |
| 2004 | Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder. | A. E. Lindsey, Charles Pecheur |
| 2004 | A Scalable Incomplete Test for the Boundedness of UML RT Models. | Stefan Leue, Richard Mayr, Wei Wei |
| 2004 | Revisiting Positive Equality. | Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur |
| 2004 | From Complementation to Certification. | Orna Kupferman, Moshe Y. Vardi |
| 2004 | Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. | Pavel Krcl, Wang Yi |
| 2004 | How Vacuous Is Vacuous? | Arie Gurfinkel, Marsha Chechik |
| 2004 | Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points. | Jan Friso Groote, Misa Keinnen |
| 2004 | Error Explanation with Distance Metrics. | Alex Groce |
| 2004 | Numeric Domains with Summarized Dimensions. | Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv |
| 2004 | Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient. | Jaco Geldenhuys, Antti Valmari |
| 2004 | Liveness with Incomprehensible Ranking. | Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |