default search action
FM 2006: Hamilton, Canada
- Jayadev Misra, Tobias Nipkow, Emil Sekerinski:
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
Interactive Verification
- 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
Invited Talk
- Ernie Cohen:
Validating the Microsoft Hypervisor. 81-81
Formal Modelling of Systems
- 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 F. 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
Real Time
- 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
Industrial Experience
- 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
Specification and Refinement
- 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
Programming Languages
- 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
Algebra
- Peter Höfner, Ridha Khédri, Bernhard Möller:
Feature Algebra. 300-315
Education
- Raymond T. Boute:
Using Domain-Independent Problems for Introducing Formal Methods. 316-331
Formal Modelling of Systems
- 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
Formal Aspects of Java
- 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
Programming Languages
- 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
Model Checking
- Wendy Johnston, Kirsten Winter, Lionel van den Berg, Paul A. Strooper, Peter J. 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
Industry Day: Abstracts of Invited Talks
- 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.