PředmětyPředměty(verze: 901)
Předmět, akademický rok 2022/2023
  
Rozhodovací procedury a verifikace - NAIX094
Anglický název: Decision Procedures and Verification
Zajišťuje: Studijní oddělení (32-STUD)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 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
Virtuální mobilita / počet míst: ne
Stav předmětu: vyučován
Jazyk výuky: čeština
Způsob výuky: prezenční
Je zajišťováno předmětem: NAIL094
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
Prerekvizity : {NXXX036, NXXX037, NXXX038, NXXX039, NXXX040, NXXX067, NXXX069}
Neslučitelnost : NAIL094
Záměnnost : NAIL094
Je neslučitelnost pro: NAIL094
Je záměnnost pro: NAIL094
Výsledky anket   Termíny zkoušek   Rozvrh   Nástěnka   
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