Change search
ReferencesLink to record
Permanent link

Direct link
Flow Graph Extraction for Modular Verification of Java Programs.
KTH, School of Computer Science and Communication (CSC).
2011 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

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.

Place, publisher, year, edition, pages
Trita-CSC-E, ISSN 1653-5715 ; 2011:038
National Category
Computer Science
URN: urn:nbn:se:kth:diva-130658OAI: diva2:654105
Educational program
Master of Science - Software Engineering of Distributed Systems
Available from: 2013-10-07 Created: 2013-10-07

Open Access in DiVA

No full text

Other links
By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 203 hits
ReferencesLink to record
Permanent link

Direct link