| 2001 | Composing Contracts: An Adventure in Financial Engineering. | Simon L. Peyton Jones |
| 2001 | View Updatability Based on the Models of a Formal Specification. | Michael Johnson, Robert D. Rosebrugh |
| 2001 | Lightweight Formal Methods. | Daniel Jackson |
| 2001 | From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study. | Manuel J. Fernndez-Iglesias, Francisco J. Gonzlez-Castao, Jos M. Pousada Carballo, Martn Llamas Nistal, Alberto Romero Feijoo |
| 2001 | Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries. | Steffen Helke, Thomas Santen |
| 2001 | Transacted Memory for Smart Cards. | Pieter H. Hartel, Michael J. Butler, Eduard de Jong, Mark Longley |
| 2001 | A Formal Model of Object-Oriented Design and GoF Design Patterns. | Andres Flores, Richard Moore, Luis Reynoso |
| 2001 | Houdini, an Annotation Assistant for ESC/Java. | Cormac Flanagan, K. Rustan M. Leino |
| 2001 | Validation of UML Models Thanks to Z and Lustre. | Sophie Dupuy-Chessa, Lydie du Bousquet |
| 2001 | A Modular Approach to the Specification and Validation of an Electrical Flight Control System. | Marielle Doche, Isabelle Vernier-Mounier, Fabrice Kordon |
| 2001 | Avoiding State Explosion for Distributed Systems with Timestamps. | Fabrice Derepas, Paul Gastin, David Plainfoss |
| 2001 | Model-Checking over Multi-valued Logics. | Marsha Chechik, Steve M. Easterbrook, Victor Petrovykh |
| 2001 | An Adequate Logic for Full LOTOS. | Muffy Calder, Savi Maharaj, Carron Shankland |
| 2001 | Verifying Implementation Relations. | Jonathan Burton, Maciej Koutny, Giuseppe Pappalardo |
| 2001 | A Heuristic for Symmetry Reductions with Scalarsets. | Dragan Bosnacki, Dennis Dams, Leszek Holenderski |
| 2001 | Improvements in BDD-Based Reachability Analysis of Timed Automata. | Dirk Beyer |
| 2001 | Reformulation: A Way to Combine Dynamic Properties and B Refinement. | Franoise Bellegarde, Christophe Darlot, Jacques Julliand, Olga Kouchnarenko |
| 2001 | Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP System. | Laurent Arditi, Hdi Boufaed, Arnaud Cavani, Vincent Stehl |
| 2001 | A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures. | Vangalur S. Alagar, Zheng Xi |
| 2001 | Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics. | Mchel Mac an Airchinnigh |
| 2001 | Test-Case Calculation through Abstraction. | Bernhard K. Aichernig |
| 1999 | Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol. | Dan Zhou, Shiu-Kai Chin |
| 1999 | An Operational Semantics for Timed RAISE. | Xia Yong, Chris George |
| 1999 | Formal Modeling in a Commercial Setting: A Case Study. | Andre Wong, Marsha Chechik |
| 1999 | Data Abstraction for CSP-OZ. | Heike Wehrheim |