Intendierte Lernergebnisse
Die Lernergebnisse dieser Übung 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
Austeilen von ÜbungsblätternAusarbeitung der Übungsblätter als HausübungPräsentation und Diskussion der Übungsausarbeitungen durch Studierende und LV-Leiter in den Übungseinheiten
Inhalt/e
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 Übung bekanntgegeben.