| 2000 | Compositional Performance Analysis Using Probabilistic I/O Automata. | Eugene W. Stark |
| 2000 | Combining Theorem Proving and Model Checking through Symbolic Analysis. | Natarajan Shankar |
| 2000 | Formal Models for Communication-Based Design. | Alberto L. Sangiovanni-Vincentelli, Marco Sgroi, Luciano Lavagno |
| 2000 | Action Contraction. | Arend Rensink |
| 2000 | Typing Non-uniform Concurrent Objects. | Antnio Ravara, Vasco Thudichum Vasconcelos |
| 2000 | Verification Using Tabled Logic Programming. | C. R. Ramakrishnan |
| 2000 | Weak Bisimulation for Probabilistic Systems. | Anna Philippou, Insup Lee, Oleg Sokolsky |
| 2000 | Programming Access Control: The KLAIM Experience. | Rocco De Nicola, Gian-Luigi Ferrari, Rosario Pugliese |
| 2000 | Process Spaces. | Radu Negulescu |
| 2000 | Synthesizing Distributed Finite-State Systems from MSCs. | Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni |
| 2000 | Nondeterminism and Probabilistic Choice: Obeying the Laws. | Michael W. Mislove |
| 2000 | Deriving Bisimulation Congruences for Reactive Systems. | James J. Leifer, Robin Milner |
| 2000 | A Unifying Approach to Data-Independence. | Ranko Lazic, David Nowak |
| 2000 | Verifying Quantitative Properties of Continuous Probabilistic Timed Automata. | Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston |
| 2000 | Pomsets for Local Trace Languages - Recognizability, Logic & Petri Nets. | Dietrich Kuske, Rmi Morin |
| 2000 | Emptiness Is Decidable for Asynchronous Cellular Machines. | Dietrich Kuske |
| 2000 | Open Systems in Reactive Environments: Control and Synthesis. | Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, Moshe Y. Vardi |
| 2000 | An Implicitly-Typed Deadlock-Free Process Calculus. | Naoki Kobayashi, Shin Saito, Eijiro Sumii |
| 2000 | LP Deadlock Checking Using Partial Order Dependencies. | Victor Khomenko, Maciej Koutny |
| 2000 | Secure Information Flow for Concurrent Processes. | Jan Jrjens |
| 2000 | Reachability Analysis for Some Models of Infinite-State Transition Systems. | Oscar H. Ibarra, Tevfik Bultan, Jianwen Su |
| 2000 | Model Checking with Finite Complete Prefixes Is PSPACE-Complete. | Keijo Heljanko |
| 2000 | From Process Calculi to Process Frameworks. | Philippa Gardner |
| 2000 | Chi Calculus with Mismatch. | Yuxi Fu, Zhenrong Yang |
| 2000 | Well-Abstracted Transition Systems. | Alain Finkel, S. Purushothaman Iyer, Grgoire Sutre |