Using System Dependence Graphs for the Automatic Generation of Frame Conditions

Forschungsthema:KeY, JOANA
Typ: BA
Datum: 2019-12-17
Betreuer: Mihai Herda
Michael Kirsten


KeY is a tool for the formal verification of sequential Java programs. In order to formally verify the correctness of a program using KeY, specifications for the program are needed. These specifications are written in the form of annotations in JML, a specification language for Java. A part of these annotations are frame conditions. These frame conditions specify which memory locations a method can read or modify.
In this thesis, an approach is developed and implemented that automatically generates frame conditions for a program from its system dependence graph (SDG). This SDG represents data and control dependencies between parts of the analysed program. To this end, an SDG of the program is constructed using JOANA, an analysis tool for Java programs. This approach is then evaluated using selected programs from the KeY example collection.