Skip to main content
SpringerLink
Log in
Book cover

Formal Methods for Components and Objects

4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures

  • Conference proceedings
  • © 2006

Overview

Editors:
  1. Frank S. Boer

    1. Centre for Mathematics and Computer Science, CWI, Amsterdam, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Marcello M. Bonsangue

    1. Leiden Institute of Advanced Computer Science, Leiden University, Leiden, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Susanne Graf

    1. Centre Equitation, VERIMAG, Grenoble-Gières, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Willem-Paul Roever

    1. Institute of Computer Science and Applied Mathematics, Christian-Albrechts University, Kiel, Germany

    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 4111)

Included in the following conference series:

Conference proceedings info: FMCO 2005.

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 (19 papers)

  1. Front Matter

    Download chapter PDF

  2. Component and Service Oriented Computing

    1. A Software Component Model and Its Preliminary Formalisation

      • Kung-Kiu Lau, Mario Ornaghi, Zheng Wang
      Pages 1-21

    2. Synchronised Hyperedge Replacement as a Model for Service Oriented Computing

      • Gian Luigi Ferrari, Dan Hirsch, Ivan Lanese, Ugo Montanari, Emilio Tuosto
      Pages 22-43

  3. System Design

    1. Control of Modular and Distributed Discrete-Event Systems

      • Jan Komenda, Jan H. van Schuppen
      Pages 44-63

    2. Model-Based Security Engineering with UML: Introducing Security Aspects

      • Jan Jürjens
      Pages 64-87

    3. The Pragmatics of STAIRS

      • Ragnhild Kobro Runde, Øystein Haugen, Ketil Stølen
      Pages 88-114

  4. Tools

    1. Smallfoot: Modular Automatic Assertion Checking with Separation Logic

      • Josh Berdine, Cristiano Calcagno, Peter W. O’Hearn
      Pages 115-137

    2. Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs

      • Dennis R. Dams, Kedar S. Namjoshi
      Pages 138-160

  5. Algebraic Methods

    1. Beyond Bisimulation: The “up-to” Techniques

      • Davide Sangiorgi
      Pages 161-171

    2. Separation Results Via Leader Election Problems

      • Maria Grazia Vigliotti, Iain Phillips, Catuscia Palamidessi
      Pages 172-194

    3. Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation

      • Wan Fokkink, Rob van Glabbeek, Paulien de Wind
      Pages 195-218

  6. Model Checking

    1. Abstraction and Refinement in Model Checking

      • Orna Grumberg
      Pages 219-242

    2. Program Compatibility Approaches

      • Edmund Clarke, Natasha Sharygina, Nishant Sinha
      Pages 243-258

    3. Cluster-Based LTL Model Checking of Large Systems

      • Jiří Barnat, Luboš Brim, Ivana Černá
      Pages 259-279

    4. Safety and Liveness in Concurrent Pointer Programs

      • Dino Distefano, Joost-Pieter Katoen, Arend Rensink
      Pages 280-312

  7. Assertional Methods

    1. Modular Specification of Encapsulated Object-Oriented Components

      • Arnd Poetzsch-Heffter, Jan Schäfer
      Pages 313-341

    2. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2

      • Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll
      Pages 342-363

    3. Boogie: A Modular Reusable Verifier for Object-Oriented Programs

      • Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino
      Pages 364-387

  8. Quantitative Analysis

    1. On a Probabilistic Chemical Abstract Machine and the Expressiveness of Linda Languages

      • Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky
      Pages 388-407

    2. Partial Order Reduction for Markov Decision Processes: A Survey

      • Marcus Groesser, Christel Baier
      Pages 408-427
Back to top

Other volumes

  1. Formal Methods for Components and Objects

Keywords

About this book

Formal methods have been applied successfully to the verification of medium-sized programs in protocol and hardware design. However, their application to the development of large systems requires more emphasis on specification, modelling and validation techniques supporting the concepts of reusability and modifiability, and their implementation in new extensions of existing programming languages.

This book presents 19 revised invited keynote lectures and revised tutorial lectures given by top-researchers at the 4th International Symposium on Formal Methods for Components and Objects, FMCO 2005, held in Amsterdam, Netherlands, in November 2005. The book provides a unique combination of ideas on software engineering and formal methods that reflect the current interest in the application or development of formal methods for large scale software systems such as component-based systems and object systems. The papers are organized in topical sections on component and service oriented computing, system design, tools, algebraic methods, model checking, assertional methods, quantitative analysis.

Editors and Affiliations

  • Centre for Mathematics and Computer Science, CWI, Amsterdam, The Netherlands

    Frank S. Boer

  • Leiden Institute of Advanced Computer Science, Leiden University, Leiden, The Netherlands

    Marcello M. Bonsangue

  • Centre Equitation, VERIMAG, Grenoble-Gières, France

    Susanne Graf

  • Institute of Computer Science and Applied Mathematics, Christian-Albrechts University, Kiel, Germany

    Willem-Paul Roever

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation