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ů