Modulcode: | Inf-EntVerf |
Englische Bezeichnung: | Decision Procedures |
Modulverantwortliche(r): | Prof. Dr. Dirk Nowotka |
Turnus: | unregelmäßig (WS13/14 WS15/16 WS16/17 WS17/18 WS18/19) |
Präsenzzeiten: | 2V 2Ü |
ECTS: | 6 |
Workload: | 30 Std. Vorlesung, 30 Std. Präsenzübung, 120 Std. Selbststudium |
Dauer: | ein Semester |
Modulkategorien: | WI (MSc Inf (15)) WI (MSc WInf (15)) WI (MEd Inf) WPI (MEd Inf) IG (MSc Inf) IS (MSc Inf) MV (MSc Inf) |
Lehrsprache: | Englisch |
Voraussetzungen: | Inf-LogInf |
In this course we deal with essential decision procedures and their applications. Decision procedures for the satisfiability problem for various logics, SAT-, SMT, and QBF-solvers, are introduced. Such procedures constitute a technological foundation for applications in the field of software verification. We consider algorithmic aspects, heuristics and modern implementations of those.
The students learn essential decision procedures for fragments of first order logic.
Algorithms, heuristics and modern implementations of decision procedures.
Basic knowledge in logic.
Oral exam over 30 minutes
Students are provided with exercise sheets that are discussed during exercise sessions.
D. Kröning, O. Strichman: Decision Procedures - An Algorithmic Point of View (Springer, 2008)