| 2003 | Construction of Efficient BDDs for Bounded Arithmetic Constraints. | Constantinos Bartzis, Tevfik Bultan |
| 2003 | Code-Based Test Generation for Validation of Functional Processor Descriptions. | Fabrice Baray, Philippe Codognet, Daniel Diaz, Henri Michel |
| 2003 | Resets vs. Aborts in Linear Temporal Logic. | Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi |
| 2003 | Experimental Analysis of Different Techniques for Bounded Model Checking. | Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel |
| 2003 | Modular Strategies for Recursive Game Graphs. | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2003 | Counter-Example Guided Predicate Abstraction of Hybrid Systems. | Rajeev Alur, Thao Dang, Franjo Ivancic |
| 2003 | On Optimal Scheduling under Uncertainty. | Yasmina Abdeddam, Eugene Asarin, Oded Maler |
| 2002 | Explicit Modeling of Influences, and of Their Absence, in Distributed Systems. | Horst F. Wedde, Arnim Wedig |
| 2002 | An Analysis of Zero-Clairvoyant Scheduling. | K. Subramani |
| 2002 | Real-Time Systems Design with PEP. | Christian Stehno |
| 2002 | Digitisation and Full Abstraction for Dense-Time Model Checking. | Jol Ouaknine |
| 2002 | Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. | Radu Mateescu |
| 2002 | Software Construction and Analysis Tools for Future Space Missions. | Michael R. Lowry |
| 2002 | Compositional Verification Using SVL Scripts. | Frdric Lang |
| 2002 | Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. | Marta Z. Kwiatkowska, Gethin Norman, David Parker |
| 2002 | Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS. | Taeho Kim, David W. J. Stringer-Calvert, Sung Deok Cha |
| 2002 | Fate and Free Will in Error Traces. | HoonSang Jin, Kavita Ravi, Fabio Somenzi |
| 2002 | Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis. | HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi |
| 2002 | Alloy: A New Technology for Software Modelling. | Daniel Jackson |
| 2002 | A Temporal Logic Based Theory of Test Coverage and Generation. | Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Hasan Ural |
| 2002 | Parallelisation of the Petri Net Unfolding Algorithm. | Keijo Heljanko, Victor Khomenko, Maciej Koutny |
| 2002 | Synthesizing Monitors for Safety Properties. | Klaus Havelund, Grigore Rosu |
| 2002 | Temporal Debugging for Concurrent Systems. | Elsa L. Gunter, Doron A. Peled |
| 2002 | Adaptive Model Checking. | Alex Groce, Doron A. Peled, Mihalis Yannakakis |
| 2002 | Exploring Very Large State Spaces Using Genetic Algorithms. | Patrice Godefroid, Sarfraz Khurshid |