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