| 2003 | Refinement and Verification of Synchronized Component-Based Systems. | Olga Kouchnarenko, Arnaud Lanoix |
| 2003 | Looking Back to the Future: Thoughts on Paradigm Shift in Software Development. | Kouichi Kishida |
| 2003 | Trends in Software Verification. | Gerard J. Holzmann |
| 2003 | Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method. | Neil Henderson |
| 2003 | Determining the Specification of a Control System from That of Its Environment. | Ian J. Hayes, Michael A. Jackson, Cliff B. Jones |
| 2003 | Generating Counterexamples for Multi-valued Model-Checking. | Arie Gurfinkel, Marsha Chechik |
| 2003 | Watchdog Transformations for Property-Oriented Model-Checking. | Michael Goldsmith, Nick Moffat, Bill Roscoe, Tim Whitworth, Irfan Zakiuddin |
| 2003 | Program Checking with Certificates: Separating Correctness-Critical Code. | Sabine Glesner |
| 2003 | Taking | Marcelo F. Frias, Carlos Lpez Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum |
| 2003 | Verifying Emulation of Legacy Mission Computer Systems. | Colin J. Fidge |
| 2003 | Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach. | Pascal Fenkam, Harald C. Gall, Mehdi Jazayeri |
| 2003 | A Strategy for Compiling Classes, Inheritance, and Dynamic Binding. | Adolfo Duran, Ana Cavalcanti, Augusto Sampaio |
| 2003 | Checking and Reasoning about Semantic Web through Alloy. | Jin Song Dong, Jing Sun, Hai H. Wang |
| 2003 | Correctness of Source-Level Safety Policies. | Ewen Denney, Bernd Fischer |
| 2003 | Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle. | Daniele Compare, Paola Inverardi, Patrizio Pelliccione, Alessandra Sebastiani |
| 2003 | Composing Invariants. | Michel Charpentier |
| 2003 | Improving JML: For a Safer and More Effective Language. | Patrice Chalin |
| 2003 | Java Applet Correctness: A Developer-Oriented Approach. | Lilian Burdy, Antoine Requet, Jean-Louis Lanet |
| 2003 | Improving Safety Assessment of Complex Systems: An Industrial Case Study. | Marco Bozzano, Antonella Cavallo, Massimo Cifaldi, Laura Valacca, Adolfo Villafiorita |
| 2003 | Synthesis and Verification of Constraints in the PGM Protocol. | Marc Boyer, Mihaela Sighireanu |
| 2003 | Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case Study. | Fabrice Bouquet, Bruno Legeard |
| 2003 | Adaptable Translator of B Specifications to Embedded C Programs. | Didier Bert, Sylvain Boulm, Marie-Laure Potet, Antoine Requet, Laurent Voisin |
| 2003 | Team Automata Satisfying Compositionality. | Maurice H. ter Beek, Jetty Kleijn |
| 2003 | A Circus Semantics for Ravenscar Protected Objects. | Diyaa-Addein Atiya, Steve King, Jim Woodcock |
| 2003 | SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis. | Alessandro Armando, Luca Compagna, Pierre Ganty |