Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

Seminar: Satisfiability Checking (S2, WS 2009/2010)

Veranstalter

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Xin Chen, Fabian Emmes, Carsten Fuhs, Nils Jansen, Ulrich Loup, Carsten Otto

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 Formulae oder SAT Modulo Theories. Es werden sowohl Techniken zur effizienten Überprüfung der Erfüllbarkeit angesprochen als auch praktische Anwendungen in der Programmverifikation vorgestellt.

Weitere Details und aktuelle Informationen finden Sie auf der entsprechenden englischsprachigen Webseite zu diesem Seminar.

Termine

Das Seminar wird voraussichtlich als Blockseminar am Ende der Vorlesungszeit durchgeführt.

Voraussetzungen

• Kenntnisse in Satisfiability Checking bzw. Programmverifikation oder verwandten Gebieten (z.B. "Erfüllbarkeitsüberprüfung", "Modellierung und Analyse hybrider Systeme", "Termersetzungssysteme", "Grundlagen der funktionalen Programmierung", "Logikprogrammierung", "Automatisierte Programmverifikation")
• Interesse an algorithmischen Fragestellungen und praktischen Anwendungen für logische Formalismen

Themen

Zuordnung

Theoretische Informatik, Informatik Vertiefung

Rückfragen

Bitte wenden Sie sich an Carsten Fuhs.

Weitere Details und aktuelle Informationen finden Sie auf der entsprechenden englischsprachigen Webseite zu diesem Seminar.

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik