Výběrová přednáška o logických teoriích a procedurách rozhodující splnitelnost v těchto teoriích s důrazem na aplikaci při verifikaci programů. Na přednášce se bude probírat: rozhodovací procedury pro výrokovou logiku (DPLL, BDD) logické teorie pro rovnost, lineární aritmetiku, bitové vektory, pole a ukazatele kombinování rozhodovacích procedur ověřování korektnosti programů

Přednáška je doplněna cvičením. V rámci cvičení bude možné mimo klasických úloh na procvičení látky řešit také úlohy implementačního charakteru..

Rozvrh: zimní semestr, 2/2 Z+Zk, čtvrtek 14:00-15:30 (přenáška) a 15:40-17:10 (cvičení), Malá Strana, S11 (začínat se bude vždy o 10 minut později)
Úmluva: Proběhla 30.9.2010 na společné úmluvě KTIML.

Plakát přednášky (reklama na úmluvu)    |   Přednáška v SISu

Zkoušku z Rozhodovacích procedur a verifikace je možno skládat ústně/písemně (písemná příprava, případně ústní doplnění písemné přípravy) ovšem také prakticky, tj. naimplementováním vybrané rozhodovací procedury (výběr je nutno zkonzultovat, nemusí se nutně jednat o proceduru probíranou na přednášce). Hodnocení bude v takovém případě zohledňovat správnost a kvalitu implementace.

Termíny zkoušek budou vypsané v SISu. Zkoušení praktickou formou se konat nebude.