| 2000 | Formal Treatment of a Family of Fixed-Point Problems on Graphs by CafeOBJ. | Tetsuo Tamai |
| 2000 | Embedding Formally Proved Code in a Smart Card: Converting B to C. | Antoine Requet, Galle Bossu |
| 2000 | Formal Foundations of Object-Oriented Modeling Notations. | Claudia Pons, Gabriel Baum |
| 2000 | Formal Derivation of Multilayered Hardware/Software Structures. | Toomas P. Plaks |
| 2000 | SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol. | Hong Peng, Sofine Tahar, Ferhat Khendek |
| 2000 | The Use of Mathematics in Software Engineering. | David Lorge Parnas |
| 2000 | Highly Reliable Component-Based Software Development by Using Algebraic Behavioral Specification. | Michihiro Matsumoto, Kokichi Futatsugi |
| 2000 | Translating UAN into CSP. | Ian MacColl, David A. Carrington |
| 2000 | Structuring Reactive Systems in B AMN. | Kevin Lano, Kelly Androutsopoulos, Pauline Kan |
| 2000 | A Unified Algebraic Framework for Specifying Communication Protocols. | Mohamed Jmaiel |
| 2000 | Legacy Code. | C. A. R. Hoare |
| 2000 | Using Use Cases in Executable Z. | Wolfgang Grieskamp, Markus Lepper |
| 2000 | Offering Formal Verification Capabilities for Industry Standard Case Tools: Challenges and Results. | Werner Damm |
| 2000 | Mechanical Verification of Transaction Processing Systems. | Dmitri Chkliaev, Jozef Hooman, Peter van der Stok |
| 2000 | An Animatable Operational Semantics of the Verilog Hardware Description Language. | Jonathan P. Bowen, Jifeng He, Qiwen Xu |
| 2000 | Fragmented Retrenchment, Concurrency and Fairness. | Richard Banach, Michael Poppleton |
| 2000 | Maximally Abstract Retrenchments. | Richard Banach |
| 2000 | ClawZ: Control Laws in Z. | R. D. Arthan, P. Caseley, Colin O'Halloran, Alf Smith |
| 2000 | An Integrated CSP-Based Tool for the Visualisation, Animation and Performance Evaluation of Message Passing Algorithms. | Ali E. Abdallah, Mark Green |
| 2000 | Filter Promotion Transformation Strategies for Deriving Efficient Programs from Z Specifications. | Ali E. Abdallah |
| 1998 | B Model Animation for External Verification. | Hlne Waeselynck, Salimeh Behnia |
| 1998 | Automatic Synthesis of Controllers from Formal Specifications. | Enrico Tronci |
| 1998 | A Calculus Based on the Agent-Place Model. | Kenji Taguchi, Keijiro Araki |
| 1998 | Proving Inductive Theorems Using Witnessed Test Sets. | Zhiqing Shao, Yongqiang Sun, Guoxin Song, Huiqun Yu |
| 1998 | Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification. | John M. Rushby |