Introduction to and Overview of the SPIN Model Checker.

Bengt Jonsson, Tuesday Feb. 1 13.15

Place: Department of Information Technology in Uppsala Room: 1245 (Building 1, Floor 2, room 45)

ABSTRACT

Spin is a widely distributed software package that supports the formal verification of distributed systems. The software was developed by Gerard Holzmann at Bell Labs over the past two decades. It is probably the most efficient existing tool for enumerative state-space exploration in verification. Spin is free, comes with source-code, is very easy to install, learn and use. It is probably the most widely used model-checker in the world.

In this seminar, we give an introduction to Spin, its modeling language, how it works, and examples of how it can be used. The seminar is intended for anyone with an interest in how Spin works and how it can be applied.

The SPIN WWW page is http://netlib.bell-labs.com/netlib/spin/whatispin.html