| 2003 | Compilation by Refinement for a Practical Assembly Language. | Geoffrey Watson |
| 2003 | Java Card Code Generation from B Specifications. | Bruno Tatibout, Antoine Requet, Jean-Christophe Voisinet, Ahmed Hammad |
| 2003 | An AMBA-ARM7 Formal Verification Platform. | Kong Woei Susanto, Thomas F. Melham |
| 2003 | A Calculus for Set-Based Program Development. | Georg Struth |
| 2003 | Formalization, Testing and Execution of a Use Case Diagram. | Wuwei Shen, Shaoying Liu |
| 2003 | Service-Based Systems Engineering: Consistent Combination of Services. | Bernhard Schtz, Christian Salzmann |
| 2003 | Constraint-Based Model Checking of Data-Independent Systems. | Beata Sarna-Starosta, C. R. Ramakrishnan |
| 2003 | Formalising an Integrated Language in PVS. | Gwen Salan, J. Christian Attiogb |
| 2003 | Incremental Derivation of Abstraction Relations for Data Refinement. | Neil J. Robinson |
| 2003 | Comparison of Data and Process Refinement. | Steve Reeves, David Streader |
| 2003 | Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow Language. | Sanjai Rayadurgam, Anjali Joshi, Mats Per Erik Heimdahl |
| 2003 | Formal Development of a Distributed Logging Mechanism Supporting Disconnected Updates. | Yuechen Qian |
| 2003 | Compositional Verification of a Switch Fabric from Nortel Networks. | Hong Peng, Sofine Tahar, Yassine Mokhtari |
| 2003 | Analyzing the Redesign of a Distributed Lift System in UPPAAL. | Jun Pang, Bart Karstens, Wan J. Fokkink |
| 2003 | Generic Interacting State Machines and Their Instantiation with Dynamic Features. | David von Oheimb, Volkmar Lotz |
| 2003 | Model Based Code Verification. | Colin O'Halloran |
| 2003 | Adding Action Refinement to Stochastic True Concurrency Models. | Mila E. Majster-Cederbaum, Jinzhao Wu |
| 2003 | The Equivalence of Statecharts. | Quan Long, Zongyan Qiu, Shengchao Qin |
| 2003 | A Z Based Approach to Verifying Security Protocols. | Benjamin W. Long, Colin J. Fidge, Antonio Cerone |
| 2003 | A Relational Model for Formal Object-Oriented Requirement Analysis in UML. | Zhiming Liu, Jifeng He, Xiaoshan Li, Yifeng Chen |
| 2003 | Efficient Path Finding with the Sweep-Line Method Using External Storage. | Lars Michael Kristensen, Thomas Mailund |
| 2003 | Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures. | Mickal Kerboeuf, David Nowak, Jean-Pierre Talpin |
| 2003 | Adding Formalism to Methods or | Mathai Joseph |
| 2003 | Programs as Paths: An Approach to Timing Constraint Analysis. | Ian J. Hayes |
| 2003 | A Refinement Tool for Z. | Angela F. Freitas, Carla Nascimento, Ana Cavalcanti |