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.
Author(s): Michael Carl Tschantz, Jeannette M. Wing (auth.), Ana Cavalcanti, Dennis R. Dams (eds.)
Series: Lecture Notes in Computer Science 5850 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 820
Tags: Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Programming Techniques; Mathematical Logic and Formal Languages; Management of Computing and Information Systems
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 -
