Apr 19, 2011: Afshin Amighi: Flow Graph Extraction for Modular Verification of Java Programs

April 19, 2011Flow Graph Extraction for Modular Verification of Java Programs
Room: Zi 5126Afshin Amighi

The starting point for the project is a framework for compositional program verification based on program flow graphs, an abstraction of program control flow giving rise to an over-approximation of the source code behavior. Flow graph extraction for modular verification should allow the independent extraction of flow graphs of subsystems or modules. Furthermore, the composition of the flow graphs of the modules should give a safe approximation of the complete program flow graph. The existing tools for flow graph extraction are not flexible enough for modular purposes, since they typically assume that they are given a complete program.

The goal of this study is the formal definition and implementation of modular flow graph extraction. In this project a formal translation from Java programs to target flow graph is specified. Then based on an operational semantics for the source language and for flow graphs, the correctness of the translation is proved. Flow graph extraction has to respect the modularity of programs, which is the main contribution of the work. Finally, a tool is developed based on specification of the translation.