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. Springer 2009 Lecture Notes in Computer Science ISBN 978-3-642-05088-6
Invited Papers
- 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
- Stefano Tonetta: Abstract Model Checking without Computing the Abstraction. 89-105
- 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
- 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
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 T. Boute: Making Temporal Logic Calculational: A Tool for Unification and Discovery. 387-402
- Mark Reynolds: A Tableau for CTL. 403-418
- Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour: Formal Reasoning about Expectation Properties for Continuous Random Variables. 435-450
Semantics
- Theophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi: Towards an Operational Semantics for Alloy. 483-498
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
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
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T203413 by the dblp team