| 2001 | Parallel Model Checking for the Alternation Free µ-Calculus. | Benedikt Bollig, Martin Leucker, Michael Weber |
| 2001 | The LOOP Compiler for Java and JML. | Joachim van den Berg, Bart Jacobs |
| 2001 | Efficient Guiding Towards Cost-Optimality in UPPAAL. | Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn |
| 2001 | CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS. | Michel Beaudouin-Lafon, Wendy E. Mackay, Mads Jensen, Peter Andersen, Paul Janecek, Henry Michael Lassen, Kasper Lund, Kjeld Hyer Mortensen, Stephanie Munck, Anne V. Ratzer, Katrine Ravn, Sren Christensen, Kurt Jensen |
| 2001 | Boolean and Cartesian Abstraction for Model Checking C Programs. | Thomas Ball, Andreas Podelski, Sriram K. Rajamani |
| 2001 | Parameterized Verification of Multithreaded Software Libraries. | Thomas Ball, Sagar Chaki, Sriram K. Rajamani |
| 2001 | Abstraction in Probabilistic Process Algebra. | Suzana Andova, Jos C. M. Baeten |
| 2001 | Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2000 | An Extensible Type System for Component-Based Design. | Yuhong Xiong, Edward A. Lee |
| 2000 | On the Construction of Automata from Linear Arithmetic Constraints. | Pierre Wolper, Bernard Boigelot |
| 2000 | Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. | Farn Wang |
| 2000 | Integrating Low Level Symmetries into Reachability Analysis. | Karsten Schmidt |
| 2000 | Verification of Parameterized Systems Using Logic Program Transformations. | Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka |
| 2000 | Tool-Based Specification of Visual Languages and Graphic Editors. | Magnus Niemann, Roswitha Bardohl |
| 2000 | CASL: From Semantics to Tools. | Till Mossakowski |
| 2000 | An Architecture for Interactive Program Provers. | Jrg Meyer, Arnd Poetzsch-Heffter |
| 2000 | Efficient Diagnostic Generation for Boolean Equation Systems. | Radu Mateescu |
| 2000 | On Memory-Block Traversal Problems in Model-Checking Timed-Systems. | Fredrik Larsson, Paul Pettersson, Wang Yi |
| 2000 | Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. | Jean-Pierre Krimm, Laurent Mounier |
| 2000 | VIP: A Visual Editor and Compiler for v-Promela. | Moataz Kamel, Stefan Leue |
| 2000 | Transitive Closures of Regular Relations for Verifying Infinite-State Systems. | Bengt Jonsson, Marcus Nilsson |
| 2000 | A Markov Chain Model Checker. | Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle |
| 2000 | Fair Bisimulation. | Thomas A. Henzinger, Sriram K. Rajamani |
| 2000 | Symbolic Model Checking for Rectangular Hybrid Systems. | Thomas A. Henzinger, Rupak Majumdar |
| 2000 | Checking for CFFD-Preorder with Tester Processes. | Juhana Helovuo, Antti Valmari |