Chapter 9. Search Optimization
“Don’t find fault. Find a remedy.” | ||
| --(Henry Ford, 1863–1947) | ||
The basic algorithms for performing explicit state verification, as implemented in SPIN, are not very complicated. The hard problem in the construction of a verification system is therefore not so much in the implementation of these algorithms, but in finding effective ways to scale them to handle large to very large verification problems. In this chapter we discuss the methods that were implemented in SPIN to address this issue.
The optimization techniques we will review here have one of two possible aims: to reduce the number of reachable system states that must be searched to verify properties, or to reduce the amount of memory that is needed to store ...
Get Spin Model Checker, The: Primer and Reference Manual now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
