FM 2009: Formal Methods

Invited Papers.- Formal Methods for Privacy.- What Can Formal Methods Bring to Systems Biology?.- Guess and Verify - Back to the Future.- Verification, Testing and Statistics.- Security, Probability and Nearly Fair Coins in the Cryptographers' Café.- Model Checking I.- Recursive Abstractions for Parameterized Systems.- Abstract Model Checking without Computing the Abstraction.- Three-Valued Spotlight Abstractions.- Fair Model Checking with Process Counter Abstraction.- Compositionality.- Systematic Development of Trustworthy Component Systems.- Partial Order Reductions Using Compositional Confluence Detection.- A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition.- Verification.- Abstract Specification of the UBIFS File System for Flash Memory.- Inferring Mealy Machines.- Formal Management of CAD/CAM Processes.- Concurrency.- Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way.- Symbolic Predictive Analysis for Concurrent Programs.- On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study.- Refinement.- Sums and Lovers: Case Studies in Security, Compositionality and Refinement.- Iterative Refinement of Reverse-Engineered Models by Model-Based Testing.- Model Checking Linearizability via Refinement.- Static Analysis.- It's Doomed; We Can Prove It.- "Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis.- Field-Sensitive Value Analysis by Field-Insensitive Analysis.- Theorem Proving.- Making Temporal Logic Calculational: A Tool for Unification and Discovery.- A Tableau for CTL*.- Certifiable Specification and Verification of C Programs.- Formal Reasoning about Expectation Properties for Continuous Random Variables.- Semantics.-The Denotational Semantics of slotted-Circus.- Unifying Probability with Nondeterminism.- Towards an Operational Semantics for Alloy.- A Robust Semantics Hides Fewer Errors.- Special Track: Industrial Applications I.- Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks.- Formal Verification of Avionics Software Products.- Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.- Object-Orientation.- Connecting UML and VDM++ with Open Tool Support.- Language and Tool Support for Class and State Machine Refinement in UML-B.- Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects.- Abstract Object Creation in Dynamic Logic.- Pointers.- Reasoning about Memory Layouts.- A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis.- Real-Time.- On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery.- Verifying Real-Time Systems against Scenario-Based Requirements.- Special Track: Tools and Industrial Applications II.- Formal Specification of a Cardiac Pacing System.- Automated Property Verification for Large Scale B Models.- Reduced Execution Semantics of MPI: From Theory to Practice.- Model Checking II.- A Metric Encoding for Bounded Model Checking.- An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method.- Verifying Information Flow Control over Unbounded Processes.- Specification and Verification of Web Applications in Rewriting Logic.- Industry-Day Abstracts.- Verifying the Microsoft Hyper-V Hypervisor with VCC.- Industrial Practice in Formal Methods: A Review.- Model-Based GUI Testing Using Uppaal at Novo Nordisk.