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: mailem (již proběhla).

Rozvrh: zimní semestr, 2/2 Z+Zk, středa 12:20-13:50 S421 (přenáška) a 14:00-15:30 S421 (cvičení), Malá Strana, (začíná se 8.10.2014, S421 je chodba ÚFALu ve 4. patře)

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

---