| 2007 | Testing conformance on Stochastic Stream X-Machines. | Mercedes G. Merayo, Manuel Nez |
| 2007 | Supporting Proof in a Reactive Development Environment. | Farhad Mehta |
| 2007 | Verification of Object Relational Maps. | Krishna K. Mehra, Sriram K. Rajamani, A. Prasad Sistla, Sumit Kumar Jha |
| 2007 | Formal Specification using Interaction Diagrams. | Kevin Lano |
| 2007 | Disciplining Orchestration and Conversation in Service-Oriented Computing. | Ivan Lanese, Francisco Martins, Vasco Thudichum Vasconcelos, Antnio Ravara |
| 2007 | Recovery from DoS Attacks in MIPv6: Modeling and Validation. | Manish C. Kumar, K. Gopinath |
| 2007 | Specification-based testing for refinement. | Temesghen Kahsai, Markus Roggenbach, Bernd-Holger Schlingloff |
| 2007 | Sound reasoning about unchecked exceptions. | Bart Jacobs, Peter Mller, Frank Piessens |
| 2007 | Specialising in Software Engineering. | Michael Jackson |
| 2007 | Flexible Behavioural Compatibility and Substitutability for Component Protocols: A Formal Specification. | Nabil Hameurlain |
| 2007 | Problem Oriented Software Engineering: A design-theoretic framework for software engineering. | Jon G. Hall, Lucia Rapanotti, Michael Jackson |
| 2007 | ASN1-light: A Verified Message Encoding for Security Protocols. | Holger Grandy, Robert Bertossi, Kurt Stenzel, Wolfgang Reif |
| 2007 | Configurable Proof Obligations in the Frog Toolkit. | Simon Fraser, Richard Banach |
| 2007 | Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. | Xianghua Deng, Robby, John Hatcliff |
| 2007 | A Thread-tag Based Semantics for Sequence Diagrams. | Haitao Dan, Robert M. Hierons, Steve Counsell |
| 2007 | Verification of C Programs Using Automated Reasoning. | David Crocker, Judith Carlton |
| 2007 | The Rle of Abstract Interpretation in Formal Methods. | Patrick Cousot |
| 2007 | Automatically Proving Concurrent Programs Correct. | Byron Cook |
| 2007 | A Scalable Lock-Free Stack Algorithm and its Verification. | Robert Colvin, Lindsay Groves |
| 2007 | An ought-to-do deontic logic for reasoning about fault-tolerance: the diarrheic philosophers. | Pablo F. Castro, T. S. E. Maibaum |
| 2007 | Formal verification of tamper-evident storage for e-voting. | Dominique Cansell, J. Paul Gibson, Dominique Mry |
| 2007 | Run-time Composition and Adaptation of Mismatching Behavioural Transactions. | Javier Cmara, Gwen Salan, Carlos Canal |
| 2007 | Model-driven architecture for cancer research. | Radu Calinescu, Steve Harris, Jeremy Gibbons, Jim Davies, Igor Toujilov, Sylvia B. Nagl |
| 2007 | An Integrated Specification Framework for Embedded Systems. | Marius C. Bujorianu, Manuela-Luminita Bujorianu |
| 2007 | A Dynamic Logic for Deductive Verification of Concurrent Programs. | Bernhard Beckert, Vladimir Klebanov |