Skip to main content
SpringerLink
Log in

SPIN Model Checking and Software Verification

7th International SPIN Workshop Stanford, CA, USA, August 30 - September 1, 2000 Proceedings

  • Conference proceedings
  • © 2000

Overview

Editors:
  1. Klaus Havelund

    1. Kestrel Technology, Palo Alto, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. John Penix

    1.  ,  

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Willem Visser

    1. SEVEN Networks, Redwood City, 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 1885)

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

    Download chapter PDF

  2. Papers

    1. Symmetric Spin

      • Dragan Bošnački, Dennis Dams, Leszek Holenderski
      Pages 1-19

    2. Using Garbage Collection in Model Checking

      • Radu Iosif, Riccardo Sisto
      Pages 20-33

    3. Model Checking Based on Simultaneous Reachability Analysis

      • Bengi Karaçali, Kuo-Chung Tai
      Pages 34-53

    4. Testing Spin’s LTL Formula Conversion into Büchi Automata with Randomly Generated Input

      • Heikki Tauriainen, Keijo Heljanko
      Pages 54-72

    5. Verification and Optimization of a PLC Control Schedule

      • Ed Brinksma, Angelika Mader
      Pages 73-92

    6. Modeling the ASCB-D Synchronization Algorithm with SPIN: A Case Study

      • Nicholas Weininger, Darren Cofer
      Pages 93-112

    7. Bebop: A Symbolic Model Checker for Boolean Programs

      • Thomas Ball, Sriram K. Rajamani
      Pages 113-130

    8. Logic Verification of ANSI-C Code with SPIN

      • Gerard J. Holzmann
      Pages 131-147

    9. Interaction Abstraction for Compositional Finite State Systems

      • Wayne Liu
      Pages 148-162

    10. Correctness by Construction: Towards Verification in Hierarchical System Development

      • Mila Majster-Cederbaum, Frank Salger
      Pages 163-180

    11. Linking ST e P with SPIN

      • Anca Browne, Henny Sipma, Ting Zhang
      Pages 181-186

    12. Abstraction of Communication Channels in Promela: A Case Study

      • Elena Fersman, Bengt Jonsson
      Pages 187-204

    13. A Language Framework for Expressing Checkable Properties of Dynamic Software

      • James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby
      Pages 205-223

    14. Model-Checking Multi-threaded Distributed Java Programs

      • Scott D. Stoller
      Pages 224-244

    15. Using Runtime Analysis to Guide Model Checking of Java Programs

      • Klaus Havelund
      Pages 245-264

    16. Communication Topology Analysis for Concurrent Programs

      • Matthieu Martel, Marc Gengler
      Pages 265-286

    17. Low-Fat Recipes for SPIN

      • Theo C. Ruys
      Pages 287-321

  3. Tool Tutorials

    1. Tutorial on FDR and Its Applications

      • Philippa Broadfoot, Bill Roscoe
      Pages 322-322

    2. The Temporal Rover and the ATG Rover

      • Doron Drusinsky
      Pages 323-330
Back to top

Keywords

About this book

The SPIN workshop is a forum for researchers interested in the subject of automata-based, explicit-state model checking technologies for the analysis and veri?cation of asynchronous concurrent and distributed systems. The SPIN - del checker (http://netlib.bell-labs.com/netlib/spin/whatispin.html), developed by Gerard Holzmann, is one of the best known systems of this kind, and has attracted a large user community. This can likely be attributed to its e?cient state exploration algorithms. The fact that SPIN’s modeling language, Promela, resembles a programming language has probably also contributed to its success. Traditionally, the SPIN workshops present papers on extensions and uses of SPIN. As an experiment, this year’s workshop was broadened to have a slightly wider focus than previous workshops in that papers on software veri?cation were encouraged. Consequently, a small collection of papers describe attempts to analyze and verify programs written in conventional programming languages. Solutions include translations from source code to Promela, as well as specially designed model checkers that accept source code. We believe that this is an - teresting research direction for the formal methods community, and that it will result in a new set of challenges and solutions. Of course, abstraction becomes the key solution to deal with very large state spaces. However, we also see - tential for integrating model checking with techniques such as static program analysis and testing. Papers on these issues have therefore been included in the proceedings.

Editors and Affiliations

  • Kestrel Technology, Palo Alto, USA

    Klaus Havelund

  •  ,  

    John Penix

  • SEVEN Networks, Redwood City, USA

    Willem Visser

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation