The SPIN Model Checker

By Gerard J. Holzmann. 2003

1,413 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/b8574b7f97e12dc5e2cedaf32fe87af9dd4d6216

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

Efficient On-the-Fly Algorithms for the Analysis of Timed Games (2005, methodology): “…been a very active research topic since the end of the 80’s [12,4,15] and is one of the most important techniques applied in ﬁnite-state model-checkers using enumerative or explicit state-space representation, as is the case with SPIN [10], which performs on-the-ﬂy model-checking of LTL properties.”
Software model checking (2009, unknown): “For example, Spin allows users to write arbitrary C code for part of the model that is executed during the model checking search.”
Deductive Software Verification – The KeY Book (2016, methodology): “The course introduces model checking with PROMELA and SPIN [Holzmann, 2003] in its first part and functional verification of Java with KeY in the second.”
Automatically validating temporal safety properties of interfaces (2001, background): “SLAM seeks a sweet spot between VCGen-based tools [16, 22, 5] that operate directly on the concrete semantics and model checking or data ow-analysis based tools [7, 18, 13, 11] that operate on abstractions of the program.”
Race directed random testing of concurrent programs (2008, background): “Static verification [4, 16, 28, 40, 8] and model checking [17, 29, 25, 27, 52, 31] or path-sensitive search of the state space is an alternative approach to finding bugs in concurrent programs.”
Combining unit-level symbolic execution and system-level concrete execution for testing nasa software (2008, unknown): “, [23, 26, 18, 7, 22]), static analysis (e.”
The software model checker Blast (2007, background): “Software model checking, the application of algorithmic verification to implemented code, has been an active area of recent research [4,17,28,35,42, 52,66].”
A view of 20th and 21st century software engineering (2006, methodology): “Some good progress in high-assurance software technology continues to be made, including Hoare and others’ scalable use of assertions in Microsoft products [71], Scherlis’ tools for detecting Java concurrency problems, Holtzmann and others’ model-checking capabilities [78] Poore and others’ model-ba”
Autonomous driving in urban environments: approaches, lessons and challenges (2010, background): “Tools such as SPIN (Holzmann 2003) and TLC (Lamport 2002) are able to efﬁciently enumerate all possible executions and can be used for quite large systems.”