PředmětyPředměty(verze: 861)
Předmět, akademický rok 2019/2020
  
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 2019 do 2019
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: vyučován
Jazyk výuky: čeština, angličtina
Způsob výuky: prezenční
Další informace: http://ktiml.mff.cuni.cz/~kucerap/satsmt/
Garant: RNDr. Petr Kučera, 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.
Cíl předmětu -
Poslední úprava: RNDr. Petr Kučera, Ph.D. (30.04.2020)

Cílem předmětu je seznámit studenty se základními principy, které se používají při řešení SAT/SMT a souvisejících problémů

Podmínky zakončení předmětu -
Poslední úprava: RNDr. Petr Kučera, Ph.D. (30.04.2020)

Předmět je zakončen zápočtem a zkouškou. K udělení zápočtu je třeba získat dostatečný počet bodů řešením domácích úkolů. Zkoušku je možné splnit dvěma způsoby. Jedním je ústní zkouška, která s ohledem na situaci může probíhat i distančně. Druhou možností je získání vyššího počtu bodů řešením domácích úkolů za podmínek, které jsou přesněji popsány na stránkách k předmětu (http://ktiml.mff.cuni.cz/~kucerap/satsmt/index-en.php)

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