| Invited Talk |
| The Embedded Systems Design Challenge / Thomas A. Henzinger ; Joseph Sifakis |
| Interactive Verification |
| The Mondex Challenge: Machine Checked Proofs for an Electronic Purse / Gerhard Schellhorn ; Holger Grandy ; Dominik Haneberg ; Wolfgang Reif |
| Interactive Verification of Medical Guidelines / Jonathan Schmitt ; Alwin Hoffmann ; Michael Balser ; Mar Marcos |
| Certifying Airport Security Regulations Using the Focal Environment / David Delahaye ; Jean-Frederic Etienne ; Veronique Viguie Donzeau-Gouge |
| Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study / Shinya Umeno ; Nancy Lynch |
| Validating the Microsoft Hypervisor / Ernie Cohen |
| Formal Modelling of Systems |
| Interface Input/Output Automata / Kim G. Larsen ; Ulrik Nyman ; Andrzej Wasowski |
| Properties of Behavioural Model Merging / Greg Brunet ; Marsha Chechik ; Sebastian Uchitel |
| Automatic Translation from Circus to Java / Angela Freitas ; Ana Lucia Caneca Cavalcanti |
| Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems / Annabelle K. McIver |
| Real Time |
| Modeling and Validating Distributed Embedded Real-Time Systems with VDM++ / Marcel Verhoef ; Peter Gorm Larsen ; Jozef Hooman |
| Towards Modularized Verification of Distributed Time-Triggered Systems / Jewgenij Botaschanjan ; Alexander Gruler ; Alexander Harhurin ; Leonid Kof ; Maria Spichkova ; David Trachtenherz |
| Industrial Experience |
| A Story About Formal Methods Adoption by a Railway Signaling Manufacturer / Stefano Bacherini ; Alessandro Fantechi ; Matteo Tempestini ; Niccolo Zingoni |
| Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven Approach / Yujun Zheng ; Jinquan Wang ; Kan Wang ; Jinyun Xue |
| Specification and Refinement |
| Compositional Class Refinement in Object-Z / Tim McComb ; Graeme Smith |
| A Proposal for Records in Event-B / Neil Evans ; Michael Butler |
| Pointfree Factorization of Operation Refinement / Jose Nuno Oliveira ; Cesar Jesus Rodrigues |
| A Formal Template Language Enabling Metaproof / Nuno Amalio ; Susan Stepney ; Fiona Polack |
| Programming Languages |
| Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions (Best Paper) / Ioannis T. Kassios |
| Type-Safe Two-Level Data Transformation / Alcino Cunha ; Joost Visser |
| Algebra |
| Feature Algebra / Peter Hofner ; Ridha Khedri ; Bernhard Moller |
| Education |
| Using Domain-Independent Problems for Introducing Formal Methods / Raymond Boute |
| Compositional Binding in Network Domains / Pamela Zave |
| Formal Modeling of Communication Protocols by Graph Transformation / Zarrin Langari ; Richard Trefler |
| Feature Specification and Static Analysis for interaction Resolution / Marc Aiguier ; Karim Berkani ; Pascale Le Gall |
| A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice / Mass Soldal Lund ; Ketil Stolen |
| Formal Aspects of Java |
| Towards Automatic Exception Safety Verification / Xin Li ; H. James Hoover ; Piotr Rudnicki |
| Enforcer - Efficient Failure Injection / Cyrille Valentin Artho ; Armin Biere ; Shinichi Honiden |
| Automated Boundary Test Generation from JML Specifications / Fabrice Bouquet ; Frederic Dadeau ; Bruno Legeard |
| Formal Reasoning About Non-atomic Java Card Methods in Dynamic Logic / Wojciech Mostowski |
| Formal Verification of a C Compiler Front-End / Sandrine Blazy ; Zaynah Dargaye ; Xavier Leroy |
| A Memory Model Sensitive Checker for C# / Thuan Quang Huynh ; Abhik Roychoudhury |
| Changing Programs Correctly: Refactoring with Specifications / Fabian Bannwart ; Peter Muller |
| Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic / Viorel Preoteasa |
| Model Checking |
| Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking / Wendy Johnston ; Kirsten Winter ; Lionel van den Berg ; Paul Strooper ; Peter Robinson |
| Exact and Approximate Strategies for Symmetry Reduction in Model Checking / Alastair F. Donaldson ; Alice Miller |
| Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces / Alexandre Genon ; Thierry Massart ; Cedric Meuter |
| PSL Model Checking and Run-Time Verification Via Testers / Amir Pnueli ; Aleksandr Zaks |
| Industry Day: Abstracts of Invited Talks |
| Formal Methods for Security: Lightweight Plug-In or New Engineering Discipline / Werner Stephan |
| Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche / David von Oheimb |
| Connector-Based Software Development: Deriving Secure Protocols / Dusko Pavlovic |
| Model-Based Security Engineering for Real / Jan Jurjens |
| Cost Effective Software Engineering for Security / D. Randolph Johnson |
| Formal Methods and Cryptography / Michael Backes ; Birgit Pfitzmann ; Michael Waidner |
| Verified Software Grand Challenge / Jim Woodcock |
| Author Index |
| Invited Talk |
| The Embedded Systems Design Challenge / Thomas A. Henzinger ; Joseph Sifakis |
| Interactive Verification |
| The Mondex Challenge: Machine Checked Proofs for an Electronic Purse / Gerhard Schellhorn ; Holger Grandy ; Dominik Haneberg ; Wolfgang Reif |
| Interactive Verification of Medical Guidelines / Jonathan Schmitt ; Alwin Hoffmann ; Michael Balser ; Mar Marcos |
| Certifying Airport Security Regulations Using the Focal Environment / David Delahaye ; Jean-Frederic Etienne ; Veronique Viguie Donzeau-Gouge |
