Problém korektnosti, tedy problém ověření (neboli verifikace), že daný počítačový (hardwarový a/nebo softwarový) systém má skutečně vlastnosti, které jsou požadovány jeho specifikací, patří mezi fundamentální praktické i teoretické problémy v oblasti informatiky. Neustálý rozvoj informačních technologií vede k vytváření stále složitějších systémů, a tak nejen výzkumná, ale i průmyslová praxe se neobejde bez solidně vybudovaných verifikačních postupů. Jako jedna třída prakticky úspěšných metod se v devadesátých letech dvacátého století etablovala automatická verifikace zahrnující i tzv. `ověření modelu' (model checking); testovaná vlastnost systému se přitom vyjádří např. v jednoduché temporální logice a ověřuje se (polo)automatickými metodami na modelu systému. Účelem kursu je vysvětlení základních principů této (automatické) verifikace a zároveň demonstrace této verifikace na modelech konkrétních praktických problémů, pro něž jsou vhodné volně dostupné softwarové verifikační nástroje.