| 2004 | Symbolic Implementation of the Best Transformer. | Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | A Complete Method for the Synthesis of Linear Ranking Functions. | Andreas Podelski, Andrey Rybalchenko |
| 2004 | Model Checking Polygonal Differential Inclusions Using Invariance Kernels. | Gordon J. Pace, Gerardo Schneider |
| 2004 | Model Checking for Object Specifications in Hidden Algebra. | Dorel Lucanu, Gabriel Ciobanu |
| 2004 | Automatic Inference of Class Invariants. | Francesco Logozzo |
| 2004 | Constructing Quantified Invariants via Predicate Abstraction. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2004 | Boolean Algebra of Shape Analysis Constraints. | Viktor Kuncak, Martin C. Rinard |
| 2004 | Approximate Probabilistic Model Checking. | Thomas Hrault, Richard Lassaigne, Frdric Magniette, Sylvain Peyronnet |
| 2004 | Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. | John Hatcliff, Robby, Matthew B. Dwyer |
| 2004 | A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal. | David Harel |
| 2004 | Security, Protocols, and Trust. | Joshua D. Guttman |
| 2004 | Liveness with Invisible Ranking. | Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
| 2004 | Analysis of Recursive Game Graphs Using Data Flow Equations. | Kousha Etessami |
| 2004 | Static Analysis versus Software Model Checking for Bug Finding. | Dawson R. Engler, Madanlal Musuvathi |
| 2004 | Completeness and Complexity of Bounded Model Checking. | Edmund M. Clarke, Daniel Kroening, Jol Ouaknine, Ofer Strichman |
| 2004 | Security Types Preserving Compilation: (Extended Abstract). | Gilles Barthe, Amitabh Basu, Tamara Rezk |
| 2004 | Rule-Based Runtime Verification. | Howard Barringer, Allen Goldberg, Klaus Havelund, Koushik Sen |
| 2004 | Widening Operators for Powerset Domains. | Roberto Bagnara, Patricia M. Hill, Enea Zaffanella |
| 2004 | Applying Jlint to Space Exploration Software. | Cyrille Artho, Klaus Havelund |
| 2004 | Type Inference for Parameterized Race-Free Java. | Rahul Agarwal, Scott D. Stoller |
| 2003 | A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution. | Ping Yang, C. R. Ramakrishnan, Scott A. Smolka |
| 2003 | Using Simulated Execution in Verifying Distributed Algorithms. | Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli Kaynar, Nancy A. Lynch |
| 2003 | Efficient Verification of Timed Automata with BDD-Like Data-Structures. | Farn Wang |
| 2003 | Optimized Live Heap Bound Analysis. | Leena Unnikrishnan, Scott D. Stoller, Yanhong A. Liu |
| 2003 | Behavior-Based Model Construction. | Bernhard Steffen, Hardi Hungar |