SPIN: A Swiss Army Knife

Theo Ruys
University of Twente
Friday, 25 November, 2005 (All day)

SPIN is a well-known, state-of-the-art model checker for the verification of distributed systems. This talk will show that SPIN can be used for much more than verifying software systems and it is argued that SPIN should be part of every computer science engineer's toolbox. For example, the talk will illustrate how SPIN can be used to solve optimization problems and as a database engine for XML databases. Furthermore, some general patterns to contruct efficient PROMELA models will be discussed and techniques will be presented how to use SPIN in the most effective way. The talk itself will have a tutorial-like presentation style and the objective is to make attendees (even more) enthusiastic about explicit state model checkers.