Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

Seminar: Satisfiability Checking (S2, SS 2020)

Veranstalter

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Daniel Cloerkes, Stefan Dollase, Marcel Hark, Rebecca Haehn, Gereon Kremer, Dr. Stefan Schupp

Inhalt

Dieses Seminar beschäftigt sich mit der automatischen Überprüfung der Erfüllbarkeit (Satisfiability) von Formeln. Hierbei werden unterschiedliche Logiken betrachtet, z.B. reine Aussagenlogik, aber auch Erweiterungen wie Quantified Boolean Formulas oder SAT Modulo Theories. Es werden sowohl Techniken zur effizienten Überprüfung der Erfüllbarkeit angesprochen als auch praktische Anwendungen in der Programmverifikation vorgestellt.

Voraussetzungen

• Kenntnisse in Satisfiability Checking bzw. Programmverifikation oder verwandten Gebieten (z.B. "Erfüllbarkeitsüberprüfung", "Modellierung und Analyse hybrider Systeme", "Logikprogrammierung", "Funktionale Programmierung", "Termersetzungssysteme", "Model Checking", "Statische Programmanalyse", "Semantik und Verifikation von Software", etc.)
• Interesse an algorithmischen Fragestellungen und praktischen Anwendungen für logische Formalismen

Termine

Das Seminar wird als Blockseminar im Sommer 2020 durchgeführt.

Zuordnung

Theoretische Informatik

Rückfragen

Bitte wenden Sie sich an Marcel Hark.

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik