Verification Techniques VT 10


NEW!! 2007 Turing Award given to pioneers of Model Checking: Articles in

topics , Schedule , Lecture material , Promela models , Examination , Homework Assignments , Course Material , Info on SPIN , Reference Material


Motivation Software systems are becoming an important part of the infrastructure of our society. Correctness and reliability have become issues of outmost importance. Testing and correction of software systems are irksome processes which typically consume half of the resources for system development. Thus, we need tools for analyzing software systems with the purpose of checking that they conform to their intended behavior, and for locating imperfections (``bugs'') that will cause run-time errors, security vulnerabilities, crashes, undelivered functionality, etc.

Topic This course concentrates on techniques to verify and find bugs in concurrent and parallel software systems. Problems that arise from the parallel execution of several threads, processes, or components are particularly hard to find a diagnose. In particular, the course teaches model checking. Model checking techniques can automatically analyze a pseudo-code description of a communication protocol, a concurrent algorithm, etc. and find all potential errors. The course will also cover the basics of structured testing for concurrent and parallel software.

Tool The material will be practically demonstrated with the tool SPIN. Spin supports a high level language to specify systems descriptions, called PROMELA (a PROcess MEta LAnguage). Spin has been used to trace logical design errors in distributed systems design, such as operating systems, data communications protocols, switching systems, concurrent algorithms, railway signaling protocols, etc. The tool checks the logical consistency of a specification. It reports on deadlocks, unspecified receptions, flags incompleteness, race conditions, and unwarranted assumptions about the relative speeds of processes. Spin can also be used to illustrate techniques in structured software testing.

This year we will direct particular attention to the analysis of concurrent multi-threaded algorithms. Such algorithms are used to make programs more performant on multiprocessor architectures. In e.g., the {\tt java.util.concurrent} package they are used to provide abstractions of common data structures (queues, sets, ...) which can be accessed concurrently by several threads.


The course will preliminarily cover the following topics. The course will use the
SPIN tool.


(The below schedule is copied from the
IT depts Schedule.
Week DateTimePlaceWhat
3 Wed20/115-171245Motivation, Overview of different verification techniques
Fri22/110-121245Modeling OBS! Flyttad
4 Mon25/113-151245SPIN: modeling exercise
Fri29/110-121245Temporal Logic
Fri29/113-151245Automata on infinite strings
5 Thu4/210-121245Modeling Exercise (Jonathan)
6 Tue9/213-151245Verification algorithms
7 Mon15/213-151245Exercise
Tue16/213-151245How to optimize models for verification
Fri19/208-101245concurrent algorithms and linearizability and Start of Project
9 Mon1/310-121245Not allocated
Mon1/313-151245Not allocated
Thu4/313-151245Guest Lecture: Jonathan Cederberg
Fri5/308-101245Not allocated
10 Mon8/310-121245Not allocated
Mon8/313-151245Not allocated
Tue9/313-151245problem solving
11 Mon15/308.00-13.00Gimogatan 4, Sal 1Final exam
23 Sat12/609.00-14.00PolacksbackenReexam
Office Hours: as you like, room 1435 and TBD

Lecture Material

Here are slides in some order (note that there is not a 1-1 correspondence between set of slides, and 2-hr lecture)

Promela models

Teaching staff


The following are part of examination

Homework Assignments

Course Material

The following will be given out As course or reference material, you can use
Other instructors are giving related courses. You can learn by looking at their material

SPIN: some information.