185.A73 Deduktive Verifikation von Software
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2016S, VU, 4.0h, 6.0EC

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

Formale Methoden zum Beweisen der Korrektheit von Programmen anwenden können.

Inhalt der Lehrveranstaltung

Grundlagen der formalen Verifikation (Hoare-Logik); Entwicklung korrekter Programme mit Hilfe von Zusicherungen, Pre- und Postconditions, Schleifeninvarianten; Verifikation sequentieller, paralleler und verteilter Programme; praktische Übungen mit ausgewählten Systemen zur Programmverifikation. Didaktische Methodik: Vortrag mit aktiver Beteiligung der anwesenden Studierenden, Praktische Aufgaben mit Abgabegesprächen

Weitere Informationen

Beginn der Vorlesung: Mo, 3.3.2014. Bitte melden Sie sich zur Lehrveranstaltung über TISS an, oder wenn das nicht geht, per Email an gernot.salzer@tuwien.ac.at.

Voraussichtlicher Aufwand für die Studierenden:

26 Std. Besuch Vorlesung, Mitarbeit und Prüfung
24 Std. Lernen für Vorlesungsprüfung
100 Std. Bearbeiten der Übungsaufgaben

Gesamt: 150 Std.

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mi.16:00 - 17:0002.03.2016Seminarraum FAV EG C (Seminarraum Gödel) Vorbesprechung
Mi.15:00 - 17:0009.03.2016 - 16.03.2016Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.15:30 - 17:0006.04.2016 - 25.05.2016Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.15:00 - 17:0001.06.2016 - 15.06.2016Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Deduktive Verifikation von Software - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.02.03.201616:00 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorbesprechung
Mi.09.03.201615:00 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.16.03.201615:00 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.06.04.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.13.04.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.20.04.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.27.04.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.04.05.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.11.05.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.18.05.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.25.05.201615:30 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.01.06.201615:00 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.08.06.201615:00 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Mi.15.06.201615:00 - 17:00Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung

LVA-Anmeldung

Von Bis Abmeldung bis
18.02.2016 00:00 16.03.2016 23:59 16.03.2016 23:59

Curricula

Literatur

David Gries: The Science of Programming, Springer 1981.

R.C. Backhouse: Program Construction and Verification, Prentice-Hall 1986.

Gerald Futschek: Programmentwicklung und Verifikation, Springer SAI 1989 (in German).

Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag 1990.

Vorkenntnisse

Grundkenntnisse der Logik. Gute Programmierkenntnisse.

Sprache

bei Bedarf in Englisch