@inproceedings{ac3cd23e0a4c4da78d81e5e5b87bd713,

title = "Provably Correct Control-Flow Graphs from Java Programs with Exceptions",

abstract = "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.",

keywords = "METIS-285024, IR-79610, Control flow graph, EWI-21319, Static Analysis, CR-D.3.1, Java bytecode",

author = "A. Amighi and {de Carvalho Gomes}, Pedro and Marieke Huisman",

note = "eemcs-eprint-21319 ; null ; Conference date: 05-10-2011 Through 07-10-2011",

year = "2011",

month = oct,

language = "Undefined",

isbn = "2190-4782",

series = "Karlsruhe Reports in Informatics",

publisher = "Karlsruhe Institute of Technology",

number = "26",

pages = "31--48",

booktitle = "Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11",

}