Abstract is missing.
- The Embedded Systems Design ChallengeThomas A. Henzinger, Joseph Sifakis. 1-15 [doi]
- The Mondex Challenge: Machine Checked Proofs for an Electronic PurseGerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif. 16-31 [doi]
- Interactive Verification of Medical GuidelinesJonathan Schmitt, Alwin Hoffmann, Michael Balser, Wolfgang Reif, Mar Marcos. 32-47 [doi]
- Certifying Airport Security Regulations Using the Focal EnvironmentDavid Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge. 48-63 [doi]
- Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case StudyShinya Umeno, Nancy A. Lynch. 64-80 [doi]
- Validating the Microsoft HypervisorErnie Cohen. 81-81 [doi]
- Interface Input/Output AutomataKim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasowski. 82-97 [doi]
- Properties of Behavioural Model MergingGreg Brunet, Marsha Chechik, Sebastián Uchitel. 98-114 [doi]
- Automatic Translation from ::::Circus:::: to JavaAngela Freitas, Ana Cavalcanti. 115-130 [doi]
- Quantitative Refinement ::::and:::: Model Checking for the Analysis of Probabilistic SystemsAnnabelle McIver. 131-146 [doi]
- Modeling and Validating Distributed Embedded Real-Time Systems with VDM++Marcel Verhoef, Peter Gorm Larsen, Jozef Hooman. 147-162 [doi]
- Towards Modularized Verification of Distributed Time-Triggered SystemsJewgenij Botaschanjan, Alexander Gruler, Alexander Harhurin, Leonid Kof, Maria Spichkova, David Trachtenherz. 163-178 [doi]
- A Story About Formal Methods Adoption by a Railway Signaling ManufacturerStefano Bacherini, Alessandro Fantechi, Matteo Tempestini, Niccolò Zingoni. 179-189 [doi]
- Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven ApproachYujun Zheng, Jinquan Wang, Kan Wang, Jinyun Xue. 190-204 [doi]
- Compositional Class Refinement in Object-ZTim McComb, Graeme Smith. 205-220 [doi]
- A Proposal for Records in Event-BNeil Evans, Michael J. Butler. 221-235 [doi]
- Pointfree Factorization of Operation RefinementJosé Nuno Oliveira, César Jesus Rodrigues. 236-251 [doi]
- A Formal Template Language Enabling MetaproofNuno Amálio, Susan Stepney, Fiona A. C. Polack. 252-267 [doi]
- Dynamic Frames: Support for Framing, Dependencies and Sharing Without RestrictionsIoannis T. Kassios. 268-283 [doi]
- Type-Safe Two-Level Data TransformationAlcino Cunha, José Nuno Oliveira, Joost Visser. 284-299 [doi]
- Feature AlgebraPeter Höfner, Ridha Khédri, Bernhard Möller. 300-315 [doi]
- Using Domain-Independent Problems for Introducing Formal MethodsRaymond T. Boute. 316-331 [doi]
- Compositional Binding in Network DomainsPamela Zave. 332-347 [doi]
- Formal Modeling of Communication Protocols by Graph TransformationZarrin Langari, Richard J. Trefler. 348-363 [doi]
- Feature Specification and Static Analysis for Interaction ResolutionMarc Aiguier, Karim Berkani, Pascale Le Gall. 364-379 [doi]
- A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory ChoiceMass Soldal Lund, Ketil Stølen. 380-395 [doi]
- Towards Automatic Exception Safety VerificationXin Li, H. James Hoover, Piotr Rudnicki. 396-411 [doi]
- Enforcer - Efficient Failure InjectionCyrille Artho, Armin Biere, Shinichi Honiden. 412-427 [doi]
- Automated Boundary Test Generation from JML SpecificationsFabrice Bouquet, Frédéric Dadeau, Bruno Legeard. 428-443 [doi]
- Formal Reasoning About Non-atomic Java Card Methods in Dynamic LogicWojciech Mostowski. 444-459 [doi]
- Formal Verification of a C Compiler Front-EndSandrine Blazy, Zaynah Dargaye, Xavier Leroy. 460-475 [doi]
- A Memory Model Sensitive Checker for C#Thuan Quang Huynh, Abhik Roychoudhury. 476-491 [doi]
- Changing Programs Correctly: Refactoring with SpecificationsFabian Bannwart, Peter Müller. 492-507 [doi]
- Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation LogicViorel Preoteasa. 508-523 [doi]
- Model-Based Variable and Transition Orderings for Efficient Symbolic Model CheckingWendy Johnston, Kirsten Winter, Lionel van den Berg, Paul A. Strooper, Peter Robinson. 524-540 [doi]
- Exact and Approximate Strategies for Symmetry Reduction in Model CheckingAlastair F. Donaldson, Alice Miller. 541-556 [doi]
- Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check TracesAlexandre Genon, Thierry Massart, Cédric Meuter. 557-572 [doi]
- PSL Model Checking and Run-Time Verification Via TestersAmir Pnueli, Aleksandr Zaks. 573-586 [doi]
- Formal Methods for Security: Lightweight Plug-In or New Engineering DisciplineWerner Stephan. 587-591 [doi]
- Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding NicheDavid von Oheimb. 592-597 [doi]
- Connector-Based Software Development: Deriving Secure ProtocolsDusko Pavlovic. 598-599 [doi]
- Model-Based Security Engineering for RealJan Jürjens. 600-606 [doi]
- Cost Effective Software Engineering for SecurityD. Randolph Johnson. 607-611 [doi]
- Formal Methods and CryptographyMichael Backes, Birgit Pfitzmann, Michael Waidner. 612-616 [doi]
- Verified Software Grand ChallengeJim Woodcock. 617-617 [doi]