Spin Model Checker, The: Primer and Reference Manual

Chapter 8. Search Algorithms

	“If I had eight hours to chop down a tree, I’d spend six hours sharpening my axe.”
	--(Abraham Lincoln, 1809–1865)

In this chapter we will discuss the basic algorithms that SPIN uses to verify correctness properties of PROMELA models. The basic algorithms are fairly simple and can quickly be explained. But, if we are interested in applying a verifier to problems of practical size, the mere basics do not always suffice. There are many ways in which the memory use and the run-time requirements of the basic algorithms can be optimized. Perhaps SPIN’s main strength lies in the range of options it offers to perform such optimizations, so that even very large problem sizes can be handled efficiently. To structure the discussion ...