Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
SRA - ICT
Identifiers
URN: urn:nbn:se:kth:diva-61188OAI: oai:DiVA.org:kth-61188DiVA: diva2:478705
Projects
CVPP
Funder
ICT - The Next Generation
Note

QC 20120116

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

Open Access in DiVA

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

Authority records BETA

de Carvalho Gomes, PedroGurov, Dilian

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: 1068 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

urn-nbn

Altmetric score

urn-nbn
Total: 357 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf