Získanie základných teoretických poznatkov a návykov na samostatné využitie verifikačných metód. Kurz je zameraný tak, aby nadobudnuté znalosti uľahčovali prácu pri praktickom zostavovaní programov.

Rozdiel medzi testovaním a verifikáciou programov. Špecifikácia algoritmických úloh. Problém ukončenia práce programu. Konečnosť, čiastočná a úplná správnosť programu vzhľadom na špecifikáciu. Floydova metóda invariantov a klesajúcich parametrov. Hoareova axiomatická metóda pre jazyky typu Pascal. Problém automatizácie procesu vytvárania správneho programu na základe špecifikácie. Dokazovanie správnosti programu ako priebežná činnosť pri jeho návrhu. Prednáška obsahuje veľa konkrétnych príkladov a prakticých ukážok verifikácie programov.

Manna Z.: Matematická teória programov. Praha, SNTL 1981
Andrejková, G. – Chytil, M.: Verifikácia programov. UPJŠ Košice 1988
Apt, K. – Olderog, E.: Verification of Sequental and Concurrent Programs. Springer-Verlag New York 1997