Pavel Surynek's Academic Page | Decision Procedures and Verification (NAIL094)

Decision Procedures and Verification (NAIL094)

General  |  Sources  |  Lecture  |  Seminar  |  Points  |  Notes     

Motivaní obrázek

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.


Rozvrh: zimní semestr, 2/2 Z+Zk, pátek 14:00-15:30 S11 (přenáška) a 15:40-17:10 S11 (cvičení), Malá Strana, (začíná se 9.10.2014)

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)  pdf   |   Přednáška v SISu