| 2000 | Optimizing Bchi Automata. | Kousha Etessami, Gerard J. Holzmann |
| 2000 | Revisiting Safety and Liveness in the Context of Failures. | Bernadette Charron-Bost, Sam Toueg, Anindya Basu |
| 2000 | The Impressive Power of Stopwatches. | Franck Cassez, Kim Guldstrand Larsen |
| 2000 | Secrecy and Group Creation. | Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon |
| 2000 | Typed Mobile Objects. | Michele Bugliesi, Giuseppe Castagna, Silvia Crafa |
| 2000 | Generalized Model Checking: Reasoning about Partial State Spaces. | Glenn Bruns, Patrice Godefroid |
| 2000 | Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic. | Roberto Bruni, David de Frutos-Escrig, Narciso Mart-Oliet, Ugo Montanari |
| 2000 | Verification Is Experimentation! | Ed Brinksma |
| 2000 | Failure Semantics for the Exchange of Information in Multi-Agent Systems. | Frank S. de Boer, Rogier M. van Eijk, Wiebe van der Hoek, John-Jules Ch. Meyer |
| 2000 | A Theory of Testing for Markovian Processes. | Marco Bernardo, Rance Cleaveland |
| 2000 | Functorial Concurrent Semantics for Petri Nets with Read and Inhibitor Arcs. | Paolo Baldan, Nadia Busi, Andrea Corradini, G. Michele Pinna |
| 2000 | On the Reachability Problem in Cryptographic Protocols. | Roberto M. Amadio, Denis Lugiez |
| 2000 | Exploiting Hierarchical Structure for Efficient Formal Verification. | Rajeev Alur |
| 2000 | The Control of Synchronous Systems. | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2000 | Proof-Outlines for Threads in Java. | Erika brahm-Mumm, Frank S. de Boer |
| 2000 | Reasoning about Probabilistic Lossy Channel Systems. | Parosh Aziz Abdulla, Christel Baier, S. Purushothaman Iyer, Bengt Jonsson |
| 1999 | Suptyping and Locality in Distributed Higher Order Processes (extended abstract). | Nobuko Yoshida, Matthew Hennessy |
| 1999 | Event Structures as Presheaves -Two Representation Theorems. | Glynn Winskel |
| 1999 | Testing Concurrent Systems: A Formal Approach. | Jan Tretmans |
| 1999 | Proof-Checking Protocols Using Bisimulations. | Christine Rckl, Javier Esparza |
| 1999 | Weakest-Congruence Results for Livelock-Preserving Equivalences. | Antti Puhakka, Antti Valmari |
| 1999 | Expressiveness and Distributed Implementation of Conciurrent Calculi with Link Mobility. | Catuscia Palamidessi |
| 1999 | Synchronous Structures. | David Nowak, Jean-Pierre Talpin, Paul Le Guernic |
| 1999 | On Coherence Properties in Team Rewriting Models of Concurrency. | Thomas Noll |
| 1999 | Validating Firewalls in Mobile Ambients. | Flemming Nielson, Hanne Riis Nielson, Ren Rydhof Hansen, Jacob Grydholt Jensen |