| 2003 | A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. Radu Mateescu |
| 2003 | A New Knowledge Representation Strategy for Cryptographic Protocol Analysis. Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano |
| 2003 | A Set of Performance and Dependability Analysis Components for CADP. Holger Hermanns, Christophe Joubert |
| 2003 | An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. Sergey Berezin, Vijay Ganesh, David L. Dill |
| 2003 | Automated Module Composition. Stavros Tripakis |
| 2003 | Automatic Abstraction without Counterexamples. Kenneth L. McMillan, Nina Amla |
| 2003 | Automatic Test Generation with AGATHA. Céline Bigot, Alain Faivre, Jean-Pierre Gallois, Arnault Lapitre, David Lugato, Jean-Yves Pierron, Nicolas Rapin |
| 2003 | BANANA - A Tool for Boundary Ambients Nesting ANAlysis. Chiara Braghin, Agostino Cortesi, Stefano Filippone, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza |
| 2003 | Bounded Model Checking for Past LTL. Marco Benedetti, Alessandro Cimatti |
| 2003 | Branching Processes of High-Level Petri Nets. Victor Khomenko, Maciej Koutny |
| 2003 | Checking Properties of Heap-Manipulating Procedures with a Constraint Solver. Mandana Vaziri, Daniel Jackson |
| 2003 | Code-Based Test Generation for Validation of Functional Processor Descriptions. Fabrice Baray, Philippe Codognet, Daniel Diaz, Henri Michel |
| 2003 | Compositional Analysis for Verification of Parameterized Systems. Samik Basu, C. R. Ramakrishnan |
| 2003 | Construction of Efficient BDDs for Bounded Arithmetic Constraints. Constantinos Bartzis, Tevfik Bultan |
| 2003 | Counter-Example Guided Predicate Abstraction of Hybrid Systems. Rajeev Alur, Thao Dang, Franjo Ivancic |
| 2003 | Decidability of Invariant Validation for Paramaterized Systems. Pascal Fontaine, E. Pascal Gribomont |
| 2003 | Experimental Analysis of Different Techniques for Bounded Model Checking. Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel |
| 2003 | Generalized Symbolic Execution for Model Checking and Testing. Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser |
| 2003 | LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios. Sebastián Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee |
| 2003 | Large State Space Visualization. Jan Friso Groote, Frank van Ham |
| 2003 | Learning Assumptions for Compositional Verification. Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu |
| 2003 | Modeling and Analysis of Power-Aware Systems. Oleg Sokolsky, Anna Philippou, Insup Lee, Kyriakos Christou |
| 2003 | Modular Strategies for Recursive Game Graphs. Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2003 | Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. Marcelo Glusman, Gila Kamhi, Sela Mador-Haim, Ranan Fraer, Moshe Y. Vardi |
| 2003 | On Optimal Scheduling under Uncertainty. Yasmina Abdeddaïm, Eugene Asarin, Oded Maler |
| 2003 | On the Universal and Existential Fragments of the µ-Calculus. Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar |
| 2003 | Optimistic Synchronization-Based State-Space Reduction. Scott D. Stoller, Ernie Cohen |
| 2003 | Pattern-Based Abstraction for Verifying Secrecy in Protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn |
| 2003 | Proof-Like Counter-Examples. Arie Gurfinkel, Marsha Chechik |
| 2003 | Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols. E. Allen Emerson, Vineet Kahlon |
| 2003 | Resets vs. Aborts in Linear Temporal Logic. Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi |
| 2003 | Saturation Unbound. Gianfranco Ciardo, Robert M. Marmorstein, Radu Siminiceanu |
| 2003 | Schedulability Analysis Using Two Clocks. Elena Fersman, Leonid Mokrushin, Paul Pettersson, Wang Yi |
| 2003 | Simple Representative Instantiations for Multicast Protocols. Javier Esparza, Monika Maidl |
| 2003 | State Class Constructions for Branching Analysis of Time Petri Nets. Bernard Berthomieu, François Vernadat |
| 2003 | Static Guard Analysis in Timed Automata Verification. Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim Guldstrand Larsen |
| 2003 | Strategies for Combining Decision Procedures. Sylvain Conchon, Sava Krstic |
| 2003 | The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems. Dezhuang Zhang, Rance Cleaveland, Eugene W. Stark |
| 2003 | Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings Hubert Garavel, John Hatcliff |
| 2003 | Using Petri Net Invariants in State Space Construction. Karsten Schmidt |
| 2003 | Verics: A Tool for Verifying Timed Automata and Estelle Specifications. Piotr Dembinski, Agata Janowska, Pawel Janowski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Bozena Wozna, Andrzej Zbrzezny |
| 2003 | Verification and Improvement of the Sliding Window Protocol. Dmitri Chkliaev, Jozef Hooman, Erik P. de Vink |
| 2003 | Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald |
| 2003 | What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code. Peter Lee |