FM 2008: Formal Methods

1. Front Matter

   PDF

2. Session 1. Invited Talks

   1. Aspects and Formal Methods

      • Shmuel Katz

      Pages 1-11

   2. Getting Formal Verification into Design Flow

      • Arvind, Nirav Dave, Michael Katelman

      Pages 12-32

   3. Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems

      • Dawson Engler

      Pages 33-33

   4. Simulation, Orchestration and Logical Clocks

      • David Kitchen, Evan Powell, Jayadev Misra

      Pages 34-34

3. Session 2. Programming Language Analysis

   1. CoVaC: Compiler Validation by Program Analysis of the Cross-Product

      • Anna Zaks, Amir Pnueli

      Pages 35-51

   2. Lazy Behavioral Subtyping

      • Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen

      Pages 52-67

   3. Checking Well-Formedness of Pure-Method Specifications

      • Arsenii Rudich, Ádám Darvas, Peter Müller

      Pages 68-83

4. Session 3. Verification

   1. Verifying Dynamic Pointer-Manipulating Threads

      • Thomas Noll, Stefan Rieger

      Pages 84-99

   2. Proofs and Refutations for Probabilistic Refinement

      • A. K. McIver, C. C. Morgan, C. Gonzalia

      Pages 100-115

   3. Assume-Guarantee Verification for Interface Automata

      • Michael Emmi, Dimitra Giannakopoulou, Corina S. Păsăreanu

      Pages 116-131

5. Session 4. Real-Time and Concurrency

   1. Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation

      • Carlo A. Furia, Matteo Pradella, Matteo Rossi

      Pages 132-147

   2. A Model Checking Language for Concurrent Value-Passing Systems

      • Radu Mateescu, Damien Thivolle

      Pages 148-164

6. Session 5. Grand Chellenge Problems

   1. Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code

      • Holger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn, Wolfgang Reif

      Pages 165-180

   2. Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM

      • Hugo Daniel Macedo, Peter Gorm Larsen, John Fitzgerald

      Pages 181-197

7. Session 6. FM Practice

   1. Industrial Use of Formal Methods for a High-Level Security Evaluation

      • Boutheina Chetali, Quang-Huy Nguyen

      Pages 198-213

   2. Secret Ninja Formal Methods

      • Joseph R. Kiniry, Daniel M. Zimmerman

      Pages 214-228

   3. Specification and Checking of Software Contracts for Conditional Information Flow

      • Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David Greve

      Pages 229-245

8. Session 7. Runtime Moitoring and Analysis

   1. JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity

      • Patrice Chalin, Frédéric Rioux

      Pages 246-261

   2. Provably Correct Runtime Monitoring

      • Irem Aktug, Mads Dam, Dilian Gurov

      Pages 262-277

This book presents the refereed proceedings of the 15th International Symposium on Formal Methods, FM 2008, held in Turku, Finland in May 2008. The 23 revised full papers presented together with 4 invited contributions and extended abstracts of 5 invited industrial presentations were carefully reviewed and selected from 106 submissions. The papers are organized in topical sections on programming language analysis, verification, real-time and concurrency, grand chellenge problems, fm practice, runtime monitoring and analysis, communication, constraint analysis, and design.

• Constraint
• Programming language A
• design
• formal method
• programming
• programming language
• real-time
• verification

Policies and ethics