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.
Last update: 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.
Aim of the course -
Last update: 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.
Last update: 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ů
Course completion requirements -
Last update: 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)
Last update: 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)
Literature -
Last update: 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.
Last update: 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.
Syllabus -
Last update: 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
