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

6 Citations (Scopus)
145 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
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
Externally publishedYes
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


  • n/a OA procedure


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

Cite this