| 2004 | A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings. Zhendong Su, David A. Wagner |
| 2004 | A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata. Denis Lugiez, Peter Niebert, Sarah Zennou |
| 2004 | A Scalable Incomplete Test for the Boundedness of UML RT Models. Stefan Leue, Richard Mayr, Wei Wei |
| 2004 | A Temporal Logic of Nested Calls and Returns. Rajeev Alur, Kousha Etessami, P. Madhusudan |
| 2004 | A Tool for Checking ANSI-C Programs. Edmund M. Clarke, Daniel Kroening, Flavio Lerda |
| 2004 | An Interpolating Theorem Prover. Kenneth L. McMillan |
| 2004 | Applying Game Semantics to Compositional Software Modeling and Verification. Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong |
| 2004 | Automated Generation of a Progress Measure for the Sweep-Line Method. Karsten Schmidt |
| 2004 | Automatic Creation of Environment Models via Training. Thomas Ball, Vladimir Levin, Fei Xie |
| 2004 | Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic. Danièle Beauquier, Tristan Crolard, Evguenia Prokofieva |
| 2004 | Automatic Verification of Time Sensitive Cryptographic Protocols. Giorgio Delzanno, Pierre Ganty |
| 2004 | Binding-Time Analysis for MetaML via Type Inference and Constraint Solving. Nathan Linger, Tim Sheard |
| 2004 | Checking Strong Specifications Using an Extensible Software Model Checking Framework. Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff |
| 2004 | CoPS - Checker of Persistent Security. Carla Piazza, Enrico Pivato, Sabina Rossi |
| 2004 | Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. Pavel Krcál, Wang Yi |
| 2004 | Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes. Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen |
| 2004 | Error Explanation with Distance Metrics. Alex Groce |
| 2004 | FASTer Acceleration of Counter Automata in Practice. Sébastien Bardin, Alain Finkel, Jérôme Leroux |
| 2004 | From Complementation to Certification. Orna Kupferman, Moshe Y. Vardi |
| 2004 | Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases. Kairong Qian, Albert Nymeyer |
| 2004 | How Vacuous Is Vacuous? Arie Gurfinkel, Marsha Chechik |
| 2004 | Liveness with Incomprehensible Ranking. Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
| 2004 | Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek |
| 2004 | MetaGame: An Animation Tool for Model-Checking Games. Markus Müller-Olm, Haiseung Yoo |
| 2004 | Minimal Assignments for Bounded Model Checking. Kavita Ravi, Fabio Somenzi |
| 2004 | Model Checking Discounted Temporal Properties. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga |
| 2004 | Monotonic Abstraction-Refinement for CTL. Sharon Shoham, Orna Grumberg |
| 2004 | Numeric Domains with Summarized Dimensions. Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv |
| 2004 | Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. Håkan L. S. Younes, Marta Z. Kwiatkowska, Gethin Norman, David Parker |
| 2004 | Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method. Thomas Mailund, Michael Westergaard |
| 2004 | Omega-Regular Model Checking. Bernard Boigelot, Axel Legay, Pierre Wolper |
| 2004 | Online Efficient Predictive Safety Analysis of Multithreaded Programs. Koushik Sen, Grigore Rosu, Gul Agha |
| 2004 | Refining Approximations in Software Predicate Abstraction. Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani |
| 2004 | Resource-Optimal Scheduling Using Priced Timed Automata. Jacob Illum Rasmussen, Kim Guldstrand Larsen, K. Subramani |
| 2004 | Revisiting Positive Equality. Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur |
| 2004 | Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder. A. E. Lindsey, Charles Pecheur |
| 2004 | Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points. Jan Friso Groote, Misa Keinänen |
| 2004 | Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. Greta Yorsh, Thomas W. Reps, Shmuel Sagiv |
| 2004 | SyncGen: An Aspect-Oriented Framework for Synchronization. Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno |
| 2004 | Tampere Verification Tool. Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä |
| 2004 | Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient. Jaco Geldenhuys, Antti Valmari |
| 2004 | The Succinct Solver Suite. Flemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, René Rydhof Hansen, Henrik Pilegaard, Helmut Seidl |
| 2004 | Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings Kurt Jensen, Andreas Podelski |
| 2004 | Vooduu: Verification of Object-Oriented Designs Using UPPAAL. Karsten Diethers, Michaela Huhn |