Provably Correct Control-Flow Graphs from Java Programs with Exceptions

A. Amighi, Pedro de Carvalho Gomes, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    43 Downloads (Pure)

    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.
    Original languageUndefined
    Title of host publicationPapers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11
    Place of PublicationKarlsruhe
    PublisherKarlsruhe Institute of Technology
    Pages31-48
    Number of pages18
    ISBN (Print)2190-4782
    Publication statusPublished - Oct 2011

    Publication series

    NameKarlsruhe Reports in Informatics
    PublisherKarlsruhe Institute of Technology
    Number26
    Volume26
    ISSN (Print)2190-4782

    Keywords

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

    Cite this

    Amighi, A., de Carvalho Gomes, P., & Huisman, M. (2011). Provably Correct Control-Flow Graphs from Java Programs with Exceptions. In 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.
    Amighi, A. ; de Carvalho Gomes, Pedro ; Huisman, Marieke. / Provably Correct Control-Flow Graphs from Java Programs with Exceptions. Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11. Karlsruhe : Karlsruhe Institute of Technology, 2011. pp. 31-48 (Karlsruhe Reports in Informatics; 26).
    @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",
    year = "2011",
    month = "10",
    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",

    }

    Amighi, A, de Carvalho Gomes, P & Huisman, M 2011, Provably Correct Control-Flow Graphs from Java Programs with Exceptions. in 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.

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 -

    Amighi A, de Carvalho Gomes P, Huisman M. Provably Correct Control-Flow Graphs from Java Programs with Exceptions. In Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11. Karlsruhe: Karlsruhe Institute of Technology. 2011. p. 31-48. (Karlsruhe Reports in Informatics; 26).