FM 2009: Eindhoven, The Netherlands

Invited Papers

• Michael Carl Tschantz, Jeannette M. Wing:
  Formal Methods for Privacy. 1-15
  
• Nicola Bonzanni, K. Anton Feenstra, Wan Fokkink, Elzbieta Krepska:
  What Can Formal Methods Bring to Systems Biology? 16-22
  
• Colin O'Halloran:
  Guess and Verify - Back to the Future. 23-32
  
• Sriram K. Rajamani:
  Verification, Testing and Statistics. 33-40
  
• Annabelle McIver, Larissa Meinicke, Carroll Morgan:
  Security, Probability and Nearly Fair Coins in the Cryptographers' Café. 41-71
  

Model Checking I

• Joxan Jaffar, Andrew E. Santosa:
  Recursive Abstractions for Parameterized Systems. 72-88
  
• Stefano Tonetta:
  Abstract Model Checking without Computing the Abstraction. 89-105
  
• Jonas Schrieb, Heike Wehrheim, Daniel Wonisch:
  Three-Valued Spotlight Abstractions. 106-122
  
• Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong:
  Fair Model Checking with Process Counter Abstraction. 123-139
  

Compositionality

• Rodrigo Ramos, Augusto Sampaio, Alexandre Mota:
  Systematic Development of Trustworthy Component Systems. 140-156
  
• Frédéric Lang, Radu Mateescu:
  Partial Order Reductions Using Compositional Confluence Detection. 157-172
  
• Ralph D. Jeffords, Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard:
  A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition. 173-189
  

Verification

• Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif:
  Abstract Specification of the UBIFS File System for Flash Memory. 190-206
  
• Muzammil Shahbaz, Roland Groz:
  Inferring Mealy Machines. 207-222
  
• Michael Kohlhase, Johannes Lemburg, Lutz Schröder, Ewaryst Schulz:
  Formal Management of CAD/CAM Processes. 223-238
  

Concurrency

• Rik Eshuis:
  Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way. 239-255
  
• Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta:
  Symbolic Predictive Analysis for Concurrent Programs. 256-272
  
• Edgar G. Daylight, Sandeep K. Shukla:
  On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study. 273-288
  

Refinement

• Annabelle McIver, Carroll C. Morgan:
  Sums and Lovers: Case Studies in Security, Compositionality and Refinement. 289-304
  
• Neil Walkinshaw, John Derrick, Qiang Guo:
  Iterative Refinement of Reverse-Engineered Models by Model-Based Testing. 305-320
  
• Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun:
  Model Checking Linearizability via Refinement. 321-337
  

Static Analysis

• Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies:
  It's Doomed; We Can Prove It. 338-353
  
• Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann:
  "Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis. 354-369
  
• Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla:
  Field-Sensitive Value Analysis by Field-Insensitive Analysis. 370-386
  

Theorem Proving

• Raymond Boute:
  Making Temporal Logic Calculational: A Tool for Unification and Discovery. 387-402
  
• Mark Reynolds:
  A Tableau for CTL. 403-418
  
• Christoph Lüth, Dennis Walter:
  Certifiable Specification and Verification of C Programs. 419-434
  
• Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour:
  Formal Reasoning about Expectation Properties for Continuous Random Variables. 435-450
  

Semantics

• Pawel Gancarski, Andrew Butterfield:
  The Denotational Semantics of slotted-Circus. 451-466
  
• Yifeng Chen, Jeff W. Sanders:
  Unifying Probability with Nondeterminism. 467-482
  
• Theophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi:
  Towards an Operational Semantics for Alloy. 483-498
  
• Steve Reeves, David Streader:
  A Robust Semantics Hides Fewer Errors. 499-515
  

Special Track: Industrial Applications I

• Faranak Heidarian, Julien Schmaltz, Frits W. Vaandrager:
  Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks. 516-531
  
• Jean Souyris, Virginie Wiels, David Delmas, Hervé Delseny:
  Formal Verification of Avionics Software Products. 532-546
  
• André Platzer, Edmund M. Clarke:
  Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. 547-562
  

Object-Orientation

• Kenneth Lausdahl, Hans Kristian Agerlund Lintrup, Peter Gorm Larsen:
  Connecting UML and VDM++ with Open Tool Support. 563-578
  
• Mar Yah Said, Michael J. Butler, Colin F. Snook:
  Language and Tool Support for Class and State Machine Refinement in UML-B. 579-595
  
• Einar Broch Johnsen, Marcel Kyas, Ingrid Chieh Yu:
  Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects. 596-611
  
• Wolfgang Ahrendt, Frank S. de Boer, Immo Grabe:
  Abstract Object Creation in Dynamic Logic. 612-627
  

Pointers

• Holger Gast:
  Reasoning about Memory Layouts. 628-643
  
• Helmut Seidl, Vesal Vojdani, Varmo Vene:
  A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis. 644-659
  

Real-Time

• Borzoo Bonakdarpour, Sandeep S. Kulkarni:
  On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery. 660-675
  
• Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas:
  Verifying Real-Time Systems against Scenario-Based Requirements. 676-691
  

Special Track: Tools and Industrial Applications II

• Artur Oliveira Gomes, Marcel Vinicius Medeiros Oliveira:
  Formal Specification of a Cardiac Pacing System. 692-707
  
• Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge:
  Automated Property Verification for Large Scale B Models. 708-723
  
• Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby:
  Reduced Execution Semantics of MPI: From Theory to Practice. 724-740
  

Model Checking II

• Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro:
  A Metric Encoding for Bounded Model Checking. 741-756
  
• Danhua Shao, Sarfraz Khurshid, Dewayne E. Perry:
  An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method. 757-772
  
• William R. Harris, Nicholas Kidd, Sagar Chaki, Somesh Jha, Thomas W. Reps:
  Verifying Information Flow Control over Unbounded Processes. 773-789
  
• María Alpuente, Demis Ballis, Daniel Romero:
  Specification and Verification of Web Applications in Rewriting Logic. 790-805
  

Industry-Day Abstracts

• Dirk Leinenbach, Thomas Santen:
  Verifying the Microsoft Hyper-V Hypervisor with VCC. 806-809
  
• Juan Bicarregui, John S. Fitzgerald, Peter Gorm Larsen, J. C. P. Woodcock:
  Industrial Practice in Formal Methods: A Review. 810-813
  
• Ulrik H. Hjort, Jacob Illum Rasmussen, Kim Guldstrand Larsen, Michael A. Petersen, Arne Skou:
  Model-Based GUI Testing Using Uppaal at Novo Nordisk. 814-818