| 2000 | ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation. | Michael Goedicke, Bettina Enders, Torsten Meyer, Gabriele Taentzer |
| 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 | 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 | Symbolic Representation of Upward-Closed Sets. | Giorgio Delzanno, Jean-Franois Raskin |
| 2000 | Partial Order Reductions for Security Protocol Verification. | Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero |
| 2000 | Model Checking Support for the ASM High-Level Language. | Giuseppe Del Castillo, Kirsten Winter |
| 2000 | BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. | Tevfik Bultan |
| 2000 | Consistent Integration of Formal Methods. | Peter Braun, Heiko Ltzbeyer, Bernhard Schtz, Oscar Slotosch |
| 2000 | Using Static Analysis to Improve Automatic Test Generation. | Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu |
| 2000 | Model Checking SDL with Spin. | Dragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova |
| 2000 | On the Construction of Live Timed Systems. | Sbastien Bornot, Gregor Gler, Joseph Sifakis |
| 2000 | FMona: A Tool for Expressing Validation Techniques over Infinite State Systems. | Jean-Paul Bodeveix, Mamoun Filali |
| 2000 | Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. | Ramesh Bharadwaj, Steve Sims |
| 2000 | Model Checking Security Protocols Using a Logic of Belief. | Massimo Benerecetti, Fausto Giunchiglia |
| 2000 | Abstracting WS1S Systems to Verify Parameterized Networks. | Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl |
| 2000 | Proof General: A Generic Tool for Proof Development. | David Aspinall |
| 2000 | A Comparison of Two Verification Methods for Speculative Instruction Execution. | Tamarah Arons, Amir Pnueli |
| 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 En |
| 1999 | Timed Diagnostics for Reachability Properties. | Stavros Tripakis |
| 1999 | Some Issues in the Software Engineering of Verification Tools. | Perdita Stevens |
| 1999 | A Theorem Prover-Based Analysis Tool for Object-Oriented Databases. | David Spelt, Susan J. Even |
| 1999 | A Period Assignment Algorithm for Real-Time System Design. | Minsoo Ryu, Seongsoo Hong |
| 1999 | On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. | Vlad Rusu, Eli Singerman |
| 1999 | Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL. | Cornelia Pusch |