The model checker SPIN

The work

AuthorsG. J. Holzmann
Editors
Typearticle
Year1997
Citekeyholzmann1997model

Where it appeared

Published inIEEE Transactions on Software Engineering
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Volume23
Issue5
Pages279--295

Identifiers

DOI10.1109/32.588521
OpenAlexW2115309705

Access

Landing pagehttps://doi.org/10.1109/32.588521

Abstract

SPIN is an efficient verification system for models of distributed software systems. It has been used to detect design errors in applications ranging from high-level descriptions of distributed algorithms to detailed code for controlling telephone exchanges. The paper gives an overview of the design and structure of the verifier, reviews its theoretical foundation, and gives an overview of significant practical applications.

How it got here

How it got hereimport via drheap-program-correctness
Added2026-08-23 00:00 UTC
Approved bya person 2026-08-24 07:32 UTC

Filed under

one-survey-section state-space-not-proof

Cite it as

@article{holzmann1997model,
  title        = {The model checker SPIN},
  author       = {G. J. Holzmann},
  year         = {1997},
  journal      = {IEEE Transactions on Software Engineering},
  publisher    = {Institute of Electrical and Electronics Engineers (IEEE)},
  volume       = {23},
  number       = {5},
  pages        = {279--295},
  doi          = {10.1109/32.588521},
}

This record lives at https://refs.drheap.org/holzmann1997model/ and will keep doing so.