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.
Poslední úprava: T_KTI (04.05.2012)
A course on logic theories and procedures for deciding satisfiability in
these theories with emphasis on the application in program verification.
Construction of an efficient SAT solver (DPLL, conflict-directed clause
learning), local algorithms for satisfiability (WalkSAT, survey
propagation), decisions in logic with equality, uninterpreted functions and
pointers, quantified Boolean formulae (QBF), combining logic theories,
SAT-modulo solvers.
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ů
Poslední úprava: RNDr. Petr Kučera, Ph.D. (30.04.2020)
The goal of the lecture is to introduce students with the basic principles and techniques used in SAT/SMT solving and related problems.
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)
Poslední úprava: RNDr. Petr Kučera, Ph.D. (30.04.2020)
The course is finished with obtaining the credit and passing the exam. The credit is given for getting enough points for the homework assignments given during the semester. The exam can be passed in two ways. One possibility is to pass an oral exam which can proceed remotely depending on the current situation. The other option is to solve enough homework assignments, the conditions of this way of passing exam is described in more details at the course web pages (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.
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.
Poslední úprava: T_KTI (04.05.2012)
A course on logic theories and procedures for deciding satisfiability in
these theories with emphasis on the application in program verification.
Construction of an efficient SAT solver (DPLL, conflict-directed clause
learning), local algorithms for satisfiability (WalkSAT, survey
propagation), decisions in logic with equality, uninterpreted functions and
