PředmětyPředměty(verze: 837)
Předmět, akademický rok 2018/2019
   Přihlásit přes CAS
Rozhodovací procedury a verifikace - NAIL094
Anglický název: Decision Procedures and Verification
Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2018
Semestr: letní
E-Kredity: 6
Rozsah, examinace: letní s.:2/2 Z+Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: nevyučován
Jazyk výuky: čeština
Způsob výuky: prezenční
Další informace: http://d3s.mff.cuni.cz/teaching/decision_procedures/
Garant: prof. RNDr. Roman Barták, Ph.D.
Třída: Informatika Mgr. - volitelný
Kategorizace předmětu: Informatika > Teoretická informatika
Anotace -
Poslední úprava: T_KTI (04.05.2012)
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.
Literatura -
Poslední úprava: T_KTI (04.05.2012)

Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View. Springer, 2008.

Aaron R. Bradley, Zohar Manna: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.

Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. The MIT Press, 2008.

Edmund M. Clarke Jr., Orna Grumberg, Doron A. Peled: Model Checking. The MIT Press, 1999.

Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of

Satisfiability, IOS Press, 2009.

Sylabus -
Poslední úprava: T_KTI (04.05.2012)

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.

 
Univerzita Karlova | Informační systém UK