Using System Dependence Graphs for the Automatic Generation of Frame Conditions
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
specification language for Java.
A part of these annotations are frame conditions.
These frame conditions specify which memory locations a method can read or
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.
- "Deductive Software Verification - The KeY Book: From Theory to Practice" in Lecture Notes in Computer Science 10001 (Springer 2016)
- "A Hybrid Approach for Proving Noninterference of Java Programs" in 28th IEEE Computer Security Foundations Symposium (CSF 2015)