The SPIN Model Checker - primer and reference manual

Keywords

Debugging, Computer science, Software engineering, Software, Model checking

References

• Logic in Computer Science: Modelling and Reasoning about SystemsMichael Huth, Mark Ryan — 2000
• Static determination of dynamic properties of programsPatrick Cousot, Radhia Cousot — 1976
• Process Synchronization in the UTS KernelLawrence M. Ruane — 1990
• Temporal verification of reactive systems - safetyZohar Manna, Amir Pnueli — 1995
• Algorithms for mutual exclusionMichel Raynal, D. Beeson — 1986
• Systems and Software Verification, Model-Checking Techniques and ToolsBéatrice Bérard, Michel Bidoit, Alain Finkel — 2001
• Notes on structured programmingEdsger W. Dijkstra — 1970
• Towards effective model checkingT.C. Ruys — 2001
• Planning and coding of problems for an Electronic Computing InstrumentHerman H. Goldstine, John von Neumann — 1947
• From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931Jean van Heijenoort — 1967
• Formal Verification of a Partial-Order Reduction Technique for Model CheckingChing-Tsun Chou, Doron Peled — 1996
• Combining partial order reductions with on-the-fly model-checkingDoron Peled — 1994
• Software model checking: extracting verification models from source code †Gerard J. Holzmann, Margaret Smith — 2001
• A note on reliable full-duplex transmission over half-duplex linksKeith A. Bartlett, R.A. Scantlebury, P. T. Wilkinson — 1969
• Recognizing safety and livenessBowen Alpern, Fred B. Schneider — 2005
• Event fairness and non-interleaving concurrencyMarta Kwiatkowska — 1989
• Patterns in property specifications for finite-state verificationMatthew B. Dwyer, George S. Avrunin, James C. Corbett — 1999
• State-space caching revisitedPatrice Godefroid, Gerard J. Holzmann, Didier Pirottin — 1992
• Memory-efficient algorithms for the verification of temporal propertiesC. Courcoubetis, M. Vardi, Pierre Wolper — 1990
• A graphical interval logic for specifying concurrent systemsLaura K. Dillon, G. Kutty, L.E. Moser — 1994

Cited by

• Running COLA on Embedded SystemsWolfgang Haberl, Uwe Baumgarten, Michael Tautschnig — 2008
• EpiSpin: An Eclipse Plug-in for Promela and SpinBob de Vos — 2011
• Multi-Model Heterogeneous Verification of Cyber-Physical SystemsAkshay H. Rajhans — 2013
• Verifikation von Webservicekompositionen:Maximilian Röglinger — 2009
• Model Checking C Programs by Translating C to PromelaKe Jiang — 2009
• Specifying, Discovering, and Monitoring Service Flows: Making Web Services Process-AwareMaja Pešić — 2006
• Comparing the use of symmetry in constraint processing and model checkingAlastair F. Donaldson, Alice Miller, Muffy Calder — 2004
• Layered Fault Tolerance for Distributed Embedded SystemsRaul Barbosa — 2008
• Systematic and Scalable Testing of Concurrent ProgramsRandy Bryant, Garth A. Gibson, Jiřı Šimša — 2013
• Model Checking for Clinical Guidelines: an Agent-based ApproachLaura Giordano, Paolo Terenziani, Alessio Bottrighi — 2006
• Custom and model based detection of deficiencies related to Java multithreadingJ. Singh — 2005
• Analyse de Programmes Malveillants par Abstraction de Comportements. (Analysis of Malware by Behavior Abstraction)Philippe Beaucamps — 2011
• Efficient web services discovery and compositionYanan Hao — 2009
• Incomplete property checking for asynchronous reactive systemsWei Wei — 2008
• Acquisition et analyse des exigences pour le développement logiciel : une approche dirigée par les modèlesErwan Brottier — 2009
• Symbolic analysis of scenario based timed models for component based systems : Compositionality results for testingBoutheina Bannour — 2012
• Impact Analysis of Changes in Functional Requirements in the Behavioral View of Software ArchitecturesS.A.M. Looman — 2009
• Progressive on-the-fly test methodJorge Mamede, Eurico Carrapatoso, Manuel Ricardo — 2005
• Transformation of PROMELA to Channel SystemsSheila Nurul Huda, Reza Pulungan — 2013
• Modelling and Verification of a Shortest Path Tree Protocol for Wireless Sensor Networks : Towards a Platform for Formal Verification ExperimentsWouter M. Everse — 2009

Related papers

• Communicating Sequential ProcessesTony Hoare — 1985
• Model checkingE. M. Clarke, Orna Grümberg, D. Long — 1996
• Model checking programsWillem Visser, Klaus Havelund, Guillaume Brat — 2000
• Bandera: extracting finite-state models from Java source codeJames C. Corbett, Matthew B. Dwyer, John Hatcliff — 2000
• Automatic verification of finite-state concurrent systems using temporal logic specificationsE. M. Clarke, E. Allen Emerson, A. Prasad Sistla — 1986
• The Model Checker SPINGerard J. Holzmann — 1997
• A Theory of Timed AutomataRajeev Alur, David L. Dill — 1994
• Symbolic Model Checking: 10^20 States and BeyondJerry R. Burch, E. M. Clarke, Kenneth L. McMillan — 1990
• The temporal logic of programsAmir Pnueli — 1977