| 2004 | A Complete Method for the Synthesis of Linear Ranking Functions. Andreas Podelski, Andrey Rybalchenko |
| 2004 | A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal. David Harel |
| 2004 | Analysis of Recursive Game Graphs Using Data Flow Equations. Kousha Etessami |
| 2004 | Applying Jlint to Space Exploration Software. Cyrille Artho, Klaus Havelund |
| 2004 | Approximate Probabilistic Model Checking. Thomas Hérault, Richard Lassaigne, Frédéric Magniette, Sylvain Peyronnet |
| 2004 | Automatic Inference of Class Invariants. Francesco Logozzo |
| 2004 | Boolean Algebra of Shape Analysis Constraints. Viktor Kuncak, Martin C. Rinard |
| 2004 | Certifying Temporal Properties for Compiled C Programs. Songtao Xia, James Hook |
| 2004 | Checking Interval Based Properties for Reactive Systems. Yu Pei, Qiwen Xu |
| 2004 | Completeness and Complexity of Bounded Model Checking. Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman |
| 2004 | Constructing Quantified Invariants via Predicate Abstraction. Shuvendu K. Lahiri, Randal E. Bryant |
| 2004 | Construction of a Semantic Model for a Typed Assembly Language. Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu |
| 2004 | History-Dependent Scheduling for Cryptographic Processes. Vincent Vanackère |
| 2004 | Liveness with Invisible Ranking. Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
| 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 | On the Expressive Power of Canonical Abstraction. Shmuel Sagiv |
| 2004 | Rule-Based Runtime Verification. Howard Barringer, Allen Goldberg, Klaus Havelund, Koushik Sen |
| 2004 | Security Types Preserving Compilation: (Extended Abstract). Gilles Barthe, Amitabh Basu, Tamara Rezk |
| 2004 | Security, Protocols, and Trust. Joshua D. Guttman |
| 2004 | Static Analysis versus Software Model Checking for Bug Finding. Dawson R. Engler, Madanlal Musuvathi |
| 2004 | Symbolic Implementation of the Best Transformer. Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | Type Inference for Parameterized Race-Free Java. Rahul Agarwal, Scott D. Stoller |
| 2004 | Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings Bernhard Steffen, Giorgio Levi |
| 2004 | Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. John Hatcliff, Robby, Matthew B. Dwyer |
| 2004 | Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone. Reinhard Wilhelm |
| 2004 | Widening Operators for Powerset Domains. Roberto Bagnara, Patricia M. Hill, Enea Zaffanella |