Certifying safety and termination proofs for integer transition systems

Marc Brockschmidt, Sebastiaan JC Joosten, René Thiemann, Akihisa Yamada

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

    1 Citation (Scopus)
    14 Downloads (Pure)

    Abstract

    Modern program analyzers translate imperative programs to an intermediate formal language like integer transition systems (ITSs), and then analyze properties of ITSs. Because of the high complexity of the task, a number of incorrect proofs are revealed annually in the Software Verification Competitions.
    In this paper, we establish the trustworthiness of termination and safety proofs for ITSs. To this end we extend our Isabelle/HOL formalization IsaFoR by formalizing several verification techniques for ITSs, such as invariant checking, ranking functions, etc. Consequently the extracted certifier CeTA can now (in)validate safety and termination proofs for ITSs. We also adapted the program analyzers T2 and AProVE to produce machinereadable proof certificates, and as a result, most termination proofs generated by these tools on a standard benchmark set are now certified.
    Original languageEnglish
    Title of host publicationAutomated Deduction - CADE 26 International Conference on Automated Deduction
    Subtitle of host publication26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017. Proceedings
    EditorsLeonardo de Moura
    Place of PublicationCham
    PublisherSpringer
    Pages454-471
    Number of pages18
    ISBN (Electronic)978-3-319-63046-5
    ISBN (Print)978-3-319-63045-8
    DOIs
    Publication statusPublished - 2017
    EventAutomated Deduction - CADE 26: 26th International Conference on Automated Deduction - Lindholmen Conference Centre, Gothenburg, Sweden
    Duration: 6 Aug 201711 Aug 2017
    Conference number: 26

    Publication series

    NameLecture Notes in Artificial Intelligence
    PublisherSpringer
    Volume10395
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Workshop

    WorkshopAutomated Deduction - CADE 26
    Abbreviated titleCADE
    CountrySweden
    CityGothenburg
    Period6/08/1711/08/17

    Fingerprint

    Computer systems
    Formal languages

    Cite this

    Brockschmidt, M., Joosten, S. JC., Thiemann, R., & Yamada, A. (2017). Certifying safety and termination proofs for integer transition systems. In L. de Moura (Ed.), Automated Deduction - CADE 26 International Conference on Automated Deduction: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017. Proceedings (pp. 454-471). (Lecture Notes in Artificial Intelligence; Vol. 10395). Cham: Springer. https://doi.org/10.1007/978-3-319-63046-5_28
    Brockschmidt, Marc ; Joosten, Sebastiaan JC ; Thiemann, René ; Yamada, Akihisa. / Certifying safety and termination proofs for integer transition systems. Automated Deduction - CADE 26 International Conference on Automated Deduction: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017. Proceedings. editor / Leonardo de Moura. Cham : Springer, 2017. pp. 454-471 (Lecture Notes in Artificial Intelligence).
    @inproceedings{4cf22f88c22447949d3fcce7d3d45289,
    title = "Certifying safety and termination proofs for integer transition systems",
    abstract = "Modern program analyzers translate imperative programs to an intermediate formal language like integer transition systems (ITSs), and then analyze properties of ITSs. Because of the high complexity of the task, a number of incorrect proofs are revealed annually in the Software Verification Competitions.In this paper, we establish the trustworthiness of termination and safety proofs for ITSs. To this end we extend our Isabelle/HOL formalization IsaFoR by formalizing several verification techniques for ITSs, such as invariant checking, ranking functions, etc. Consequently the extracted certifier CeTA can now (in)validate safety and termination proofs for ITSs. We also adapted the program analyzers T2 and AProVE to produce machinereadable proof certificates, and as a result, most termination proofs generated by these tools on a standard benchmark set are now certified.",
    author = "Marc Brockschmidt and Joosten, {Sebastiaan JC} and Ren{\'e} Thiemann and Akihisa Yamada",
    year = "2017",
    doi = "10.1007/978-3-319-63046-5_28",
    language = "English",
    isbn = "978-3-319-63045-8",
    series = "Lecture Notes in Artificial Intelligence",
    publisher = "Springer",
    pages = "454--471",
    editor = "{de Moura}, Leonardo",
    booktitle = "Automated Deduction - CADE 26 International Conference on Automated Deduction",

    }

    Brockschmidt, M, Joosten, SJC, Thiemann, R & Yamada, A 2017, Certifying safety and termination proofs for integer transition systems. in L de Moura (ed.), Automated Deduction - CADE 26 International Conference on Automated Deduction: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017. Proceedings. Lecture Notes in Artificial Intelligence, vol. 10395, Springer, Cham, pp. 454-471, Automated Deduction - CADE 26, Gothenburg, Sweden, 6/08/17. https://doi.org/10.1007/978-3-319-63046-5_28

    Certifying safety and termination proofs for integer transition systems. / Brockschmidt, Marc; Joosten, Sebastiaan JC; Thiemann, René; Yamada, Akihisa.

    Automated Deduction - CADE 26 International Conference on Automated Deduction: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017. Proceedings. ed. / Leonardo de Moura. Cham : Springer, 2017. p. 454-471 (Lecture Notes in Artificial Intelligence; Vol. 10395).

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

    TY - GEN

    T1 - Certifying safety and termination proofs for integer transition systems

    AU - Brockschmidt, Marc

    AU - Joosten, Sebastiaan JC

    AU - Thiemann, René

    AU - Yamada, Akihisa

    PY - 2017

    Y1 - 2017

    N2 - Modern program analyzers translate imperative programs to an intermediate formal language like integer transition systems (ITSs), and then analyze properties of ITSs. Because of the high complexity of the task, a number of incorrect proofs are revealed annually in the Software Verification Competitions.In this paper, we establish the trustworthiness of termination and safety proofs for ITSs. To this end we extend our Isabelle/HOL formalization IsaFoR by formalizing several verification techniques for ITSs, such as invariant checking, ranking functions, etc. Consequently the extracted certifier CeTA can now (in)validate safety and termination proofs for ITSs. We also adapted the program analyzers T2 and AProVE to produce machinereadable proof certificates, and as a result, most termination proofs generated by these tools on a standard benchmark set are now certified.

    AB - Modern program analyzers translate imperative programs to an intermediate formal language like integer transition systems (ITSs), and then analyze properties of ITSs. Because of the high complexity of the task, a number of incorrect proofs are revealed annually in the Software Verification Competitions.In this paper, we establish the trustworthiness of termination and safety proofs for ITSs. To this end we extend our Isabelle/HOL formalization IsaFoR by formalizing several verification techniques for ITSs, such as invariant checking, ranking functions, etc. Consequently the extracted certifier CeTA can now (in)validate safety and termination proofs for ITSs. We also adapted the program analyzers T2 and AProVE to produce machinereadable proof certificates, and as a result, most termination proofs generated by these tools on a standard benchmark set are now certified.

    U2 - 10.1007/978-3-319-63046-5_28

    DO - 10.1007/978-3-319-63046-5_28

    M3 - Conference contribution

    SN - 978-3-319-63045-8

    T3 - Lecture Notes in Artificial Intelligence

    SP - 454

    EP - 471

    BT - Automated Deduction - CADE 26 International Conference on Automated Deduction

    A2 - de Moura, Leonardo

    PB - Springer

    CY - Cham

    ER -

    Brockschmidt M, Joosten SJC, Thiemann R, Yamada A. Certifying safety and termination proofs for integer transition systems. In de Moura L, editor, Automated Deduction - CADE 26 International Conference on Automated Deduction: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017. Proceedings. Cham: Springer. 2017. p. 454-471. (Lecture Notes in Artificial Intelligence). https://doi.org/10.1007/978-3-319-63046-5_28