Viele Programmeigenschaften lassen sich vollautomatisch mit teils sehr effizienten Entscheidungsverfahren untersuchen. Solche "Push-Button"-Verifikationstechniken sind ohne großen Zeitaufwand einsetzbar und erfordern keine entsprechende Schulung der Benutzer. Sie werden daher in immer stärkerem Maße in der Industrie verwendet. In diesem Seminar sollen verschiedene solche Verfahren (für unterschiedliche Probleme bei der Zuverlässigkeit von Programmen und Systemen) vorgestellt werden.
Wird bei der Vorbesprechung bekanntgegeben und verteilt.
Theoretische Informatik, Informatik Vertiefung
Prof. Dr. Jürgen Giesl, Tel: 80-21230, E-Mail: giesl@informatik.rwth-aachen.de
Termine
Freitag, 20.07 | ||||
---|---|---|---|---|
Nr. | Uhrzeit | Thema | Referent | Betreuer |
1 | 13:00 - 14:00 | Binary Decision Diagrams | Martin Thomas | Prof. Jürgen Giesl |
2 | 14:15 - 15:15 | Davis-Putnam Algorithmus | Khai-Binh Duong | Prof. Jürgen Giesl |
3 | 15.30 - 16:30 | Stalmarck's Prozedur | Markus Grohs | Darius Dlugosz |
Montag, 23.07 | ||||
4 | 11:00 - 12:00 | Temporale Logik und Model-Checking | Oliver Specht | Martin Leucker |
5 | 12:15 - 13:15 | Model-Checking und Automaten, SPIN | Steffen Offermann | Darius Dlugosz |
Pause | ||||
6 | 15:00 - 16:00 | Monadische Logik 2.Ordnung | Stephan Küpper | Benedikt Bollig |
7 | 16:15 - 17:15 | Presburger Arithmetik | Marc-Oliver Westerburg | Benedikt Bollig |
|