Programmsynthese aus formalen Spezifikationen im Tool CorC

  • Kontext: Correctness-by-Construction (CbC) ist ein Verfahren zur Softwareentwicklung. Hierbei werden Programme mit formalen Spezifikationen versehen und durch Korrektheit bewahrende Verfeinerungen erstellt. Das Tool CorC bietet die Möglichkeit, Programme unter Verwendung von CbC zu entwickeln. Bei der Programmsynthese geht es darum, aus einer formalen Spezifikation, wie sie auch bei CbC verwendet wird, Programme, die die Spezifikation erfüllen automatisch zu synthetisieren.

     

    Ziel: In der Masterarbeit soll sich in Programmsynthesetechniken eingearbeitet werden und ein Konzept entwickelt werden, diese auf CbC, wie es im Tool CorC implementiert ist, anzuwenden. In der Arbeit soll außerdem evaluiert werden, zu welchem Grad sich Programmsynthese mit dem entstandenen Konzept umsetzen lässt und wie gut die synthetisierten Programme zu ihren Spezifikationen passen.

     

    Voraussetzung: Programmierkenntnisse in Java, Grundlegende Kenntnisse im Bereich der Programmverifikation und -spezifikation