| 2004 | Vooduu: Verification of Object-Oriented Designs Using UPPAAL. | Karsten Diethers, Michaela Huhn |
| 2004 | SyncGen: An Aspect-Oriented Framework for Synchronization. | Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno |
| 2004 | Automatic Verification of Time Sensitive Cryptographic Protocols. | Giorgio Delzanno, Pierre Ganty |
| 2004 | A Tool for Checking ANSI-C Programs. | Edmund M. Clarke, Daniel Kroening, Flavio Lerda |
| 2004 | Omega-Regular Model Checking. | Bernard Boigelot, Axel Legay, Pierre Wolper |
| 2004 | Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. | Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelnek |
| 2004 | Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic. | Danile Beauquier, Tristan Crolard, Evguenia Prokofieva |
| 2004 | FASTer Acceleration of Counter Automata in Practice. | Sbastien Bardin, Alain Finkel, Jrme Leroux |
| 2004 | Automatic Creation of Environment Models via Training. | Thomas Ball, Vladimir Levin, Fei Xie |
| 2004 | Refining Approximations in Software Predicate Abstraction. | Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani |
| 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 | A Temporal Logic of Nested Calls and Returns. | Rajeev Alur, Kousha Etessami, P. Madhusudan |
| 2004 | Model Checking Discounted Temporal Properties. | Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Marille Stoelinga |
| 2004 | Applying Game Semantics to Compositional Software Modeling and Verification. | Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong |
| 2003 | The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems. | Dezhuang Zhang, Rance Cleaveland, Eugene W. Stark |
| 2003 | Checking Properties of Heap-Manipulating Procedures with a Constraint Solver. | Mandana Vaziri, Daniel Jackson |
| 2003 | LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios. | Sebastin Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee |
| 2003 | Automated Module Composition. | Stavros Tripakis |
| 2003 | Optimistic Synchronization-Based State-Space Reduction. | Scott D. Stoller, Ernie Cohen |
| 2003 | Modeling and Analysis of Power-Aware Systems. | Oleg Sokolsky, Anna Philippou, Insup Lee, Kyriakos Christou |
| 2003 | Using Petri Net Invariants in State Space Construction. | Karsten Schmidt |
| 2003 | Automatic Abstraction without Counterexamples. | Kenneth L. McMillan, Nina Amla |
| 2003 | A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. | Radu Mateescu |
| 2003 | What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code. | Peter Lee |
| 2003 | Generalized Symbolic Execution for Model Checking and Testing. | Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser |