[TYPES/announce] FM 2009: Accepted Papers

[Arend Rensink]

*********************************************************
*                                                       *
*  FM2009: 16th FM Symposium and 2nd World Congress     *
*            >>> Theory meets practice <<<              *
*                                                       *
*            October 30 - November 7,  2009             *
*              Eindhoven, the Netherlands               *
*             http://www.win.tue.nl/fm2009              *
*                                                       *
*                LIST OF ACCEPTED PAPERS                *
*                                                       *
*********************************************************

* A Formal Method for Developing Provably Correct Faul=t-Tolerant
 Systems Using Partial Refinement and Composition
 Ralph Jeffords, Constance Heitmeyer, Myla Archer and Elizabeth Leonard

* A smooth combination of linear and Herbrand equalities
   for polynomial time must-alias analysis
 Helmut Seidl, Vesal Vojdani and Varmo Vene

* A Tableau for CTL*
 Mark Reynolds

* Abstract Model Checking without Computing the Abstraction
 Stefano Tonetta

* Abstract Object Creation in Dynamic Logic - To Be or Not To Be Created
 Wolfgang Ahrendt, Frank de Boer and Immo Grabe

* Abstract Specification of the UBIFS File System for Flash Memory
 Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg and Wolfgang Reif

* Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks
 Faranak Heidarian, Julien Schmaltz and Frits Vaandrager

* Automated Property Verification for Large Scale B Models
 Michael Leuschel, Jérôme Falampin, Fabian Fritz and Daniel Plagge

* "Carbon Credits" for Resource-Bounded Computations using
   Amortised Analysis
 Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife and
   Martin Hofmann

* Certifiable specification and verification of C programs
 Christoph Lüth and Dennis Walter

* Connecting UML and VDM++ with Open Tool Support
 Kenneth Lausdahl, Hans Kristian Agerlund Lintrup and Peter Gorm Larsen

* Dynamic Classes: Modular Asynchronous Evolution of Distributed
   Concurrent Objects
 Einar Broch Johnsen, Marcel Kyas and Ingrid Chieh Yu

* Formal Management of CAD/CAM Processes
 Michael Kohlhase, Johannes Lemburg, Lutz Schröder and Ewaryst Schulz

* Formal Reasoning about Expectation Properties for Continuous
   Random Variables
 Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiene Tahar and
   Reza Akbarpour

* Formal Specification of a Cardiac Pacing System
 Artur Gomes and Marcel Vinicius Medeiros Oliveira Oliveira

* Formal Verification of Curved Flight Collision Avoidance Maneuvers:
   A Case Study
 Andre Platzer and Edmund Clarke

* Inferring Mealy Machines
 Muzammil Shahbaz and Roland Groz

* Iterative Refinement of Reverse-Engineered Models by Model-Based Testing
 Neil Walkinshaw, John Derrick and QIANG GUO

* It's doomed; we can prove it
 Jochen Hoenicke, Rustan Leino, Andreas Podelski, Martin Schäf and
   Thomas Wies

* Making Temporal Logic Calculational: A Tool For Unification and Discovery
 Raymond Boute

* Model Checking Linearizability via Refinement
 Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun

* On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time
   2-Phase Recovery
 Borzoo Bonakdarpour and Sandeep Kulkarni

* On the Difficulty of Concurrent-System-Design, Illustrated with a
   2x2 Switch Case Study
 Edgar Daylight and Sandeep Shukla

* Partial Order Reductions using Compositional Confluence Detection
 Frederic Lang and Radu Mateescu

* Perry: An incremental approach to scope-bounded checking using a
   lightweight formal method
 Danhua Shao, Sarfraz Khurshid and Dewayne E

* Reasoning about Memory Layouts
 Holger Gast

* Speci?cation and Veri?cation of Web Applications in  Rewriting Logic
 Demis Ballis, Daniel Romero and María Alpuente

* Sums and Lovers: Case studies in security, compositionality and
   refinement
 Annabelle McIver and Carroll Morgan

* Symbolic Predictive Analysis for Concurrent Programs
 Chao Wang, Sudipta Kundu, Malay Ganai and Aarti Gupta

* Systematic Development of Trustworthy Component Systems
 Rodrigo Ramos, Augusto Sampaio and Alexandre Mota

* The Denotation Semantics of Slotted-Circus
 Pawel Gancarski and Andrew Butterfield

* Three-Valued Spotlight Abstractions
 Jonas Schrieb, Heike Wehrheim and Daniel Wonisch

* Towards an Operational Semantics for Alloy
 Daniel Dougherty, Shriram Krishnamurthi, Kathi Fisler and
   Theophilos Giannakopoulos

* Verifying Information Flow Control Over Unbounded Processes
 William Harris, Nicholas Kidd, Sagar Chaki, Somesh Jha and
   Thomas Reps

* Verifying Real-time Systems against Scenario-based Requirements
 Kim Larsen, Shuhao Li, Brian Nielsen and Saulius Pusinskas