Course Info
Semantics & Verification, Spring 2005
Lecturer: Jiri Srba
(email: srba@cs.aau.dk, office:
B2-203)
Teaching Assistant:
Bjørn Haagensen
(email: bh@cs.aau.dk, office:
B2-205)
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 and
reactive systems. As part of the course material, we also introduce several
automatic verification tools, and hint at some of the implementation techniques underlying them.
The working language of the course will be English.
Reading Material: Most of the material has been collected in two compendiums
(Semantics & Verification 2004 by L. Aceto, and Semantics & Verification 2005 by J. Srba).
They can be bought for a good price at the bookshop in building B. I do recommend to
buy both of the compendiums. Some of the material is also available
on-line.
Exercises: The course consists of 15 lectures which will be accompanied by
tutorials. You will be split into two classrooms for the exercises and there will
a teaching assistant present for the whole tutorial. You are expected to form groups
of two or three students to discuss the exercises. These groups might change every time
and can be formed "randomly" in the beginning of each tutorial. For each tutorial
there will be a set of exercises to be solved. Try to discuss/compare your solutions
with your fellow student(s) in the groups. At any time you can ask the teaching assistant
for advice. You are supposed to prepare in advance for the tutorial by reading the
recommended material and by going through your own notes taken during the lectures.
Print the exercise sets before the tutorial, otherwise you will not know what to
work on. Some of the exercises will be marked with the star (*) sign. This means
that the exercise is a mandatory (and minimal) requirement to pass the exam. You are
strongly advised to pay enough attention to them as you will be asked to solve
one of the star exercises (but of course a different instance) during the preparation
time before your exam. Without being able to independently solve the task, you cannot
successfully pass the course.
Mini Projects: Twice during the semester, you will be asked to solve
two mini projects to demonstrate that you can use your theoretical knowledge to
model and verify a simple system using the verification tools CWB and UPPAAL. You will
be given 6 supervised hours for each mini project (two tutorial sessions and one
lecture block). The mini projects are supposed to be solved in
groups of two or three students and short reports should be delivered to the lecturer.
The solutions of different groups must be independent and sharing parts
of the code or the text of the report is strictly forbidden. The mini projects
are not mandatory, though the students are highly encouraged to hand in their
reports. A satisfactory solution of the mini project will give you a dispensation
from the exam syllabus. This means that if you demonstrate an active
knowledge of CWB and/or UPPAAL already during the semester, you will have
fewer questions to prepare for during the exam period! In case you decide not
to hand in the mini project reports during the semester, your exam pensum will be larger
as the mini project tasks will be contained in extra exam questions.
Exam: Individual and oral exam with preparation time. The exam will consist of
20 minute preparation time followed by 20 minutes of the actual examination. Topics
(including your personal instance of a star exercise) will be selected randomly.
You will first demonstrate a solution to your star exercise and then continue with
a presentation
of the selected topic. The outcome of the oral exam will be either pass or fail.
You can choose to give your presentation in English or Danish.
A detailed list of
exam questions
is here
and the main topics look as follows:
- Transition systems and CCS.
- Strong and weak bisimilarity, bisimulation games.
- Hennessy-Milner logic and bisimulation.
- Tarski's fixed-point theorem, Hennessy-Milner logic with recursively defined formulae, game characterization.
- Alternating bit protocol and its modelling and verification using CWB.
(Pensum dispensation for students who are on this list.)
- Timed automata, networks of timed automata and their semantics.
- Gossiping girls problem and its modelling and verification using UPPAAL.
(Pensum dispensation for students who are on this list.)
- Binary decision diagrams and their use in verification.
The required reading for the exam is summarized at the end of every lecture
on the Lectures Plan web-page. Any optional
(non-compulsary) reading is explicitly marked and you are also not required
to read the material that corresponds to the questions you got a dispensation
from.