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

    5 Citations (Scopus)
    104 Downloads (Pure)


    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
    Number of pages18
    ISBN (Electronic)978-3-319-63046-5
    ISBN (Print)978-3-319-63045-8
    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
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    WorkshopAutomated Deduction - CADE 26
    Abbreviated titleCADE


    Dive into the research topics of 'Certifying safety and termination proofs for integer transition systems'. Together they form a unique fingerprint.

    Cite this