Specification and Verification of Object-Oriented Software

Abstract

Interface specifications, program verification, model checking, testing, advanced type systems, alias and pointer analysis

Objective

Ziel des Seminars ist es, Studierende mit den grundsätzlichen Problemstellungen der Beschreibung und Überprüfung von Programmeigenschaften vertraut zu machen. Dadurch soll unter anderem das Verständnis für die Semantik von Programmen und Spezifikationen geschärft und so der Programmierstil verbessert werden. Darüber hinaus schult das Seminar die Fähigkeit, wissenschaftliche Literatur zu verstehen und sich kritisch mit ihr auseinanderzusetzen.

Content

Spezifikationen sind präzise Beschreibungen der Eigenschaften von Programmen und Komponenten. Sie sind ein wichtiger Bestandteil einer sauberen Entwicklungsmethodik und bilden die Grundlage für Wiederverwendung, Wartung, Analyse und Verifikation von Software. Unter Verifikation versteht man die formale Beweisführung, dass ein Programm seine Spezifikation erfüllt, also den Nachweis seiner Korrektheit. In diesem Seminar werden wissenschaftliche Aufsätze zur Spezifikation, Analyse und Verifikation objektorientierter Software behandelt. Schwerpunkte liegen dabei auf speziellen Typsystemen zur Beschreibung und automatischen Prüfung bestimmter Programmeigenschaften, auf Techniken zur Spezifikation von Schnittstellen in objektorientierten Programmen sowie auf Ansätzen zur formalen Programmanalyse und -verifikation.

Resources