FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings

Front Matter....Pages -
Formal Methods for Privacy....Pages 1-15
What Can Formal Methods Bring to Systems Biology?....Pages 16-22
Guess and Verify – Back to the Future....Pages 23-32
Verification, Testing and Statistics....Pages 33-40
Security, Probability and Nearly Fair Coins in the Cryptographers’ Café....Pages 41-71
Recursive Abstractions for Parameterized Systems....Pages 72-88
Abstract Model Checking without Computing the Abstraction....Pages 89-105
Three-Valued Spotlight Abstractions....Pages 106-122
Fair Model Checking with Process Counter Abstraction....Pages 123-139
Systematic Development of Trustworthy Component Systems....Pages 140-156
Partial Order Reductions Using Compositional Confluence Detection....Pages 157-172
A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition....Pages 173-189
Abstract Specification of the UBIFS File System for Flash Memory....Pages 190-206
Inferring Mealy Machines....Pages 207-222
Formal Management of CAD/CAM Processes....Pages 223-238
Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way....Pages 239-255
Symbolic Predictive Analysis for Concurrent Programs....Pages 256-272
On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study....Pages 273-288
 Sums and Lovers: Case Studies in Security, Compositionality and Refinement....Pages 289-304
Iterative Refinement of Reverse-Engineered Models by Model-Based Testing....Pages 305-320
Model Checking Linearizability via Refinement....Pages 321-337
It’s Doomed; We Can Prove It....Pages 338-353
“Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis....Pages 354-369
Field-Sensitive Value Analysis by Field-Insensitive Analysis....Pages 370-386
Making Temporal Logic Calculational: A Tool for Unification and Discovery....Pages 387-402
A Tableau for CTL*....Pages 403-418
Certifiable Specification and Verification of C Programs....Pages 419-434
Formal Reasoning about Expectation Properties for Continuous Random Variables....Pages 435-450
The Denotational Semantics of slotted-Circus ....Pages 451-466
Unifying Probability with Nondeterminism....Pages 467-482
Towards an Operational Semantics for Alloy....Pages 483-498
A Robust Semantics Hides Fewer Errors....Pages 499-515
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks....Pages 516-531
Formal Verification of Avionics Software Products....Pages 532-546
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study....Pages 547-562
Connecting UML and VDM++ with Open Tool Support....Pages 563-578
Language and Tool Support for Class and State Machine Refinement in UML-B....Pages 579-595
Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects....Pages 596-611
Abstract Object Creation in Dynamic Logic....Pages 612-627
Reasoning about Memory Layouts....Pages 628-643
A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis....Pages 644-659
On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery....Pages 660-675
Verifying Real-Time Systems against Scenario-Based Requirements....Pages 676-691
Formal Specification of a Cardiac Pacing System....Pages 692-707
Automated Property Verification for Large Scale B Models....Pages 708-723
Reduced Execution Semantics of MPI: From Theory to Practice....Pages 724-740
A Metric Encoding for Bounded Model Checking....Pages 741-756
An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method....Pages 757-772
Verifying Information Flow Control over Unbounded Processes....Pages 773-789
Specification and Verification of Web Applications in Rewriting Logic....Pages 790-805
Verifying the Microsoft Hyper-V Hypervisor with VCC....Pages 806-809
Industrial Practice in Formal Methods: A Review....Pages 810-813
Model-Based GUI Testing Using Uppaal   at Novo Nordisk....Pages 814-818
Back Matter....Pages -