| 2000 | A Comparison of Two Verification Methods for Speculative Instruction Execution. Tamarah Arons, Amir Pnueli |
| 2000 | A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors. Stefania Gnesi, Diego Latella, Gabriele Lenzini, C. Abbaneo, Arturo M. Amendola, P. Marmo |
| 2000 | A Markov Chain Model Checker. Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle |
| 2000 | Abstracting WS1S Systems to Verify Parameterized Networks. Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl |
| 2000 | An Architecture for Interactive Program Provers. Jörg Meyer, Arnd Poetzsch-Heffter |
| 2000 | An Extensible Type System for Component-Based Design. Yuhong Xiong, Edward A. Lee |
| 2000 | BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. Tevfik Bultan |
| 2000 | CASL: From Semantics to Tools. Till Mossakowski |
| 2000 | Checking for CFFD-Preorder with Tester Processes. Juhana Helovuo, Antti Valmari |
| 2000 | Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. Jean-Pierre Krimm, Laurent Mounier |
| 2000 | Consistent Integration of Formal Methods. Peter Braun, Heiko Lötzbeyer, Bernhard Schätz, Oscar Slotosch |
| 2000 | Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. Farn Wang |
| 2000 | Efficient Diagnostic Generation for Boolean Equation Systems. Radu Mateescu |
| 2000 | FMona: A Tool for Expressing Validation Techniques over Infinite State Systems. Jean-Paul Bodeveix, Mamoun Filali |
| 2000 | Fair Bisimulation. Thomas A. Henzinger, Sriram K. Rajamani |
| 2000 | Integrating Low Level Symmetries into Reachability Analysis. Karsten Schmidt |
| 2000 | Model Checking SDL with Spin. Dragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova |
| 2000 | Model Checking Security Protocols Using a Logic of Belief. Massimo Benerecetti, Fausto Giunchiglia |
| 2000 | Model Checking Support for the ASM High-Level Language. Giuseppe Del Castillo, Kirsten Winter |
| 2000 | On Memory-Block Traversal Problems in Model-Checking Timed-Systems. Fredrik Larsson, Paul Pettersson, Wang Yi |
| 2000 | On the Construction of Automata from Linear Arithmetic Constraints. Pierre Wolper, Bernard Boigelot |
| 2000 | On the Construction of Live Timed Systems. Sébastien Bornot, Gregor Gößler, Joseph Sifakis |
| 2000 | Partial Order Reductions for Security Protocol Verification. Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero |
| 2000 | Proof General: A Generic Tool for Proof Development. David Aspinall |
| 2000 | Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. Ramesh Bharadwaj, Steve Sims |
| 2000 | Symbolic Model Checking for Rectangular Hybrid Systems. Thomas A. Henzinger, Rupak Majumdar |
| 2000 | Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation. Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Roberto Segala |
| 2000 | Symbolic Reachability Analysis Based on SAT-Solvers. Parosh Aziz Abdulla, Per Bjesse, Niklas Eén |
| 2000 | Symbolic Representation of Upward-Closed Sets. Giorgio Delzanno, Jean-François Raskin |
| 2000 | The PROSPER Toolkit. Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham |
| 2000 | Tool-Based Specification of Visual Languages and Graphic Editors. Magnus Niemann, Roswitha Bardohl |
| 2000 | Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings Susanne Graf, Michael I. Schwartzbach |
| 2000 | Transitive Closures of Regular Relations for Verifying Infinite-State Systems. Bengt Jonsson, Marcus Nilsson |
| 2000 | Using Static Analysis to Improve Automatic Test Generation. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu |
| 2000 | VIP: A Visual Editor and Compiler for v-Promela. Moataz Kamel, Stefan Leue |
| 2000 | Verification of Parameterized Systems Using Logic Program Transformations. Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka |
| 2000 | ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation. Michael Goedicke, Bettina Enders, Torsten Meyer, Gabriele Taentzer |