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

Kurzfassung:

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.

Lernziele:

The students learn essential decision procedures for fragments of first order logic.

Lehrinhalte:

Algorithms, heuristics and modern implementations of decision procedures.

Weitere Voraussetzungen:

Basic knowledge in logic.

Prüfungsleistung:

Oral exam over 30 minutes

Lehr- und Lernmethoden:

Students are provided with exercise sheets that are discussed during exercise sessions.

Verwendbarkeit:

Literatur:

D. Kröning, O. Strichman: Decision Procedures - An Algorithmic Point of View (Springer, 2008)

Verweise:

Kommentar: