Introduction to Concurrency and Verification, Winter semester 2007/2008

Department of Computer Sciences, University of Salzburg

Lecturer:      Dr. A. Sokolova, ana.sokolova"at", office 2.17 (maybe sometimes Prof. C.M. Kirsch)

Schedule:      Tuesdays 3pm-5pm, Wednesdays 2pm-3pm

First meeting:    Tuesday, 2.10.2007, 2pm, room T06

Language:      English

The course may also be taken by PhD students

Course description: The aim of this course is to introduce advanced mathematical models for the formal description and analysis of programs, with emphasis on parallel, reactive systems. The course consists of 3 hours lectures per week and lasts for about 15 weeks. It deals with semantic models for parallel systems, and logics for the description of their properties. As part of the course material, we will also introduce automatic verification tools, and hint at some of the implementation techniques underlying them. The teaching consists of lectures interspersed with exercises.

Via this course a practicaly oriented student learns the need of abstraction, formal specification and verification; the student interested in theory gets a solid introduction to formal methods for specification and verification. In particular, we will: model simple systems using transition systems and (CCS) process expressions, deal with various notions of behaviour equivalences, learn the need of abstraction, formulate (and verify) properties of systems in Hennessi-Milner logic.

What is this theory good for? A typical question asked by (practically oriented) students. The authors of the book Reactive Systems have compiled a nice webpage answering this question. Click on the corresponding link on the left to get to the needed subpage.

Prerequisites: None, the course material is self-contained, as is the textbook and the scriptum. Knowledge of basics of theoretical computer science like logic for computer science or automata theory is an asset.

Exam: This is a VP course. There will be three exam possibilities in February/March. The exam is written consisting of several excersises from the material covered during the course (we will do an open-book exam). Additionally, the homeworks and the mini project, will also contribute to the final grade. (mini project = 25%, homeworks = 10%, exam - the rest)
Exam dates: Tuesday, 29.1.2008, during classes, duration 2-3 hours. Thursday, 14.2.2008, 10 am, duration 2-3 hours. Wednesday, 5.3.2008, 2pm, duration 2-3 hours.
Mini project: The description of the mini project is given in the following pdf file.

Results from the exam(s) and homeworks
Student ID Exam points (<= 100) HW points (*)(<= 11) Project points (<= 25) Total (mark) (**) Exam date
****240 96 9 25 1 29.1.8
****949 93 7 25 1 29.1.8
****744 90 1 20 1 29.1.8
****112 80 11 25 1 29.1.8
****016 75 6 25 1 29.1.8
****173 68 8 25 1 29.1.8
****810 56 6 20 3 29.1.8
****433 - 3 20 5 -

(*) There were 11 homeworks. Each delivered homework counts as one HW point.
(**) Total = Exam points + HW points + Project points. The final mark is given according to the following rules: 1 (Total >= 100), 2 (85<= Total < 100), 3 (70 <= Total < 85), 4 (60 <= Total < 70), 5 (Total < 60)

Exam problems from 29.1.8