Intendierte Lernergebnisse
Die Lernergebnisse dieser Vorlesung sinddas Erlernen der Grundlagen logikbasierter Beweismethoden,das Erlernen verschiedener formaler Methoden zur Programmverifikation,das Beherrschen der logikbasierten Spezifikation und Verifikation von sequenziellen und parallelen Programmen,das Beherrschen der Spezifikation und Verifikation von Java-Programmen unddas Erlernen zukünftiger Trends und Anwendungen von formalen Methoden in der Softwareentwicklung.
Lehrmethodik
Diese Vorlesung wird geblockt abgehalten. Jeder Block umfasst vier Einheiten, die jeweils mit Pausen im Zeitraum von 08:00 – 12:00 geplant sind. Die Vorlesung findet an ausgewählten Samstagen und an einem Freitag statt.Diese Lehrveranstaltung wird in Form einer Vorlesung angeboten. Die Vorlesung wird interaktiv gestaltet und es kommen Mini-Aufgaben zum Einsatz.
Inhalt/e
Die Vorlesung beinhaltet folgende Themen:Logik und BeweisführungFormale Methoden im Software EngineeringFormale ProgrammspezifikationProgrammverifikationSpezifikation und Verifikation von sequenziellen Programmen, insbesondere von Java-Programmen, die mittels der Java Modeling Language (JML) spezifiziert sindSpezifikation und Verifikation von parallelen Programmen, insbesondere mit dem Spin Model Checker
Erwartete Vorkenntnisse
Gute Kenntnisse der Java-Programmierung sind erforderlich.
Literatur
Die Literatur wird in der ersten Vorlesung bekanntgegeben.