RWTH Leitseite

Seminar: Verifikation von Programmen


Veranstalter

Prof. Dr. Jürgen Giesl, Benedikt Bollig, Darius Dlugosz, Volker Stolz, Michael Weber

Das Seminar wird als Blockseminar am Ende der Vorlesungszeit (Mo. 18.02.02, Di. 19.02.02) veranstaltet.


Inhalt

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.



Literatur

Wird bei der Vorbesprechung bekanntgegeben und verteilt.


Zuordnung

Theoretische Informatik, Informatik Vertiefung



Termine
Montag, 18.02
Nr.UhrzeitThemaReferentBetreuer
109:30 - 10:30ACL2Thorsten OttmannProf. Jürgen Giesl
210:45 - 11:45KIVLuan AhmetiProf. Jürgen Giesl
312:00 - 13:00IsabelleChristian HaselbachDarius Dlugosz
Pause
414:00 - 15:00SparkleMichael SpernatVolker Stolz
515:15 - 16:15KeyMarkus KlinkeProf. Jürgen Giesl
616:30 - 17:30Java-Verifikation mit IsabelleAchim LückingDarius Dlugosz
717:45 - 18:45Proof-Carrying CodeOliver RattayVolker Stolz
Dienstag, 19.02
809:30 - 10:30ESCIngo FliegenDarius Dlugosz
910:45 - 11:45Temporale Logik und Model-CheckingAnas ElisbihaniBenedikt Bollig
1012:00 - 13:00Symbolisches Model-Checking mit BBD's, SMVIbrahim ArmacBenedikt Bollig
Pause
1114:00 - 15:00Model-Checking und Automaten, SPINNicole SchneiderBenedikt Bollig
1215:15 - 16:15SLAMAndreas CapellmannMichael Weber
1316:30 - 17:30VeriSoftThomas ApelMichael Weber

Last modified: Wed Feb 13 13:25:09 CET 2002 / Darius Dlugosz / Lehr- und Forschungsgebiet Informatik II
RWTH Aachen