| 2003 | A General Approach to Deadlock Freedom Verification for Software Architectures. | Alessandro Aldini, Marco Bernardo |
| 2003 | Event Based Sequential Program Development: Application to Constructing a Pointer Program. | Jean-Raymond Abrial |
| 2002 | A Formal Basis for a Program Compilation Proof Tool. | Luke Wildman |
| 2002 | Synthesizing Certified Code. | Michael W. Whalen, Johann Schumann, Bernd Fischer |
| 2002 | A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization Channels. | Takaaki Umedu, Yoshiki Terashima, Keiichi Yasumoto, Akio Nakata, Teruo Higashino, Kenichi Taniguchi |
| 2002 | Supplementing a UML Development Process with B. | Helen Treharne |
| 2002 | Little Engines of Proof. | Natarajan Shankar |
| 2002 | Refinement in Circus. | Augusto Sampaio, Jim Woodcock, Ana Cavalcanti |
| 2002 | Verification Using Test Generation Techniques. | Vlad Rusu |
| 2002 | Improvements in Coverability Analysis. | Gil Ratsaby, Baruch Sterin, Shmuel Ur |
| 2002 | Interference Analysis for Dependable Systems Using Refinement and Abstraction. | Claus Pahl |
| 2002 | Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. | David von Oheimb, Tobias Nipkow |
| 2002 | Mechanical Abstraction of CSP | Alexandre Mota, Paulo Borba, Augusto Sampaio |
| 2002 | VAlloy - Virtual Functions Meet a Relational Language. | Darko Marinov, Sarfraz Khurshid |
| 2002 | Automated Boundary Testing from Z and B. | Bruno Legeard, Fabien Peureux, Mark Utting |
| 2002 | A Generalised Sweep-Line Method for Safety Properties. | Lars Michael Kristensen, Thomas Mailund |
| 2002 | Safeness of Make-Based Incremental Recompilation. | Niels Jrgensen |
| 2002 | Closing Open SDL-Systems for Model Checking with DTSpin. | Natalia Ioustinova, Natalia Sidorova, Martin Steffen |
| 2002 | Towards an Integrated Model Checker for Railway Signalling Data. | Michael Huber, Steve King |
| 2002 | The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism. | Neil Henderson, Stephen Paynter |
| 2002 | Correctness by Construction: Integrating Formality into a Commercial Development Process. | Anthony Hall |
| 2002 | On Combining Functional Verification and Performance Evaluation Using CADP. | Hubert Garavel, Holger Hermanns |
| 2002 | Property Dependent Abstraction of Control Structure for Software Verification. | Thomas Firley, Ursula Goltz |
| 2002 | Timing Analysis of Assembler Code Control-Flow Paths. | Colin J. Fidge |
| 2002 | Semantic Web for Extending and Linking Formalisms. | Jin Song Dong, Jing Sun, Hai H. Wang |