Satisfiability Checking (SS 2019)

Seminar:
Satisfiability Checking
(S2, SS 2019)
LuFG Informatik 2

Veranstalter

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

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")
Interesse an algorithmischen Fragestellungen und praktischen Anwendungen für logische Formalismen

Termine

Das Seminar wird als Blockseminar am 01.08.2019 in unserem Seminarraum (4201b) durchgeführt. durchgeführt. Die Vorbesprechung fand am 4.April um 10:30 in 5055 statt. Es gelten folgende Fristen

Bis 19 April: Betreuende kontaktieren und Literatur besprechen.
Bis 25 April: Spätester Rücktritt vom Seminar ohne es nicht zu bestehen.
Bis 17 Mai: Konzeption des Vortrags mit Betreuenden absprechen.
Bis 14 Juni: Vollständige Ausarbeitung muss vorliegen.
Bis 18 Juli: Folien zur Kontrolle abgeben.
Bis 25 Juli: Finale Ausarbeitung einreichen.

Themen

Titel	Literatur	Betreuung	Student
Linear Optimization via SMT	Link	Rebecca Haehn	Dennis Prudlik
Verification of Neural Networks	Link	Prof. Dr. Erika Ábrahám	David Klüner
Termination of Triangular Integer Loops is Decidable	N.N.	Prof. Dr. Jürgen Giesl	Eric Skaliks
Proving termination of imperative programs using Max-SMT	Link	Stefan Dollase	Kai Liehr
Answer Set Programming Based on Propositional Satisfiability	Link	Jera Hensel	Dinh-An Ho

Die Ausarbeitung inkl. Deckblatt darf nicht mehr als 10 Seiten umfassen, wobei das Layout in etwa dem der Vorlage entsprechen muss. Die Vortragsdauer beträgt 25 Minuten..

Vorlagen

Latex-Vorlagen für die Ausarbeitung finden Sie hier.

Zuordnung

Theoretische Informatik

Rückfragen

Bitte wenden Sie sich an Marcel Hark.

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

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

Seminar: Satisfiability Checking