| 2004 | Glass-Box and Black-Box Views on Object-Oriented Specifications. | Michel Bidoit, Rolf Hennicker, Alexander Knapp, Hubert Baumeister |
| 2004 | Test Case Generation Using Stochastic Automata Networks: Quantitative Analysis. | Cristiano Bertolini, Andr G. Farina, Paulo Fernandes, Flvio Moreira Oliveira |
| 2004 | Random Testing in Isabelle/HOL. | Stefan Berghofer, Tobias Nipkow |
| 2004 | Proof Reuse for Deductive Program Verification. | Bernhard Beckert, Vladimir Klebanov |
| 2004 | Property-Driven Development. | Hubert Baumeister, Alexander Knapp, Martin Wirsing |
| 2004 | Models and Temporal Logics for Timed Component Connectors. | Farhad Arbab, Christel Baier, Frank S. de Boer, Jan J. M. M. Rutten |
| 2003 | Facilitating Program Verification with Dependent Types. | Hongwei Xi |
| 2003 | A Partial-Correctness Semantics for Modelling Assembler Programs. | Geoffrey Watson, Colin J. Fidge |
| 2003 | Architecting Specifications for Test Case Generation. | Richard O. Sinnott |
| 2003 | Model Checking Visual Specification of Requirements. | Ulka Shrotri, Purandar Bhaduri, R. Venkatesh |
| 2003 | Taming Mobile Processes Using Types. | Davide Sangiorgi |
| 2003 | Towards Formalizing UML State Diagrams in CSP. | Muan Yong Ng, Michael J. Butler |
| 2003 | Supporting the Software Testing Process through Specification Animation. | Tim Miller, Paul A. Strooper |
| 2003 | Animation of Object-Z Specifications Using a Z Animator. | Tim McComb, Graeme Smith |
| 2003 | Behavioral Consistency Validation of UML Diagrams. | Boris Litvak, Shmuel S. Tyszberowicz, Amiram Yehudai |
| 2003 | Weak Bisimulation for Probabilistic Timed Automata and Applications to Security. | Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina |
| 2003 | Component-Based Design and Analysis: A Case Study. | Yan Jin, Charles Lakos, Robert Esser |
| 2003 | Semantic Properties of mu-Charts. | Doug Goldson, Greg Reeve |
| 2003 | Formal Verification of ASM Designs Using the MDG Tool. | Amjad Gawanmeh, Sofine Tahar, Kirsten Winter |
| 2003 | Specification Matching of Object-Oriented Components. | Frank Feiks, David Hemer |
| 2003 | Modelling Java Concurrency with Object-Z. | Roger Duke, Luke Wildman, Brad Long |
| 2003 | From Requirements to Design: Formalizing the Key Steps. | R. Geoff Dromey |
| 2003 | Light-Weight Theorem Proving for Debugging and Verifying Units of Code. | David Dharbe, Silvio Ranise |
| 2003 | A Formal Model for Trust in Dynamic Networks. | Marco Carbone, Mogens Nielsen, Vladimiro Sassone |
| 2003 | Formalizing the Framework Design Language F-UML. | Nadia Bouassida, Hanne Ben-Abdallah, Faez Gargouri, Abdelmajid Ben Hamadou |