Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2014 / Automatisches Beweisen


Inhaltsbereich

Automatisches Beweisen

Seminar, Hofmann, Jost, Schöpp

Aktuelles


Inhalt

Automatische Verfahren zur Lösung von Entscheidungsproblemen (Entscheidungsverfahren, Decision Procedures) erfreuen sich in der Programmverifikation, dem automatischen Beweisen und der Programmsynthese zunehmender Beliebtheit. Das liegt daran, dass im Zuge der Verfügbarkeit höherer Rechenleistung bisher für praktisch nicht durchführbar gehaltene Verfahren, zum Beispiel für das SAT-Problem (aussagenlogische Erfüllbarkeit), implementiert wurden und aufgrund der damit erzielten Erfahrungen signifikant verbessert wurden. Im Zuge dieser Entwicklung entstanden auch neue Entscheidungsverfahren, etwa "Satisfiability modulo theories". Im Seminar wollen wir das vor kurzem erschienene einschlägige Lehrbuch

   Kroening, Strichman
   "Decision Procedures"
   Springer-Verlag, 2008

durcharbeiten. Dieses behandelt neben den Verfahren für das SAT-Problem auch Entscheidungsverfahren für Lineare Arithmetik, Bitvektoren, das Omega-Verfahren für ganzzahlige Arithmetik. Falls gewünscht, können auch weitere Themen angeboten werden, z.B. zur reellen nichtlinearen Arithmetik oder zu symbolischen Verfahren in der Computeralgebra.    


Themen

Die Vortragsthemen werden in einer Vorbesprechung zu Beginn des Semesters vergeben.

 


Organisation

Anforderungen

  • Blitzvortrag 90 Sekunden: Inhaltsübersicht, eine Folie
  • Vortrag: 30 Minuten (plus Diskussion)
  • Anwesenheit während der Seminarsitzungen
  • Ausarbeitung zum Thema
    • 7000-14000 Zeichen
    • Bei Master- und Diplomstudenten werden die Anforderungen mit den Betreuern abgesprochen.

Zeit und Ort

  • Zeitplan und Themen werden in einer Vorbesprechung mit den Teilnehmern zu Beginn des Semesters festgelegt.

 


Themen

  1. Aussagenlogik & SAT-Solver
    • Bearbeitet von: Kevin Hanel
    • Betreuer: St. Jost
  2. Gleichungslogik & uninterpretierte Funktionssymbole
    • Bearbeitet von: Julian Jorczik
    • Betreuer: U. Schöpp
  3. Entscheidungsverfahren für 2.
    • Bearbeitet von: Jakob Schuster
    • Betreuer: U. Schöpp
  4. Lineare Arithmetik: Definition und Simplex-Algorithmus
    • Bearbeitet von: Michael Fromm
    • Betreuer: St. Jost
  5. Lineare Arithmetik: Fourier-Motzkin-Elimination, Omega-Test
    • Bearbeitet von: Felix Reihl
    • Betreuer: M. Hofmann
  6. Pointer Logic
    • Bearbeitet von: Habib Awada
    • Betreuer: M. Hofmann
  7. Kombination von Theorien: Nelson-Oppen-Prozedur
    • Bearbeitet von: Aigerim Zhuankhan
    • Betreuer: M. Hofmann
  8. SMT (SAT-Solver über einer beliebigen Theorie)
    • Bearbeitet von: Veronika Bader
    • Betreuer: St. Jost

 


Organisation

Zeitplan (vorläufig)

  • Blitzvorträge: 14.5., 14:00h, L109
  • Erstes Treffen mit Betreuer: bis 31.5.
  • Abgabe Ausarbeitung: 14.6.
  • Abgabe Reviews: 21.6.
  • Seminar: 2.7. 12:00h ct
  • Abgabe Ausarbeitung (Endfassung): 16.7.

Anforderungen

  • Blitzvortrag 90 Sekunden: Inhaltsübersicht, eine Folie
  • Vortrag: 30 Minuten (plus Diskussion)
  • Anwesenheit während der Seminarsitzungen
  • Anwesenheit während der Seminarsitzungen
    • 7000-14000 Zeichen
    • Bei Master- und Diplomstudenten werden die Anforderungen mit den Betreuern abgesprochen.

 


Weitere Informationen

Tipps zum Aufbau von Vorträgen und zu Präsentationstechniken:

 

Artikelaktionen


Funktionsleiste