Předmět Rozhodovací procedury a verifikace (NAIL094)
Na serveru studentino.cz naleznete nejrůznější studijní materiály: zápisky z přednášek nebo cvičení, vzorové testy, seminární práce, domácí úkoly a další z předmětu NAIL094 - Rozhodovací procedury a verifikace, Matematicko-fyzikální fakulta, Univerzita Karlova v Praze (UK).
Top 10 materiálů tohoto předmětu
Materiály tohoto předmětu
| Materiál | Typ | Datum | Počet stažení |
|---|
Další informace
Sylabus
Přednáška o logických teoriích a procedurách rozhodujících splnitelnost vtěchto teoriíchs důrazem na aplikaci při verifikaci programů. Konstrukce efektivního SATřešiče (DPLL, conflict-directed clause learning), lokální algoritmysplnitelnosti (WalkSAT, survey propagation), rozhodování v logice srovností, 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 sebudou řešit také implementační úlohy pomocí existujících softwarovýchknihoven.
Literatura
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 ofSatisfiability, IOS Press, 2009.
Garant
RNDr. Pavel Surynek, Ph.D.