| Invited Talk | |
| The Embedded Systems Design Challenge | p. 1 |
| Interactive Verification | |
| The Mondex Challenge: Machine Checked Proofs for an Electronic Purse | p. 16 |
| Interactive Verification of Medical Guidelines | p. 32 |
| Certifying Airport Security Regulations Using the Focal Environment | p. 48 |
| Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study | p. 64 |
| Invited Talk | |
| Validating the Microsoft Hypervisor | p. 81 |
| Formal Modelling of Systems | |
| Interface Input/Output Automata | p. 82 |
| Properties of Behavioural Model Merging | p. 98 |
| Automatic Translation from Circus to Java | p. 115 |
| Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems | p. 131 |
| Real Time | |
| Modeling and Validating Distributed Embedded Real-Time Systems with VDM++ | p. 147 |
| Towards Modularized Verification of Distributed Time-Triggered Systems | p. 163 |
| Industrial Experience | |
| A Story About Formal Methods Adoption by a Railway Signaling Manufacturer | p. 179 |
| Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven Approach | p. 190 |
| Specification and Refinement | |
| Compositional Class Refinement in Object-Z | p. 205 |
| A Proposal for Records in Event-B | p. 221 |
| Pointfree Factorization of Operation Refinement | p. 236 |
| A Formal Template Language Enabling Metaproof | p. 252 |
| Programming Languages | |
| Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions (Best Paper) | p. 268 |
| Type-Safe Two-Level Data Transformation | p. 284 |
| Algebra | |
| Feature Algebra | p. 300 |
| Education | |
| Using Domain-Independent Problems for Introducing Formal Methods | p. 316 |
| Formal Modelling of Systems | |
| Compositional Binding in Network Domains | p. 332 |
| Formal Modeling of Communication Protocols by Graph Transformation | p. 348 |
| Feature Specification and Static Analysis for interaction Resolution | p. 364 |
| A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice | p. 380 |
| Formal Aspects of Java | |
| Towards Automatic Exception Safety Verification | p. 396 |
| Enforcer - Efficient Failure Injection | p. 412 |
| Automated Boundary Test Generation from JML Specifications | p. 428 |
| Formal Reasoning About Non-atomic Java Card Methods in Dynamic Logic | p. 444 |
| Programming Languages | |
| Formal Verification of a C Compiler Front-End | p. 460 |
| A Memory Model Sensitive Checker for C# | p. 476 |
| Changing Programs Correctly: Refactoring with Specifications | p. 492 |
| Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic | p. 508 |
| Model Checking | |
| Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking | p. 524 |
| Exact and Approximate Strategies for Symmetry Reduction in Model Checking | p. 541 |
| Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces | p. 557 |
| PSL Model Checking and Run-Time Verification Via Testers | p. 573 |
| Industry Day: Abstracts of Invited Talks | |
| Formal Methods for Security: Lightweight Plug-In or New Engineering Discipline | p. 587 |
| Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche | p. 592 |
| Connector-Based Software Development: Deriving Secure Protocols | p. 598 |
| Model-Based Security Engineering for Real | p. 600 |
| Cost Effective Software Engineering for Security | p. 607 |
| Formal Methods and Cryptography | p. 612 |
| Verified Software Grand Challenge | p. 617 |
| Author Index | p. 619 |
| Table of Contents provided by Ingram. All Rights Reserved. |