| 2002 | Simulation as Coarsest Partition Problem. | Raffaella Gentilini, Carla Piazza, Alberto Policriti |
| 2002 | Timed Automata with Asynchronous Processes: Schedulability and Decidability. | Elena Fersman, Paul Pettersson, Wang Yi |
| 2002 | Model Checking Large-Scale and Parameterized Resource Allocation Systems. | E. Allen Emerson, Vineet Kahlon |
| 2002 | Towards the Automated Verification of Multithreaded Java Programs. | Giorgio Delzanno, Jean-Franois Raskin, Laurent Van Begin |
| 2002 | STG: A Symbolic Test Generation Tool. | Duncan Clarke, Thierry Jron, Vlad Rusu, Elena Zinovieva |
| 2002 | Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems. | Hojung Cha, Rhan Ha |
| 2002 | Applicability of Fair Simulation. | Doron Bustan, Orna Grumberg |
| 2002 | Improving the Verification of Timed Systems Using Influence Information. | Vctor A. Braberman, Diego Garbervetsky, Alfredo Olivero |
| 2002 | Beyond Parameterized Verification. | Marco Bozzano, Giorgio Delzanno |
| 2002 | CLPS-B - A Constraint Solver for B. | Fabrice Bouquet, Bruno Legeard, Fabien Peureux |
| 2002 | Black Box Unfolding with Local First Search. | Sbastien Bornot, Rmi Morin, Peter Niebert, Sarah Zennou |
| 2002 | Resource-Constrained Model Checking of Recursive Programs. | Samik Basu, K. Narayan Kumar, L. Robert Pokorny, C. R. Ramakrishnan |
| 2002 | Relative Completeness of Abstraction Refinement for Software Model Checking. | Thomas Ball, Andreas Podelski, Sriram K. Rajamani |
| 2002 | A Functional Semantics of Attribute Grammars. | Kevin Backhouse |
| 2002 | The ForSpec Temporal Logic: A New Temporal Property-Specification Language. | Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Yael Zbar |
| 2002 | TIMES - A Tool for Modelling and Implementation of Embedded Systems. | Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson, Wang Yi |
| 2002 | Preemptive Job-Shop Scheduling Using Stopwatch Automata. | Yasmina Abdeddam, Oded Maler |
| 2001 | A Library for Composite Symbolic Representations. | Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan |
| 2001 | Satisfiability Checking Using Boolean Expression Diagrams. | Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard |
| 2001 | Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. | Miroslav N. Velev |
| 2001 | Branching vs. Linear Time: Final Showdown. | Moshe Y. Vardi |
| 2001 | A Technique for Invariant Generation. | Ashish Tiwari, Harald Rue, Hassen Sadi, Natarajan Shankar |
| 2001 | Simulation Revisited. | Li Tan, Rance Cleaveland |
| 2001 | TATOO: Testing and Analysis Tool for Object- Oriented Software. | Amie L. Souter, Tiffany M. Wong, Stacey A. Shindo, Lori L. Pollock |
| 2001 | Model Checking Syllabi and Student Carreers. | Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia |