[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
********************************************************* * * * 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