Pavel Surynek's Home Page

Rozhodovací procedury a verifikace (NAIL094)

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, středa 15:40-17:10 S11 (přenáška) a 17:20-18:50 S10 (cvičení), Malá Strana, (začíná se 3.10.2012)
Úmluva: Proběhla 2.10.2012 na společné úmluvě KTIML.

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