[ LVAs 185/2 | Abteilung 185/2 | Institut 185 | Informatik | TU Wien | Server home page ]
Lehrveranstaltungsleiter: Gernot Salzer, salzer@logic.at
Diese Lehrveranstaltung ist Teil des Wahlfachs "AI und theoretische Informatik" des Studiums Informatik.
Jeder Computerbenutzer kennt Softwarefehler: Textverarbeitungsprogramme, Spiele, ja ganze Betriebssysteme stürzen unvermutet ab oder liefern unvorhergesehene Resultate. Während derartige Phänomene im Privat- und Bürobereich meist nur ärgerlich sind und keine großen Schäden verursachen, gibt es eine Reihe von Anwendungen, bei denen Programmfehler teure Produktionsausfälle, Image- und Kundenverlust oder gar Katastrophen zur Folge haben können, etwa bei der Steuerung von Fertigungsstraßen, Eisenbahnen oder Flugzeugen. Aus diesem Grund wird bei kritischen Anwendungen in zunehmendem Maße die formale Verifikation der Hard- und Software gefordert, um die Fehlerfreiheit hinsichtlich einer gegebenen Spezifikation nachzuweisen.
In diesem Seminar werden Methoden zur Verifikation sequentieller, paralleler und verteilter Programme besprochen, die auf den Arbeiten von Hoare, Dijkstra und Gries basieren. Das Seminar stellt eine Vertiefung und Erweiterung des in der Vorlesung Einführung in die Theorie der Informatik eingeführten Hoare-Kalküls dar; es gehört damit einerseits in den Bereich der Programmiersprachen und baut andererseits auf Begriffen der mathematischen Logik auf.
Das Seminar findet jeden Dienstag, 10:00-12:00, im Seminarraum E1852, Favoritenstraße 9/Stiege 1 oder 3/3. Stock (gelber Bereich) statt. Es beginnt am 19.Oktober mit der Vortragseinteilung.
Das Seminar basiert unter anderem auf dem deutschsprachigen Lehrbuch
Krzysztof R. Apt, Ernst-Rüdiger Olderog: Programmverifikation - Sequentielle, parallele und verteilte Programme.Exemplare des Buches sind in der Hauptbibliothek (Freihandbereich / DAT:431 / 543143 I) und in der Mathematikbibliothek (68Q60A / 224267 I) entlehnbar. Relevante Teile werden im Laufe des Seminars als Kopie zur Verfügung gestellt.
Springer-Verlag, 1994.
Von den TeilnehmerInnen wird erwartet, dass sie einen Abschnitt des Buches erarbeiten, schriftlich zusammenfassen und in einem etwa einstündigen Vortrag präsentieren. Für die Beurteilung ist sowohl die Qualität der Zusammenfassung und des Vortrages als auch die Beteiligung an der allgemeinen Diskussion maßgebend.
[ LVAs 185/2 | Abteilung 185/2 | Institut 185 | Informatik | TU Wien | Server home page ]