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

    4 Citations (Scopus)
    43 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 Dive into the research topics of 'Certifying safety and termination proofs for integer transition systems'. Together they form a unique fingerprint.

  • 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