SubjectsSubjects(version: 916)
Course, academic year 2022/2023
   Login via CAS
Decision procedures and SAT/SMT solvers - NAIL094
Title: Rozhodovací procedury a SAT/SMT řešiče
Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty: Faculty of Mathematics and Physics
Actual: from 2020
Semester: summer
E-Credits: 5
Hours per week, examination: summer s.:2/2, C+Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
Virtual mobility / capacity: no
State of the course: taught
Language: Czech, English
Teaching methods: full-time
Additional information: http://ktiml.mff.cuni.cz/~kucerap/satsmt/index-en.php
Guarantor: RNDr. Petr Kučera, Ph.D.
Class: Informatika Mgr. - volitelný
Classification: Informatics > Theoretical Computer Science
Incompatibility : NAIX094
Interchangeability : NAIX094
Is incompatible with: NAIX094
Is interchangeable with: NAIX094
Annotation -
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.
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.

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)

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.

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

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.

 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html