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, SMT 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.

Úmluva: již proběhla ve středu 2.10.2013.

Rozvrh: ! POZOR PŘEROZVRŽENO ! zimní semestr, 2/2 Z+Zk, čtvrtek 10:40-12:10 S301 (přenáška) a 12:20-14:00 S301 (cvičení), Malá Strana, (začíná se 9.10.2013)

Regular lectures on 31-10-2013 and 7-10-2013 will be canceled due to attendance of a conference by the lecturer.

Teaching in English: The lecture will be taught in English if required (study materials in English will be provided).

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