The SPIN Model Checker - primer and reference manual

By Gerard J. Holzmann. 2003

2,646 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/33ec9130b2cfd2e46e5f365a851ed49d888ad65c

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

A Declarative Approach for Flexible Business Processes Management (2006, methodology): “The Spin tool [13] uses an automata theoretic approach for the simulation and exhaustive formal verification of systems, and as a proof approximation system.”
Combining unit-level symbolic execution and system-level concrete execution for testing nasa software (2008, methodology): “Techniques for checking software include model checking (e.g., [ 23 , 26, 18, 7, 22]), static analysis (e.g., [29]), and testing.”
Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III (2019, unknown): “MonPoly [8] TimeSquare [11] RV-Monitor [27]”
Privacy and contextual integrity: framework and applications (2006, methodology): “Furthermore, there are tools that work well in practice, such as the widely used SPIN model-checker [24].”
A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications (2008, background): “If there are blocking states in T , then the “stutter extension" rule [10], [39] can be applied when”
Practical verification of decision-making in agent-based autonomous systems (2013, methodology): “(2012) have investigated the model checking of Brahms (Sierhuis 2001) programs using SPIN (Holzmann 2004).”
CADP 2011: a toolbox for the construction and analysis of distributed processes (2012, unknown): “Spin [75]), Cadp has the following principles and distinctive features (some of which were already present in precursory tools rooted in concurrency theory, such as Cwb [24] and Cwb- Nc [23]): – Cadp supports both high-level languages with a formal”
Principles of model checking (2008, methodology): “For further reading on partial order reduction and its implementation in the model checker SPIN we refer to [169], [92, Chapter 10], and the monograph by Holzmann on SPIN [209].”
Programming Multi-Agent Systems in AgentSpeak using Jason (Wiley Series in Agent Technology) (2007, methodology): “One target model checker for the translation was the SPIN system [53].”
Worst‐case execution time analysis for a Java processor (2010, unknown): “who used the SPIN model checker [16] to verify parts of the MPD process manager used in MPICH2 [20].”
Randomized Differential Testing as a Prelude to Formal Verification (2007, methodology): “We believe the reference implementation and hardware simulation will be equally useful for model-driven verification [6] using the SPIN model checker [4].”