Model Checking Software

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

  • Matthew Dwyer
Conference proceedings SPIN 2001

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

Table of contents

  1. Front Matter
    Pages I-XI
  2. Invited Keynotes

    1. Doron Peled, Lenore Zuck
      Pages 1-14
  3. Model checking if your life depends on it: a view from intel’s trenches

  4. Technical Papers and Tool Reports

    1. Marsha Chechik, Benet Devereux, Arie Gurfinkel
      Pages 16-36
    2. Javier Esparza, Keijo Heljanko
      Pages 37-56
  5. Directed explicit model checking with HSF-SPIN

    1. Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue
      Pages 57-79
  6. Addressing dynamic issues of program model checking

    1. Flavio Lerda, Willem Visser
      Pages 80-102
  7. Automatically validating temporal safety properties of interfaces

    1. Thomas Ball, Sriram K. Rajamani
      Pages 102-122
  8. Verification experiments on the MASCARA protocol

    1. Guoping Jia, Susanne Graf
      Pages 123-142
  9. Using SPIN for feature interaction analysis - a case study

    1. Muffy Calder, Alice Miller
      Pages 143-162
  10. Behavioural analysis of the enterprise javaBeans™ component architecture

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

  12. Transformations for model checking distributed java programs

    1. Scott D. Stoller, Yanhong A. Liu
      Pages 192-199
  13. Distributed LTL model-checking in SPIN

    1. Jiri Barnat, Lubos Brim, Jitka Stříbrná
      Pages 200-216
  14. Parallel state space construction for model-checking

    1. Hubert Garavel, Radu Mateescu, Irina Smarandache
      Pages 217-234
  15. Model checking systems of replicated processes with spin

    1. Fabrice Derepas, Paul Gastin
      Pages 235-251
  16. A SPIN-based model checker for telecommunication protocols

    1. Vivek K. Shanbhag, K. Gopinath
      Pages 252-271
  17. Modeling and verifying a price model for congestion control in computer networks using promela/spin

  18. Invited Project Summaries

    1. Leszek Holenderski
      Pages 288-295
    2. Darren Cofer, Eric Engstrom, Robert Goldman, David Musliner, Steve Vestal
      Pages 296-303
    3. Bernhard Steffen, Tiziana Margaria, Volker Braun
      Pages 304-311
  19. Back Matter
    Pages 313-313

About these proceedings


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.


Concurrent Systems Distributed Systems Finite State Systems Formal Methods Mathematical Foundations Program Analysis Programming Theory Proof Theory Software Verification Systems Validation Systems Verificati formal verification model checking verification

Editors and affiliations

  • Matthew Dwyer
    • 1
  1. 1.Department of Computing and Information SciencesKansas State UniversityManhattanUSA

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2001
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-42124-5
  • Online ISBN 978-3-540-45139-6
  • Series Print ISSN 0302-9743
  • Buy this book on publisher's site
Industry Sectors
Chemical Manufacturing
Finance, Business & Banking
IT & Software
Energy, Utilities & Environment