FM 2006: Hamilton, Canada

Jayadev Misra, Tobias Nipkow, Emil Sekerinski (Eds.): FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings. Lecture Notes in Computer Science 4085 Springer 2006, ISBN 3-540-37215-6

Invited Talk

Thomas A. Henzinger, Joseph Sifakis:
The Embedded Systems Design Challenge. 1-15

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif:
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. 16-31
Jonathan Schmitt, Alwin Hoffmann, Michael Balser, Wolfgang Reif, Mar Marcos:
Interactive Verification of Medical Guidelines. 32-47
David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
Certifying Airport Security Regulations Using the Focal Environment. 48-63
Shinya Umeno, Nancy A. Lynch:
Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study. 64-80

Kim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasowski:
Interface Input/Output Automata. 82-97
Greg Brunet, Marsha Chechik, Sebastián Uchitel:
Properties of Behavioural Model Merging. 98-114
Angela Freitas, Ana Cavalcanti:
Automatic Translation from Circus to Java. 115-130
Annabelle McIver:
Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems. 131-146

Marcel Verhoef, Peter Gorm Larsen, Jozef Hooman:
Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. 147-162
Jewgenij Botaschanjan, Alexander Gruler, Alexander Harhurin, Leonid Kof, Maria Spichkova, David Trachtenherz:
Towards Modularized Verification of Distributed Time-Triggered Systems. 163-178

Stefano Bacherini, Alessandro Fantechi, Matteo Tempestini, Niccolò Zingoni:
A Story About Formal Methods Adoption by a Railway Signaling Manufacturer. 179-189
Yujun Zheng, Jinquan Wang, Kan Wang, Jinyun Xue:
Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven Approach. 190-204

Tim McComb, Graeme Smith:
Compositional Class Refinement in Object-Z. 205-220
Neil Evans, Michael J. Butler:
A Proposal for Records in Event-B. 221-235
José Nuno Oliveira, César Jesus Rodrigues:
Pointfree Factorization of Operation Refinement. 236-251
Nuno Amálio, Susan Stepney, Fiona Polack:
A Formal Template Language Enabling Metaproof. 252-267

Ioannis T. Kassios:
Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. 268-283
Alcino Cunha, José Nuno Oliveira, Joost Visser:
Type-Safe Two-Level Data Transformation. 284-299

Raymond T. Boute:
Using Domain-Independent Problems for Introducing Formal Methods. 316-331

Pamela Zave:
Compositional Binding in Network Domains. 332-347
Zarrin Langari, Richard J. Trefler:
Formal Modeling of Communication Protocols by Graph Transformation. 348-363
Marc Aiguier, Karim Berkani, Pascale Le Gall:
Feature Specification and Static Analysis for Interaction Resolution. 364-379
Mass Soldal Lund, Ketil Stølen:
A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice. 380-395

Xin Li, H. James Hoover, Piotr Rudnicki:
Towards Automatic Exception Safety Verification. 396-411
Cyrille Artho, Armin Biere, Shinichi Honiden:
Enforcer - Efficient Failure Injection. 412-427
Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard:
Automated Boundary Test Generation from JML Specifications. 428-443
Wojciech Mostowski:
Formal Reasoning About Non-atomic Java Card Methods in Dynamic Logic. 444-459

Sandrine Blazy, Zaynah Dargaye, Xavier Leroy:
Formal Verification of a C Compiler Front-End. 460-475
Thuan Quang Huynh, Abhik Roychoudhury:
A Memory Model Sensitive Checker for C#. 476-491
Fabian Bannwart, Peter Müller:
Changing Programs Correctly: Refactoring with Specifications. 492-507
Viorel Preoteasa:
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. 508-523

Wendy Johnston, Kirsten Winter, Lionel van den Berg, Paul A. Strooper, Peter Robinson:
Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking. 524-540
Alastair F. Donaldson, Alice Miller:
Exact and Approximate Strategies for Symmetry Reduction in Model Checking. 541-556
Alexandre Genon, Thierry Massart, Cédric Meuter:
Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces. 557-572
Amir Pnueli, Aleksandr Zaks:
PSL Model Checking and Run-Time Verification Via Testers. 573-586

Werner Stephan:
Formal Methods for Security: Lightweight Plug-In or New Engineering Discipline. 587-591
David von Oheimb:
Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche. 592-597
Dusko Pavlovic:
Connector-Based Software Development: Deriving Secure Protocols. 598-599
Jan Jürjens:
Model-Based Security Engineering for Real. 600-606
D. Randolph Johnson:
Cost Effective Software Engineering for Security. 607-611
Michael Backes, Birgit Pfitzmann, Michael Waidner:
Formal Methods and Cryptography. 612-616
Jim Woodcock:
Verified Software Grand Challenge. 617-617