Skip to Content

Certifying safety and termination proofs for integer transition systems

Posted on

Authors:

  • Brockschmidt, Marc
  • Joosten, Sebastiaan J. C.
  • Thiemann, René
  • Yamada, Akihisa

Published in: Automated Deduction - CADE 26 International Conference on Automated Deduction. de Moura, Leonardo (Eds) pp 454–471

DOI: 10.1007/978-3-319-63046-5_28

Paper

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.

BibTeX entry:

@inproceedings{Brockschmidt17,
 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 Jozef Christiaan} and Ren{\'e} Thiemann and Akihisa Yamada},
 bdsk-url-1 = {https://doi.org/10.1007/978-3-319-63046-5_28},
 booktitle = {Automated Deduction - CADE 26 International Conference on Automated Deduction},
 day = {11},
 doi = {10.1007/978-3-319-63046-5_28},
 editor = {{de Moura}, Leonardo},
 isbn = {978-3-319-63045-8},
 language = {English},
 month = {Aug},
 pages = {454--471},
 publisher = {Springer},
 series = {Lecture Notes in Artificial Intelligence},
 title = {Certifying safety and termination proofs for integer transition systems},
 year = {2017}
}