| 2002 | From States to Transitions: Improving Translation of LTL Formulae to Bchi Automata. | Dimitra Giannakopoulou, Flavio Lerda |
| 2002 | NTIF: A General Symbolic Model for Communicating Sequential Processes with Data. | Hubert Garavel, Frdric Lang |
| 2002 | C Wolf - A Toolset for Extracting Models from C Programs. | Daniel C. DuVarney, S. Purushothaman Iyer |
| 2002 | Formal Test Purposes and the Validity of Test Cases. | Peter H. Deussen, Stephan Tobies |
| 2002 | Congruent Weak Conformance, a Partial Order among Processes. | Ronald W. Brower, Kenneth S. Stevens |
| 2002 | A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction. | Dragan Bosnacki |
| 2002 | Mechanical Translation of I/O Automaton Specifications into First-Order Logic. | Andrej Bogdanov, Stephen J. Garland, Nancy A. Lynch |
| 2002 | Submodule Construction for Specifications with Input Assumptions and Output Guarantees. | Gregor von Bochmann |
| 2002 | Bounded Model Checking for Timed Systems. | Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. | Alessandro Armando, Luca Compagna |
| 2002 | Visual Specifications for Modular Reasoning about Asynchronous Systems. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2001 | From Active to Passive: Progress in Testing of Internet Routing Protocols. | Jianping Wu, Yixin Zhao, Xia Yin |
| 2001 | Survivability Analysis of Networked Systems. | Jeannette M. Wing |
| 2001 | Patterns and Rules for Behavioural Subtyping. | Heike Wehrheim |
| 2001 | Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. | Farn Wang |
| 2001 | Towards a Formal Framework for Interoperability Testing. | Csar Viho, Sbastien Barbin, Lnaick Tanguy |
| 2001 | Testing Liveness Properties: Approximating Liveness Properties by Safety Properties. | Ulrich Ultes-Nitsche, Simon St. James |
| 2001 | Automated Derivation of ILP Implementations from SDL Specifications. | Sven Twarok, Peter Langendrfer, Hartmut Knig |
| 2001 | Compiling Real-Time Scenarios into a Timed Automaton. | Aziz Salah, Rachida Dssouli, Guy Lapalme |
| 2001 | Verifying a Sliding Window Protocol using PVS. | Vlad Rusu |
| 2001 | PAMR: A Process Algebra for the Management of Resources in Concurrent Systems. | Manuel Nez, Ismael Rodrguez |
| 2001 | Deriving Parameter Conditions for Periodic Timed Automata Satisfying Real-Time Temporal Logic Formulas. | Akio Nakata, Teruo Higashino |
| 2001 | A Method to Generate Conformance Test Sequences for FSM with Timer System Call. | Takanori Mori, K. Tokuda, Harumasa Tada, Masahiro Higuchi, Teruo Higashino |
| 2001 | Verification of Dense Time Properties using Theories of Untimed Process Algebra. | Matti Luukkainen |
| 2001 | Test Sequence Selection. | David Lee, Ruibing Hao |