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 |
| Aushang: |
Abstract
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.
Literature
- "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)