Rozhodovací procedury a verifikace

Sylabus

Přednáška o logických teoriích a procedurách rozhodujících splnitelnost v těchto teoriích s důrazem na aplikaci při verifikaci programů. Konstrukce efektivního SAT

řešiče (DPLL, conflict-directed clause learning), lokální algoritmy splnitelnosti (WalkSAT, survey propagation), rozhodování v logice s rovností, s neinterpretovanými funkcemi a ukazateli, rozhodování ve výrokové logice s kvantifikátory (QBF), kombinování logických teorií, SAT-modulo

řešiče.

Přednáška je doplněna cvičením. Mimo klasických úloh na procvičení látky se budou řešit také implementační úlohy pomocí existujících softwarových knihoven.

Anotace

Přednáška o logických teoriích a procedurách rozhodujících splnitelnost v těchto teoriích s důrazem na aplikaci při verifikaci programů. Konstrukce efektivního SAT

řešiče (DPLL, conflict-directed clause learning), lokální algoritmy splnitelnosti (WalkSAT, survey propagation), rozhodování v logice s rovností, s neinterpretovanými funkcemi a ukazateli, rozhodování ve výrokové logice s kvantifikátory (QBF), kombinování logických teorií, SAT-modulo

řešiče.