Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society

Proseminar "Das Erfüllbarkeitsproblem SAT (2) 5LP" (WS 2012/2013), Vorlesungsnummer: 67260

Dozenten


Inhalt

Viele Probleme in der Hard- und Softwareverifikation können durch aussagenlogische Formeln modelliert werden. Das Verifikationsproblem entspricht dann dem Erfüllbarkeitsproblem (satisfyability problem, SAT) der aussagenlogischen Formeln. Daher sind effiziente Lösungsverfahren für SAT in der Praxis von großer Bedeutung. In diesem Proseminar besprechen wir die Theorie, Algorithmen und Anwendungen von SAT.


Start

Vorbesprechung: 16. Oktober 2012, 16:00 - 17:00 Uhr

Die Vorbesprechung findet in Raum 630, Gebäde E1 5 statt. Alle Themen werden dabei von uns vorgestellt. Sie erhalten dann die Möglichkeit, sich ein Vortragsthema auszusuchen und mit Ihrem Betreuer in Kontakt zu treten.


Wo und Wann?

Vorläufiger Zeitplan


Voraussetzungen

Kenntnisse in theoretischer Informatik, insbesondere Logik sind nützlich aber keine Zulassungsvoraussetzung. Wir werden eine Einführung in SAT geben. Sie müssen englische Fachaufsätze lesen können. Die Vorträge können in deutscher Sprache gehalten werden, wir begrüssen es jedoch wenn der Vortrag auf englisch gehalten wird.


Literatur


Anmeldung

Bitte melden sie sich auf unserer Registrierungsseite an. Das Proseminar ist auf 10 Teilnehmer beschränkt.

Anmeldeschluss: 16. Oktober 2012

Bitte vergessen sie nicht, sich auch bei HISPOS anzumelden, da wir die Prüfungsanmeldung nicht automatisch vornehmen können.


Benotung

Die Benotung erfolgt aufgrund des mündlichen Vortrags.


Verschiedenes

TeX4PPT ist ein nützliches, kostenloses Tool zum Erstellen von math. Formeln in Powerpoint.

Sie können folgende Präsentationsvorlagen verwenden, können aber auch gerne ihre eigene erstellen: LaTeX (basierend auf dem 'Seminar'-Package), PowerPoint