Provably Correct Control-Flow Graphs from Java Programs with Exceptions
2011 (English)In: Formal Verification of Object-Oriented Software, 2011, Vol. 26, 31-48 p.Conference paper (Refereed)
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
Static Analysis, Control flow graph, Java bytecode
IdentifiersURN: urn:nbn:se:kth:diva-154795OAI: oai:DiVA.org:kth-154795DiVA: diva2:758575
2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011, October 5-7, 2011, Turin, Italy
QC 201502052014-10-272014-10-272015-02-05Bibliographically approved