Formal verification 1000-2M25WER
1. Temporal logic model-checking of finite-state reactive systems. Temporal logics (LTL, CTL, CTL*), Büchi automata.
2. Symbolic model checking with BDDs. Partial order reduction.
3. Proving termination of programs with the size-change termination principle (SCP).
4. Verification of continuous-time systems with timed automata.
5. Stochastic model-checking: Verification of discrete and continuous-time Markov chains.
6. Infinite-state model-checking: Verification of recursive programs with pushdown automata. Verification of communicating protocols with channel
systems. Parametrised verification.
7. Hardware model-checking: Verification of combinational and sequential circuits.
8. Synthesis of finite-state programs: Church’s problem and the Büchi-Landweber’s theorem. Ramadge and Wonham’s control of discrete event systems.
Type of course
Prerequisites
Course coordinators
Assessment criteria
The evaluation is based on homeworks during the duration of the course and a final oral exam.
Bibliography
Lecture slides and selected chapters from the following
books:
- Model Checking by Clarke, Grumberg, and Peled (1, 2)
- Principles of Model Checking by Baier and Katoen (1, 2, 4, 5)
- Handbook of Model Checking by Clarke, Henzinger, Veith, and Bloem (1, 2,
4, 5, 6, 8)
- Handbook of Automata Theory (8)
- Program termination analysis in polynomial time by Ben-Amram and Lee (3)
- Introduction to Formal Hardware Verification by Kropf (7)
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: