Introduction to Concurrency and Verification, Summer semester 2010/2011
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
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.
- Recent textbook: Reactive Systems: Modelling, Specification and Verification by
Luca Aceto, Anna Ingolsfdottir,
Kim G. Larsen and Jiri Srba. Cambridge University Press, 2007. Check the publishers web page
here. The book can also be ordered
via Amazon.co.uk . Several copies are available at the department library.
- Scriptum: Introduction to Process Theory, by Kees
Middelburg and Michel Reniers, Technische Universiteit Eindhoven 2004, available here.
- Additional literature links will also be assembled here as needed, during the semester.
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.
- Week 2, Thursday 10.3.11: Introduction to reactive systems, LTS, CCS informally (for sequential processes).
Book - up to page 13 and Section 2.2.1 (LTS), scriptum - up to page 22 (Sections 1.1.-1.4.).
- Week 3, Thursday 17.3.11: CCS informally, continued. Formal syntax and semantics of CCS. Examples.
Book: pages 21 - 28.
- Week 4, Thursday 24.3.11: Behaviour relations: isomorphism, trace equivalence. Examples.
Book: pages 28 - 35, scriptum: pages 22 - 29 (Section 1.5).
- No class on Thursday 31.3.11 (conference), we will schedule an additional replacement class.
- Week 5, Thursday 7.4.11: Behaviour relations continued, strong bisimilarity.
Book: pages 35 - 45.
- Week 6, Thursday 14.4.11: Properties of bisimilarity.
Book: pages 45-49, scriptum: pages 29 - 40.
- No class on Thursday 21.4.11 (Easter break).
- No class on Thursday 28.4.11 (Easter break).
- Week 7, Thursday 5.5.11: Counters, buffers, meaningful examples. Game characterization of bisimilarity.
Book: pages 50 - 53 and 65 - 70.
- Week 8/9, (additional class) Tuesday 10.5.11: Weak bisimulation, game characterization. Book: pages 53 - 65 and 70 - 72.
(regular class) Thursday 12.5.11: Fixed points and bisimilarity, computing bisimilarity. Book: pages 75 - 87.
- Week 10, Thursday 19.5.11: Computing bisimilarity (continued), Hennessy-Milner logic. Book: pages 87 - 96.
- No class on Thursday 26.5.11 (conference), we will schedule an additional replacement class.
- No class on Thursday 2.6.11 (holiday).
- Week 11, Thursday 9.6.11: Expressivity of Hennessy-Milner logic. Book: pages 96 - 104.
- Week 12, Thursday 16.6.11: Hennessy-Milner logic with recursion. Book: pages 104 - 115.
- Week 13, (additional class) Tuesday 21.6.11, 1pm-4pm, T06: Game characterization of Hennessy-Milner logic, characteristic properties.
Book: pages 115 - 134.
- No class on Thursday 23.6.2011 (holiday).
- Week 14, Thursday 30.6.11: last class, one hour on mixing largest and least fixed points.
Book: pages 134-139. Two hours on example exam problems, questions and answers.