Change search
ReferencesLink to record
Permanent link

Direct link
Provably Correct Control-Flow Graphs from 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)Report (Other academic)
Abstract [en]

We present an algorithm to extract flow graphs from Java bytecode, including exceptional control flows. We prove its correctness, meaning that the behavior of the extracted control-flow graph is a sound over-approximation of the behavior 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 various static analyses, such as model checking.The extraction is performed in two phases. In the first phase the program is transformed into a BIR program, a stack-less intermediate representation of Java bytecode, from which the control-flow graph is extracted in the second phase. We use this intermediate format because it results in compact flow graphs, with provably correct exceptional control flow. To prove the correctness of the two-phase extraction, we also define an idealized extraction algorithm, whose correctness can be proven directly. Then we show that the behavior of the control-flow graph extracted via the intermediate representation is an over-approximation of the behavior of the directly extracted graphs, and thus of the original program. We implemented the indirect extraction as the CFGEx tool and performed several test-cases to show the efficiency of the algorithm.

Place, publisher, year, edition, pages
KTH Royal Institute of Technology and University of Twente , 2012. , 30 p.
Keyword [en]
Software Verification, Static Analysis, Program Models
National Category
Computer Systems
Research subject
URN: urn:nbn:se:kth:diva-61188OAI: diva2:478705
ICT - The Next Generation

QC 20120116

Available from: 2012-01-16 Created: 2012-01-16 Last updated: 2013-04-15Bibliographically approved

Open Access in DiVA

fulltext(522 kB)740 downloads
File information
File name FULLTEXT04.pdfFile size 522 kBChecksum SHA-512
Type fulltextMimetype application/pdf

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
Total: 797 downloads
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: 305 hits
ReferencesLink to record
Permanent link

Direct link