Nová 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. Mimo klasických úloh na procvičení látky se budou řešit také implementační úlohy pomocí existujících softwarových knihoven pro vývoj rozhodovacích procedur.

Rozvrh: zimní semestr, 2/2 Z+Zk, středa 12:20, Malá Strana, chodba S300 (začíná se 7. 10. 2009)
Úmluva: Již proběhla.

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

Zkoušku z Rozhodovacích procedur a verifikace je možno složit také prakticky, tj. naimplementováním vybrané rozhodovací procedury (výběr je nutno zkonzultovat). Hodnocení bude v takovém případě zohledňovat správnost a kvalitu implementace.

Termíny zkoušek (standardních i praktických) jsou vypsané v SISu.