Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Model Checking Software

11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004, Proceedings

  • Conference proceedings
  • © 2004

Overview

Editors:
  1. Susanne Graf

    1. VERIMAG, Grenoble-Gières, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Laurent Mounier

    1. Vérimag Laboratory, Gières, France

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

Included in the following conference series:

Conference proceedings info: SPIN 2004.

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

  1. Front Matter

    Download chapter PDF

  2. Invited Paper

    1. Formal Analysis of Processor Timing Models

      • Reinhard Wilhelm
      Pages 1-4

  3. Heuristics and Probabilities

    1. Typical Structural Properties of State Spaces

      • Radek Pelánek
      Pages 5-22

    2. State Caching Reconsidered

      • Jaco Geldenhuys
      Pages 23-38

    3. Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM

      • Peter Leven, Tilman Mehler, Stefan Edelkamp
      Pages 39-56

    4. Fast and Accurate Bitstate Verification for SPIN

      • Peter C. Dillinger, Panagiotis Manolios
      Pages 57-75

  4. Improvements of SPIN

    1. Model-Driven Software Verification

      • Gerard J. Holzmann, Rajeev Joshi
      Pages 76-91

    2. Minimization of Counterexamples in SPIN

      • Paul Gastin, Pierre Moro, Marc Zeitoun
      Pages 92-108

  5. Validation of Timed Systems

    1. Black-Box Conformance Testing for Real-Time Systems

      • Moez Krichen, Stavros Tripakis
      Pages 109-126

    2. Validation of UML Models via a Mapping to Communicating Extended Timed Automata

      • Iulian Ober, Susanne Graf, Ileana Ober
      Pages 127-145

  6. Tool Papers

    1. Explicit State Model Checking with Hopper

      • Michael Jones, Eric Mercer
      Pages 146-150

    2. SEQ.OPEN: A Tool for Efficient Trace-Based Verification

      • Hubert Garavel, Radu Mateescu
      Pages 151-157

    3. Model Checking Genetic Regulatory Networks Using GNA and CADP

      • Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, Radu Mateescu
      Pages 158-163

  7. Abstraction and Symbolic Methods

    1. Verification of Java Programs Using Symbolic Execution and Invariant Generation

      • Corina S. Păsăreanu, Willem Visser
      Pages 164-181

    2. Polynomial Time Image Computation with Interval-Definable Counters Systems

      • Alain Finkel, Jérôme Leroux
      Pages 182-197

    3. Using Fairness to Make Abstractions Work

      • Dragan Bošnački, Natalia Ioustinova, Natalia Sidorova
      Pages 198-215

    4. A Scalable Incomplete Test for Message Buffer Overflow in Promela Models

      • Stefan Leue, Richard Mayr, Wei Wei
      Pages 216-233

  8. Applications

    1. Translation from Adapted UML to Promela for CORBA-Based Applications

      • J. Chen, H. Cui
      Pages 234-251

    2. Verifying Commit-Atomicity Using Model-Checking

      • Cormac Flanagan
      Pages 252-266

    3. Analysis of Distributed Spin Applied to Industrial-Scale Models

      • Murali Rangarajan, Samar Dajani-Brown, Kirk Schloegel, Darren Cofer
      Pages 267-285
Back to top

Other volumes

  1. Model Checking Software

Keywords

About this book

Since 1995, when the SPIN workshop series was instigated, SPIN workshops have been held on an annual basis in Montr´ eal (1995), New Brunswick (1996), Enschede (1997), Paris (1998), Trento (1999), Toulouse (1999), Stanford (2000), Toronto (2001), Grenoble (2002) and Portland (2003). All but the ?rst SPIN workshop were organized as satellite events of larger conferences, in particular of CAV (1996), TACAS (1997), FORTE/PSTV (1998), FLOC (1999), the World Congress on Formal Methods (1999), FMOODS (2000), ICSE (2001, 2003) and ETAPS (2002). This year again, SPIN was held as a satellite event of ETAPS 2004. The co-location of SPIN workshops with conferences has proven to be very successful and has helped to disseminate SPIN model checking technology to wider audiences. Since 1999, the proceedings of the SPIN workshops have appeared in Springer-Verlag’s Lecture Notes in Computer Science series. The history of successful SPIN workshops is evidence for the maturing of model checking technology, not only in the hardware domain, but increasingly also in the software area. While in earlier years algorithms and tool development aroundtheSPINmodelcheckerwerethefocusofthisworkshopseries,forseveral years now the scope has been widened to include more general approaches to software model checking techniques and tools as well as applications. The SPIN workshop has become a forum for all practitioners and researchers interested in model checking based techniques for the validation and analysis of communication protocols and software systems.

Editors and Affiliations

  • VERIMAG, Grenoble-Gières, France

    Susanne Graf

  • Vérimag Laboratory, Gières, France

    Laurent Mounier

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation