TranscriptThis is a short course in software verification for which we will be using the logic model checker Spin.
The course is in four parts, explaining the basics of the various steps that are involved in doing software verification. The first part covers basic automata theory, omega automata, modeling parallel processes and correctness properties, leading upto a simple explanation of the automata theoretic verification method, which is used in Spin.
Then, there are two possible tracks you can take. One track, is an explanation of Promela, the process meta language that you can use to specify pure Spin models for Spin verification. Another track explains model extraction from C code using the Modex tool. It explains how non-determinism is used in model extraction, and explains which features in the Spin specification language are used to support embedded C code that is imported with the model extractor.
The last part of the course deals with applying model checking to larger problem sizes, which relies on abstraction, proof approximation techniques and the use of swarm search on multi-core systems and grid compute networks.
At the end of this course you should be able to prove key correctness properties of small multi-threaded C programs, and build basic verification models to experiment with. Plus, you'll have a good understanding of what makes formal software verification work.
The only pre-requisites are to have a general familiarity with programming in C and with the basics of compiling and running programs in a Unix-like system.
All the tools we use in this course are freely available from the spinroot website.
(c) 2015 All rights reserved