FM 2009: Formal Methods

1. Front Matter

   PDF

2. Invited Papers

   1. Formal Methods for Privacy

      • Michael Carl Tschantz, Jeannette M. Wing

      Pages 1-15

   2. What Can Formal Methods Bring to Systems Biology?

      • Nicola Bonzanni, K. Anton Feenstra, Wan Fokkink, Elzbieta Krepska

      Pages 16-22

   3. Guess and Verify – Back to the Future

      • Colin O’Halloran

      Pages 23-32

   4. Verification, Testing and Statistics

      • Sriram K. Rajamani

      Pages 33-40

   5. Security, Probability and Nearly Fair Coins in the Cryptographers’ Café

      • Annabelle McIver, Larissa Meinicke, Carroll Morgan

      Pages 41-71

3. Model Checking I

   1. Recursive Abstractions for Parameterized Systems

      • Joxan Jaffar, Andrew E. Santosa

      Pages 72-88

   2. Abstract Model Checking without Computing the Abstraction

      • Stefano Tonetta

      Pages 89-105

   3. Three-Valued Spotlight Abstractions

      • Jonas Schrieb, Heike Wehrheim, Daniel Wonisch

      Pages 106-122

   4. Fair Model Checking with Process Counter Abstraction

      • Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong

      Pages 123-139

4. Compositionality

   1. Systematic Development of Trustworthy Component Systems

      • Rodrigo Ramos, Augusto Sampaio, Alexandre Mota

      Pages 140-156

   2. Partial Order Reductions Using Compositional Confluence Detection

      • Frédéric Lang, Radu Mateescu

      Pages 157-172

   3. A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition

      • Ralph Jeffords, Constance Heitmeyer, Myla Archer, Elizabeth Leonard

      Pages 173-189

5. Verification

   1. Abstract Specification of the UBIFS File System for Flash Memory

      • Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif

      Pages 190-206

   2. Inferring Mealy Machines

      • Muzammil Shahbaz, Roland Groz

      Pages 207-222

   3. Formal Management of CAD/CAM Processes

      • Michael Kohlhase, Johannes Lemburg, Lutz Schröder, Ewaryst Schulz

      Pages 223-238

6. Concurrency

   1. Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way

      • Rik Eshuis

      Pages 239-255

   2. Symbolic Predictive Analysis for Concurrent Programs

      • Chao Wang, Sudipta Kundu, Malay Ganai, Aarti Gupta

      Pages 256-272

   3. On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study

      • Edgar G. Daylight, Sandeep K. Shukla

      Pages 273-288

7. Refinement

   1. Sums and Lovers: Case Studies in Security, Compositionality and Refinement

      • Annabelle K. McIver, Carroll C. Morgan

      Pages 289-304

th FM 2009, the 16 International Symposium on Formal Methods, marked the 10th an- versary of the First World Congress on Formal Methods that was held in 1999 in Toulouse, France. We wished to celebrate this by advertising and organizing FM 2009 as the Second World Congress in the FM series, aiming to once again bring together the formal methods communities from all over the world. The statistics displayed in the table on the next page include the number of countries represented by the Programme Committee members, as well as of the authors of submitted and accepted papers. Novel this year was a special track on tools and industrial applications. Subm- sions of papers on these topics were especially encouraged, but not given any special treatment. (It was just as hard to get a special track paper accepted as any other paper.) What we did promote, however, was a discussion of how originality, contri- tion, and soundness should be judged for these papers. The following questions were used by our Programme Committee.

• B-method
• C programming language
• calculus
• communication protocols
• complexity
• constraint solving
• design
• distributed systems
• formal modeling
• formal specification
• logic
• model checking
• model-based testing
• statistics
• verification

• Department of Computer Science, Heslington, University of York, York, UK

  Ana Cavalcanti

• Bell Laboratories, Murray Hill, USA

  Dennis R. Dams

Policies and ethics