|
|
|
||
|
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)
|
|
||
|
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: Kučera Petr, RNDr., 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: Kučera Petr, RNDr., Ph.D. (30.04.2020)
|
|
||
|
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)
|
|
||
|
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.
The course is accompanied with a seminar. There will be tasks to exercise the taught material as well as implementation tasks based on the existent software libraries. Last update: T_KTI (04.05.2012)
|