| 2000 | A Theory of Testing for Markovian Processes. Marco Bernardo, Rance Cleaveland |
| 2000 | A Unifying Approach to Data-Independence. Ranko Lazic, David Nowak |
| 2000 | Action Contraction. Arend Rensink |
| 2000 | An Implicitly-Typed Deadlock-Free Process Calculus. Naoki Kobayashi, Shin Saito, Eijiro Sumii |
| 2000 | Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic. Roberto Bruni, David de Frutos-Escrig, Narciso Martí-Oliet, Ugo Montanari |
| 2000 | CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings Catuscia Palamidessi |
| 2000 | Chi Calculus with Mismatch. Yuxi Fu, Zhenrong Yang |
| 2000 | Combining Theorem Proving and Model Checking through Symbolic Analysis. Natarajan Shankar |
| 2000 | Compositional Performance Analysis Using Probabilistic I/O Automata. Eugene W. Stark |
| 2000 | Deriving Bisimulation Congruences for Reactive Systems. James J. Leifer, Robin Milner |
| 2000 | Emptiness Is Decidable for Asynchronous Cellular Machines. Dietrich Kuske |
| 2000 | Exploiting Hierarchical Structure for Efficient Formal Verification. Rajeev Alur |
| 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 | Formal Models for Communication-Based Design. Alberto L. Sangiovanni-Vincentelli, Marco Sgroi, Luciano Lavagno |
| 2000 | From Process Calculi to Process Frameworks. Philippa Gardner |
| 2000 | Functorial Concurrent Semantics for Petri Nets with Read and Inhibitor Arcs. Paolo Baldan, Nadia Busi, Andrea Corradini, G. Michele Pinna |
| 2000 | Generalized Model Checking: Reasoning about Partial State Spaces. Glenn Bruns, Patrice Godefroid |
| 2000 | LP Deadlock Checking Using Partial Order Dependencies. Victor Khomenko, Maciej Koutny |
| 2000 | Model Checking with Finite Complete Prefixes Is PSPACE-Complete. Keijo Heljanko |
| 2000 | Nondeterminism and Probabilistic Choice: Obeying the Laws. Michael W. Mislove |
| 2000 | On the Reachability Problem in Cryptographic Protocols. Roberto M. Amadio, Denis Lugiez |
| 2000 | Open Systems in Reactive Environments: Control and Synthesis. Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, Moshe Y. Vardi |
| 2000 | Optimizing Büchi Automata. Kousha Etessami, Gerard J. Holzmann |
| 2000 | Pomsets for Local Trace Languages - Recognizability, Logic & Petri Nets. Dietrich Kuske, Rémi Morin |
| 2000 | Process Languages for Rooted Eager Bisimulation. Irek Ulidowski, Shoji Yuen |
| 2000 | Process Spaces. Radu Negulescu |
| 2000 | Programming Access Control: The KLAIM Experience. Rocco De Nicola, Gian-Luigi Ferrari, Rosario Pugliese |
| 2000 | Proof-Outlines for Threads in Java. Erika Ábrahám-Mumm, Frank S. de Boer |
| 2000 | Reachability Analysis for Some Models of Infinite-State Transition Systems. Oscar H. Ibarra, Tevfik Bultan, Jianwen Su |
| 2000 | Reasoning about Probabilistic Lossy Channel Systems. Parosh Aziz Abdulla, Christel Baier, S. Purushothaman Iyer, Bengt Jonsson |
| 2000 | Revisiting Safety and Liveness in the Context of Failures. Bernadette Charron-Bost, Sam Toueg, Anindya Basu |
| 2000 | Secrecy and Group Creation. Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon |
| 2000 | Secure Information Flow for Concurrent Processes. Jan Jürjens |
| 2000 | Synthesizing Distributed Finite-State Systems from MSCs. Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni |
| 2000 | The Control of Synchronous Systems. Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2000 | The Impressive Power of Stopwatches. Franck Cassez, Kim Guldstrand Larsen |
| 2000 | Typed Mobile Objects. Michele Bugliesi, Giuseppe Castagna, Silvia Crafa |
| 2000 | Typing Non-uniform Concurrent Objects. António Ravara, Vasco Thudichum Vasconcelos |
| 2000 | Verification Is Experimentation! Ed Brinksma |
| 2000 | Verification Using Tabled Logic Programming. C. R. Ramakrishnan |
| 2000 | Verifying Quantitative Properties of Continuous Probabilistic Timed Automata. Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston |
| 2000 | Weak Bisimulation for Probabilistic Systems. Anna Philippou, Insup Lee, Oleg Sokolsky |
| 2000 | Well-Abstracted Transition Systems. Alain Finkel, S. Purushothaman Iyer, Grégoire Sutre |