|
Um die Zuverlässigkeit und Korrektheit von Programmen (oder auch von Schaltungen) zu garantieren, wird eine formale Verifikation benötigt. Die Durchführung eines mathematischen Korrektheitsbeweises ist jedoch im allgemeinen sehr aufwendig - insbesondere bei umfangreichen Algorithmen, wie sie in der Praxis eingesetzt werden. Aus diesem Grund wird versucht, die Aufgabe der Programmverifikation weitgehend zu automatisieren. In dem Seminar werden verschiedene Techniken und Systeme vorgestellt, um Korrektheitseigenschaften von Programmen rechnergestützt zu untersuchen.
Wird bei der Vorbesprechung bekanntgegeben und verteilt.
Theoretische Informatik, Informatik Vertiefung
Termine
| Montag, 18.02 | ||||
|---|---|---|---|---|
| Nr. | Uhrzeit | Thema | Referent | Betreuer |
| 1 | 09:30 - 10:30 | ACL2 | Thorsten Ottmann | Prof. Jürgen Giesl |
| 2 | 10:45 - 11:45 | KIV | Luan Ahmeti | Prof. Jürgen Giesl |
| 3 | 12:00 - 13:00 | Isabelle | Christian Haselbach | Darius Dlugosz |
| Pause | ||||
| 4 | 14:00 - 15:00 | Sparkle | Michael Spernat | Volker Stolz |
| 5 | 15:15 - 16:15 | Key | Markus Klinke | Prof. Jürgen Giesl |
| 6 | 16:30 - 17:30 | Java-Verifikation mit Isabelle | Achim Lücking | Darius Dlugosz |
| 7 | 17:45 - 18:45 | Proof-Carrying Code | Oliver Rattay | Volker Stolz |
| Dienstag, 19.02 | ||||
| 8 | 09:30 - 10:30 | ESC | Ingo Fliegen | Darius Dlugosz |
| 9 | 10:45 - 11:45 | Temporale Logik und Model-Checking | Anas Elisbihani | Benedikt Bollig |
| 10 | 12:00 - 13:00 | Symbolisches Model-Checking mit BBD's, SMV | Ibrahim Armac | Benedikt Bollig |
| Pause | ||||
| 11 | 14:00 - 15:00 | Model-Checking und Automaten, SPIN | Nicole Schneider | Benedikt Bollig |
| 12 | 15:15 - 16:15 | SLAM | Andreas Capellmann | Michael Weber |
| 13 | 16:30 - 17:30 | VeriSoft | Thomas Apel | Michael Weber |
|
|