Software model checking with SPIN

8 years 10 months ago
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
Gerard J. Holzmann
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2005
Where AC
Authors Gerard J. Holzmann
Comments (0)