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 |