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.
Vorbesprechung: 25. November 2010, 16:00 - 17:00 Uhr
Die Vorbesprechung findet in Raum 2.01, Gebäde E1 7 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.
Vorläufiger Zeitplan
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.
Bitte melden sie sich auf unserer Registrierungsseite an. Das Proseminar ist auf 10 Teilnehmer beschränkt.
Anmeldeschluss: 19. November 2010
Bitte vergessen sie nicht, sich auch bei HISPOS anzumelden, da wir die Prüfungsanmeldung nicht automatisch vornehmen können.
Die Benotung erfolgt aufgrund des mündlichen Vortrags.
Die Scheine können bei Jennifer Müller (Raum 2.23, Gebäude E1 7) abgeholt werden.
TeX4PPT ist ein nützliches, kostenloses Tool zum Erstellen von math. Formeln in Powerpoint.
Präsentationsvorlagen: LaTeX (basierend auf dem 'Seminar'-Package), PowerPoint