Skip to main content
SpringerLink
Log in

Model Checking Software

8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001 Proceedings

  • Conference proceedings
  • © 2001

Overview

Editors:
  1. Matthew Dwyer

    1. Department of Computing and Information Sciences, Kansas State University, Manhattan, USA

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

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

  1. Front Matter

    Pages I-XI
    Download chapter PDF

  2. Invited Keynotes

    1. From model checking to a temporal proof

      • Doron Peled, Lenore Zuck
      Pages 1-14

  3. Model checking if your life depends on it: a view from intel’s trenches

    1. Model checking if your life depends on it: a view from intel’s trenches

      • Rob Gerth
      Pages 15-15

  4. Technical Papers and Tool Reports

    1. Model-checking in finite state-space systems with fine-grained abstractions using SPIN

      • Marsha Chechik, Benet Devereux, Arie Gurfinkel
      Pages 16-36

    2. Implementing LTL model checking with net unfoldings

      • Javier Esparza, Keijo Heljanko
      Pages 37-56

  5. Directed explicit model checking with HSF-SPIN

    1. Directed explicit model checking with HSF-SPIN

      • Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue
      Pages 57-79

  6. Addressing dynamic issues of program model checking

    1. Addressing dynamic issues of program model checking

      • Flavio Lerda, Willem Visser
      Pages 80-102

  7. Automatically validating temporal safety properties of interfaces

    1. Automatically validating temporal safety properties of interfaces

      • Thomas Ball, Sriram K. Rajamani
      Pages 102-122

  8. Verification experiments on the MASCARA protocol

    1. Verification experiments on the MASCARA protocol

      • Guoping Jia, Susanne Graf
      Pages 123-142

  9. Using SPIN for feature interaction analysis - a case study

    1. Using SPIN for feature interaction analysis - a case study

      • Muffy Calder, Alice Miller
      Pages 143-162

  10. Behavioural analysis of the enterprise javaBeans™ component architecture

    1. Behavioural analysis of the enterprise javaBeans™ component architecture

      • Shin Nakajima, Tetsuo Tamai
      Pages 163-182

  11. p2b: A translation utility for linking promela and symbolic model checking (tool paper)

    1. p2b: A translation utility for linking promela and symbolic model checking (tool paper)

      • Michael Baldamus, Jochen Schröder-Babo
      Pages 183-191

  12. Transformations for model checking distributed java programs

    1. Transformations for model checking distributed java programs

      • Scott D. Stoller, Yanhong A. Liu
      Pages 192-199

  13. Distributed LTL model-checking in SPIN

    1. Distributed LTL model-checking in SPIN

      • Jiri Barnat, Lubos Brim, Jitka Stříbrná
      Pages 200-216

  14. Parallel state space construction for model-checking

    1. Parallel state space construction for model-checking

      • Hubert Garavel, Radu Mateescu, Irina Smarandache
      Pages 217-234

  15. Model checking systems of replicated processes with spin

    1. Model checking systems of replicated processes with spin

      • Fabrice Derepas, Paul Gastin
      Pages 235-251

  16. A SPIN-based model checker for telecommunication protocols

    1. A SPIN-based model checker for telecommunication protocols

      • Vivek K. Shanbhag, K. Gopinath
      Pages 252-271

  17. Modeling and verifying a price model for congestion control in computer networks using promela/spin

    1. Modeling and verifying a price model for congestion control in computer networks using promela/spin

      • Clement Yuen, Wei Tjioe
      Pages 272-287

  18. Invited Project Summaries

    1. A model checking project at philips research

      • Leszek Holenderski
      Pages 288-295

    2. Applications of model checking at honeywell laboratories

      • Darren Cofer, Eric Engstrom, Robert Goldman, David Musliner, Steve Vestal
      Pages 296-303
Back to top

Keywords

About this book

This book constitutes the refereed proceedings of the 8th International SPIN Workshop held in Toronto, Canada, in May 2001.
The SPIN model checker is one of the most powerful and popular systems for the analysis and verification of distributed and concurrent systems.
The 13 revised full papers presented together with one invited survey paper and three invited industrial experience reports were carefully reviewed and selected from 26 submissions. Besides foundational issues of program analysis and formal verification, the papers focus on tools for model checking and practical applications in a variety of fields.

Editors and Affiliations

  • Department of Computing and Information Sciences, Kansas State University, Manhattan, USA

    Matthew Dwyer

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation