Change search
ReferencesLink to record
Permanent link

Direct link
Provably Correct Control-Flow Graphs from Java Programs with Exceptions
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-6468-1605
2011 (English)In: Formal Verification of Object-Oriented Software, 2011, Vol. 26, 31-48 p.Conference paper (Refereed)
Abstract [en]

We present an algorithm to extract flow graphs from Java bytecode, focusing on exceptional control flows. We prove its correctness, meaning that the behaviour of the extracted control-flow graph is an over-approximation of the behaviour of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing different static analyses. For precision and efficiency, the extraction is performed in two phases. In the first phase the program is transformed into a BIR program, where BIR is a stack-less intermediate representation of Java bytecode; in the second phase the control-flow graph is extracted from the BIR representation. To prove the correctness of the two-phase extraction, we also define a direct extraction algorithm, whose correctness can be proven immediately. Then we show that the behaviour of the control-flow graph extracted via the intermediate representation is an over-approximation of the behaviour of the directly extracted graphs, and thus of the original program.

Place, publisher, year, edition, pages
2011. Vol. 26, 31-48 p.
, Karlsruhe Reports in Informatics
Keyword [en]
Static Analysis, Control flow graph, Java bytecode
National Category
Computer Science
URN: urn:nbn:se:kth:diva-154795OAI: diva2:758575
2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011, October 5-7, 2011, Turin, Italy

QC 20150205

Available from: 2014-10-27 Created: 2014-10-27 Last updated: 2015-02-05Bibliographically approved

Open Access in DiVA

No full text

Other links

Search in DiVA

By author/editor
de Carvalho Gomes, Pedro
By organisation
Theoretical Computer Science, TCS
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: 44 hits
ReferencesLink to record
Permanent link

Direct link