Automated verification (Q1)

Język wykładowy Angielski
Semestr Letni
Status W ofercie
Opiekun Witold Charatonik
Liczba godzin 15 (wyk.) 15 (ćw.)
Rodzaj I2.T - teoria inf.
Polecany dla I roku No
Egzamin Yes
Tagi JP (języki programowania i logika)

Opis przedmiotu:

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