Half-semester (the first half of the summer semester) introductory course to
automated verification by model checking. Students are encouraged to take
deductive verification course with Małgorzata Biernacka in the second half of
the semester.
Model checking is a collection of algorithmic techniques to verify (i.e.,
prove or disprove) if a given model of a computer system (software or
hardware) meets its formal specification. The specification is given as a
formula in temporal logic. In this course we want to introduce basic concepts
of the theory behind model checking.
Specifically, we are going to cover the following:
* temporal logics LTL and CTL
* explicit-state model checking
* symbolic model checking with ordered binary decision diagrams (OBDD)
* bounded model checking and reduction to SAT
