Change search
ReferencesLink to record
Permanent link

Direct link
Sound Control-Flow Graph Extraction for Java Programs with Exceptions
University of Twente.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-6468-1605
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
University of Twente.
2012 (English)In: Software Engineering and Formal Methods: 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, Springer Berlin/Heidelberg, 2012, 33-47 p.Conference paper (Refereed)
Abstract [en]

We present an algorithm to extract control-flow graphs from Java bytecode, considering exceptional flows. We then establish its correctness: the behavior of the extracted graphs is shown to be a sound over-approximation of the behavior of the original programs. Thus, any temporal safety property that holds for the extracted control-flow graph also holds for the original program. This makes the extracted graphs suitable for performing various static analyses, in particular model checking. The extraction proceeds in two phases. First, we translate Java bytecode into BIR, a stack-less intermediate representation. The BIR transformation is developed as a module of Sawja, a novel static analysis framework for Java bytecode. Besides Sawja’s efficiency, the resulting intermediate representation is more compact than the original bytecode and provides an explicit representation of exceptions. These features make BIR a natural starting point for sound control-flow graph extraction. Next, we formally define the transformation from BIR to control-flow graphs, which (among other features) considers the propagation of uncaught exceptions within method calls. We prove the correctness of the two-phase extraction by suitably combining the properties of the two transformations with those of an idealized control-flow graph extraction algorithm, whose correctness has been proved directly. The control-flow graph extraction algorithm is implemented in the ConFlEx tool. A number of test-cases show the efficiency and the utility of the implementation.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2012. 33-47 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 7504
Keyword [en]
Software Verification, Static Analysis, Program Models, Control-Flow Graphs, Java bytecode
National Category
Computer Systems
Research subject
SRA - E-Science (SeRC)
URN: urn:nbn:se:kth:diva-104238DOI: 10.1007/978-3-642-33826-7_3ScopusID: 2-s2.0-84868256995ISBN: 978-3-642-33825-0OAI: diva2:563620
10th International Conference on Software Engineering and Formal Methods, SEFM 2012; Thessaloniki; 1 October 2012 through 5 October 2012
ICT - The Next GenerationSwedish e‐Science Research Center

QC 20121213

Available from: 2012-10-30 Created: 2012-10-30 Last updated: 2013-04-15Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
de Carvalho Gomes, PedroGurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Systems

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

Altmetric score

Total: 52 hits
ReferencesLink to record
Permanent link

Direct link