Skip to main content
SpringerLink
Log in

FM 2008: Formal Methods

15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Proceedings

  • Conference proceedings
  • © 2008

Overview

Editors:
  1. Jorge Cuellar
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Tom Maibaum
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Kaisa Sere
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 5014)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Included in the following conference series:

Conference proceedings info: FM 2008.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (32 papers)

  1. Front Matter

    Download chapter 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
Back to top

Other volumes

  1. FM 2008: Formal Methods

Keywords

About this book

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.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation