### Abstract

Original language | Undefined |
---|---|

Title of host publication | Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11 |

Place of Publication | Karlsruhe |

Publisher | Karlsruhe Institute of Technology |

Pages | 31-48 |

Number of pages | 18 |

ISBN (Print) | 2190-4782 |

Publication status | Published - Oct 2011 |

### Publication series

Name | Karlsruhe Reports in Informatics |
---|---|

Publisher | Karlsruhe Institute of Technology |

Number | 26 |

Volume | 26 |

ISSN (Print) | 2190-4782 |

### Keywords

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

### Cite this

*Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11*(pp. 31-48). (Karlsruhe Reports in Informatics; Vol. 26, No. 26). Karlsruhe: Karlsruhe Institute of Technology.

}

*Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11.*Karlsruhe Reports in Informatics, no. 26, vol. 26, Karlsruhe Institute of Technology, Karlsruhe, pp. 31-48.

**Provably Correct Control-Flow Graphs from Java Programs with Exceptions.** / Amighi, A.; de Carvalho Gomes, Pedro; Huisman, Marieke.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Provably Correct Control-Flow Graphs from Java Programs with Exceptions

AU - Amighi, A.

AU - de Carvalho Gomes, Pedro

AU - Huisman, Marieke

N1 - eemcs-eprint-21319

PY - 2011/10

Y1 - 2011/10

N2 - 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.

AB - 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.

KW - METIS-285024

KW - IR-79610

KW - Control flow graph

KW - EWI-21319

KW - Static Analysis

KW - CR-D.3.1

KW - Java bytecode

M3 - Conference contribution

SN - 2190-4782

T3 - Karlsruhe Reports in Informatics

SP - 31

EP - 48

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

PB - Karlsruhe Institute of Technology

CY - Karlsruhe

ER -