FM 2009: Eindhoven, The Netherlands

Ana Cavalcanti, Dennis Dams (Eds.): FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. Lecture Notes in Computer Science 5850 Springer 2009, ISBN 978-3-642-05088-6

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

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

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

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

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

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

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

Raymond T. 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

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

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

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

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

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

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

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

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

Last update Fri May 25 08:14:13 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page