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

This book presents the refereed proceedings of FM 2009, the 16th International Symposium on Formal Methods, held as the Second World Congress on Formal Methods in Eindhoven, The Netherlands, in November 2009 in the course of the first International Formal Methods Week, FMWeek 2009.

The 45 revised full papers presented together with 5 invited papers and 3 additional papers from the Industry Day were carefully reviewed and selected from 139 submissions. The papers are organized in topical sections on model checking, compositionality, verification, concurrency, refinement, static analysis, theorem proving, semantics, industrial applications, object-orientation, pointers, real-time, tools and industrial applications, and industry-day abstracts.

---

This book presents the refereed proceedings of FM 2009, the 16th International Symposium on Formal Methods, held as the Second World Congress on Formal Methods in Eindhoven, The Netherlands, in November 2009 in the course of the first International Formal Methods Week, FMWeek 2009.

The 45 revised full papers presented together with 5 invited papers and 3 additional papers from the Industry Day were carefully reviewed and selected from 139 submissions. The papers are organized in topical sections on model checking, compositionality, verification, concurrency, refinement, static analysis, theorem proving, semantics, industrial applications, object-orientation, pointers, real-time, tools and industrial applications, and industry-day abstracts.

---

This book presents the refereed proceedings of FM 2009, the 16th International Symposium on Formal Methods, held as the Second World Congress on Formal Methods in Eindhoven, The Netherlands, in November 2009 in the course of the first International Formal Methods Week, FMWeek 2009.

The 45 revised full papers presented together with 5 invited papers and 3 additional papers from the Industry Day were carefully reviewed and selected from 139 submissions. The papers are organized in topical sections on model checking, compositionality, verification, concurrency, refinement, static analysis, theorem proving, semantics, industrial applications, object-orientation, pointers, real-time, tools and industrial applications, and industry-day abstracts.

Content:
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
Iterative Refinement of Reverse-Engineered Models by Model-Based Testing....Pages 289-304
Model Checking Linearizability via Refinement....Pages 305-320
It’s Doomed; We Can Prove It....Pages 321-337
“Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis....Pages 338-353
Field-Sensitive Value Analysis by Field-Insensitive Analysis....Pages 354-369
Making Temporal Logic Calculational: A Tool for Unification and Discovery....Pages 370-386
A Tableau for CTL*....Pages 387-402
Certifiable Specification and Verification of C Programs....Pages 403-418
Formal Reasoning about Expectation Properties for Continuous Random Variables....Pages 419-434
Unifying Probability with Nondeterminism....Pages 435-450
Towards an Operational Semantics for Alloy....Pages 451-466
A Robust Semantics Hides Fewer Errors....Pages 467-482
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks....Pages 483-498
Formal Verification of Avionics Software Products....Pages 499-515
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study....Pages 516-531
Connecting UML and VDM++ with Open Tool Support....Pages 532-546
Language and Tool Support for Class and State Machine Refinement in UML-B....Pages 547-562
Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects....Pages 563-578
Abstract Object Creation in Dynamic Logic ....Pages 579-595
Reasoning about Memory Layouts....Pages 596-611
A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis....Pages 612-627
On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery....Pages 628-643
Verifying Real-Time Systems against Scenario-Based Requirements....Pages 644-659
Formal Specification of a Cardiac Pacing System....Pages 660-675
Automated Property Verification for Large Scale B Models....Pages 676-691
Reduced Execution Semantics of MPI: From Theory to Practice....Pages 692-707
A Metric Encoding for Bounded Model Checking....Pages 708-723
An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method....Pages 724-740
Verifying Information Flow Control over Unbounded Processes....Pages 741-756
Specification and Verification of Web Applications in Rewriting Logic....Pages 757-772
Verifying the Microsoft Hyper-V Hypervisor with VCC....Pages 773-789
Industrial Practice in Formal Methods: A Review....Pages 790-805
Model-Based GUI Testing Using Uppaal  at Novo Nordisk....Pages 806-809
Back Matter....Pages 810-813
....Pages 814-818