kth.sePublikationer KTH
Driftstörningar
Det förekommer återkommande driftstörningar på några av sök-portalerna på grund av hög belastning. Vi arbetar på att lösa problemet, ni kan tillfälligt mötas av ett felmeddelande.
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Provably Correct Control Flow Graphs from Java Bytecode Programs with Exceptions
University of Twente.
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0002-6468-1605
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0002-0074-8786
University of Twente.
2016 (Engelska)Ingår i: International Journal on Software Tools for Technology Transfer, ISSN 1433-2779, E-ISSN 1433-2787, ISSN 1433-2779, Vol. 18, nr 6, s. 653-684Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

We present an algorithm for extracting control flow graphs from Java bytecode that captures normal as well as exceptional control flow. We prove its correctness, in the sense that the behaviour of the extracted control flow graph is a sound over-approximation of the behaviour of the original program. This makes control flow graphs suitable for performing various static analyses, such as model checking of temporal safety properties.Analyzing exceptional control flow for Java bytecode is difficult because of the stack-based nature of the language. We therefore develop the extraction in two stages. In the first, we abstract away from the complications arising from exceptional flows, and relativize the extraction on an oracle that is able to look into the stack and predict the exceptions that can be raised at each instruction. This idealized algorithm provides a specification for concrete extraction algorithms, which have to provide a suitable implementation for the oracle. We prove correctness of the idealized algorithm by means of behavioural simulation.In the second stage, we develop a concrete extraction algorithm that consists of 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 provides the information needed to implement the oracle, and since it gives rise to more compact graphs. We show that the behaviour of the control flow graph extracted via the intermediate representation is a sound over-approximation of the behaviour of the graph extracted by the direct, idealized algorithm, and thus of the original program. The concrete extraction algorithm is implemented as the ConFlEx tool. A number of test cases are performed to evaluate the efficiency of the algorithm.

Ort, förlag, år, upplaga, sidor
Springer Nature, 2016. Vol. 18, nr 6, s. 653-684
Nyckelord [en]
Software Verification, Static Analysis, Program Models
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Informations- och kommunikationsteknik
Identifikatorer
URN: urn:nbn:se:kth:diva-164580DOI: 10.1007/s10009-015-0375-0ISI: 000385180700006Scopus ID: 2-s2.0-84926377646OAI: oai:DiVA.org:kth-164580DiVA, id: diva2:806114
Anmärkning

QC 20230927

Tillgänglig från: 2015-04-17 Skapad: 2015-04-17 Senast uppdaterad: 2024-01-17Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Person

de Carvalho Gomes, PedroGurov, Dilian

Sök vidare i DiVA

Av författaren/redaktören
de Carvalho Gomes, PedroGurov, Dilian
Av organisationen
Teoretisk datalogi, TCS
I samma tidskrift
International Journal on Software Tools for Technology Transfer
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 668 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf