| 2004 | A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models. Ana Fernández Vilas, José Juan Pazos-Arias, Rebeca P. Díaz Redondo, Alberto Gil-Solla, Jorge García Duque |
| 2004 | A Method for Compiling and Executing Expressive Assertions. Francisco José Galán Morillo, José Miguel Cañete Valdeón |
| 2004 | A Tutorial Introduction to Designs in Unifying Theories of Programming. Jim Woodcock, Ana Cavalcanti |
| 2004 | An Integration of Program Analysis and Automated Theorem Proving. Bill J. Ellis, Andrew Ireland |
| 2004 | An Optimal Approach to Hardware/Software Partitioning for Synchronous Model. Geguang Pu, Dang Van Hung, Jifeng He, Wang Yi |
| 2004 | Constituent Elements of a Correctness-Preserving UML Design Approach. Tiberiu Seceleanu, Juha Plosila |
| 2004 | Design Verification for Control Engineering. Richard J. Boulton, Hanne Gottliebsen, Ruth Hardy, Tom W. Kelsey, Ursula Martin |
| 2004 | Efficient CSP Adalberto Farias, Alexandre Mota, Augusto Sampaio |
| 2004 | Embeddings of Hybrid Automata in Process Algebra. Tim A. C. Willemse |
| 2004 | Formalising Behaviour Trees with CSP. Kirsten Winter |
| 2004 | Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors. Paul Curzon, Ann Blandford |
| 2004 | Generating MSCs from an Integrated Formal Specification Language. Jin Song Dong, Shengchao Qin, Jun Sun |
| 2004 | Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings Eerke A. Boiten, John Derrick, Graeme Smith |
| 2004 | Integrating Formal Methods by Unifying Abstractions. Raymond T. Boute |
| 2004 | Integrating Model Checking and Theorem Proving in a Reflective Functional Language. Thomas F. Melham |
| 2004 | Integrating Temporal Logics. Yifeng Chen, Zhiming Liu |
| 2004 | Integration of Specification Languages Using Viewpoints. Marius C. Bujorianu |
| 2004 | Linking CSP-OZ with UML and Java: A Case Study. Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim |
| 2004 | Object-Oriented Modelling with High-Level Modular Petri Nets. Cécile Bui Thanh, Hanna Klaudel |
| 2004 | Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption. Xu Wang, A. W. Roscoe, Ranko Lazic |
| 2004 | SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani |
| 2004 | Software Verification with Integrated Data Type Refinement for Integer Arithmetic. Bernhard Beckert, Steffen Schlager |
| 2004 | Specification and Verification of Synchronizing Concurrent Objects. Gabriel Ciobanu, Dorel Lucanu |
| 2004 | State/Event-Based Software Model Checking. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha |
| 2004 | UML to B: Formal Verification of Object-Oriented Models. Kevin Lano, David Clark, Kelly Androutsopoulos |
| 2004 | Understanding Object-Z Operations as Generalised Substitutions. Steve Dunne |
| 2004 | Using UML Sequence Diagrams as the Basis for a Formal Test Description Language. Simon Pickin, Jean-Marc Jézéquel |
| 2004 | Verifying Controlled Components. Steve A. Schneider, Helen Treharne |
| 2004 | Viewpoint-Based Testing of Concurrent Components. Luke Wildman, Roger Duke, Paul A. Strooper |