Software model checking with SPIN

The aim of this chapter is to give an overview of the theoretical foundation and the practical application of logic model checking techniques for the verification of multi-threaded software (rather than hardware) systems. The treatment is focused on the logic model checker SPIN, which was designed for this specific domain of application. SPIN implements an automata-theoretic method of verification. Although the tool has been available for over 15 years, it continues to evolve, adopting new optimization strategies from time to time to help it tackle larger verification problems. This chapter explains how the tool works, and which types of software verification problems it is designed to handle. Contents

• Type: Journal
• Year: 2005
• Where: AC
• Authors: Gerard J. Holzmann
• Keywords: AC 2005, Larger Verification Problems, Logic Model, Software Engineering, Theoretical Foundation