Introduction to Concurrency and Verification, Summer semester 2010/2011

Department of Computer Sciences, University of Salzburg

Lecturer:      Dr. A. Sokolova, ana.sokolova"at"cs.uni-salzburg.at, office 2.17

Schedule:      Thursdays 10am-12am, 1pm-2pm, room T06

First meeting:    Tuesday, 1.3.2011, 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 Hennessy-Milner logic.
Literature:
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 July/August. 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: First exam possibility: Thursday 7.7.11, 10am, T06. Second exam possibility: Thursday 14.7.11, 10am, T06. If needed there will be a third exam possibility in the middle of August.
Mini project: t.b.a.
Schedule: