### Certifying Termination and Complexity Proofs of Programs

Computer programs become ubiquitous in our world: they are used to manage our money, to control activities in vehicles, and to interact with medical equipment. Therefore, it is of vital importance that programs behave correctly. Here, termination (all computations produce a result) and complexity (how long does it take to get the result, and how much memory is required) are fundamental properties of programs. Unfortunately, these fundamental properties are undecidable. For example, it is not possible to design an analyser-program which decides for each other program, whether it terminates or not. Nevertheless, much work has been spent on the development of such analysers which are often able to guarantee the property of concern.

Whereas the answer of an analysis for a given program might be simple (yes, the program is terminating), the underlying argument for this answer, i.e., the proof, is usually not simple. In fact, most analysers for the properties complexity and termination are complex programs on their own, which combine several techniques while trying to determine the behaviour of a program. Consequently, these analysers may contain errors and give wrong answers and proofs.

Our solution to this problem is the program CeTA (Certified Tool Assertions), a certifier that was developed in this project. CeTA can figure out whether the proofs that are generated by the analysers are correct or not. To make CeTA trustworthy, we formally verified all algorithms within CeTA with the help of the theorem prover Isabelle.

In comparison to previous certifiers, CeTA offers the following unique features:

- CeTA supports several kinds of complexity proofs from various analysers.
- CeTA supports checking termination proofs for LLVM, a widely used intermediate language that is utilised when compiling programs written in popular programming languages such as C and Haskell.
- For checking complexity proofs, internally CeTA supports precise calculations via algebraic numbers. For instance, CeTA is able to compute all roots of a polynomial such as
*x*without any rounding errors.^{8}– 5x^{6}+ 7x^{3}– 17 - For checking LLVM proofs, CeTA provides a validity checker for linear inequalities, e.g., it can decide whether there are integers
*x*,*y*and*z*such that*2x + 3y – 2z > 7*,*x – 5y + 4z > -2*and*3x + 4y + z < 15*.

As further results of this project, mistakes in textbooks and published research articles have been spotted (and corrected) during the formalisation of the algorithms that are used in CeTA; wrong proofs of some analysis tools have been identified by CeTA and the corresponding tools have been fixed; and finally, the developed verified algorithms can serve as a good starting point for other formalisations in the area of program analysis.

#### Members

- Ralph Bottesch
- Max W. Haslbeck
- Sebastiaan Joosten
- Christian Sternagel
- René Thiemann (project leader)
- Akihisa Yamada

#### FWF project number

Y757#### Contact

rene.thiemann at uibk.ac.at#### Publications

Regular Tree Relations

Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel

Archive of Formal Proofs 2021.

Factorization of Polynomials with Algebraic Coefficients

Manuel Eberl, René Thiemann

Archive of Formal Proofs 2021.

A Formalization of Weighted Path Orders and Recursive Path Orders

Christian Sternagel, René Thiemann, Akihisa Yamada

Archive of Formal Proofs 2021.

Solving Cubic and Quartic Equations

René Thiemann

Archive of Formal Proofs 2021.

A Perron–Frobenius theorem for deciding matrix growth

René Thiemann

Journal of Logical and Algebraic Methods in Programming 123,
2021.

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

Ralph Bottesch, Jose Divasón, René Thiemann

Archive of Formal Proofs 2021.

The Sunflower Lemma of Erdős and Rado

René Thiemann

Archive of Formal Proofs 2021.

An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR

Max Haslbeck, Rene Thiemann

10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),
pp. 238 – 249,
2021.

Certifying the Weighted Path Order

Rene Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada

5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020),
Leibniz International Proceedings in Informatics (LIPIcs) 167,
pp. 4:1 – 4:20,
2020.

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J.C. Joosten, Akihisa Yamada

Journal of Automated Reasoning 64,
pp. 827 – 856,
2020.

A Formalization of Knuth-Bendix Orders

Christian Sternagel, René Thiemann

Archive of Formal Proofs 2020.

Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL

Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann

12th International NASA Formal Methods Symposium (NFM 2020),
LNCS 12229,
pp. 233 – 250,
2020.

Verified Analysis of Random Binary Tree Structures

Manuel Eberl, Max W. Haslbeck, Tobias Nipkow

Journal of Automated Reasoning 64,
pp. 879 – 910,
2020.

Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL

Ralph Bottesch, Max W. Haslbeck, and René Thiemann

International Symposium on Frontiers of Combining Systems,
Lecture Notes in Computer Science 11715,
pp. 223 – 239,
2019.

Linear Inequalities

Ralph Bottesch, Alban Reynaud, René Thiemann

Archive of Formal Proofs 2019.

A Verified Implementation of the Berlekamp—Zassenhaus Factorization Algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada

Journal of Automated Reasoning 64(4),
pp. 699 – 735,
2020.

Farkas’ Lemma and Motzkin’s Transposition Theorem

Ralph Bottesch, Max W. Haslbeck, René Thiemann

Archive of Formal Proofs 2019.

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Journal of Automated Reasoning 64,
pp. 363 – 389,
2020.

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm

Ralph Bottesch, Max W. Haslbeck, René Thiemann

22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning,
EPiC Series in Computing 57,
pp. 164 – 180,
2018.

Extending a Verified Simplex Algorithm

René Thiemann

13th International Workshop on the Implementation of Logics,
Kalpa Publications in Computing 9,
pp. 37 – 48,
2018.

On W[1]-Hardness as Evidence for Intractability

Ralph C. Bottesch

43rd International Symposium on Mathematical Foundations of Computer Science,
Leibniz International Proceedings in Informatics 117,
pp. 73:1 – 73:15,
2018.

An Incremental Simplex Algorithm with Unsatisfiable Core Generation

Filip Marić, Mirko Spasić, René Thiemann

Archive of Formal Proofs 2018.

A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Proceedings of the 16th International Workshop on Termination,
pp. 30-34,
2018.

Formal Verification of Bounds for the LLL Basis Reduction Algorithm

Max W. Haslbeck, René Thiemann

Isabelle Workshop 2018,
2018.

A Formalization of the LLL Basis Reduction Algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Proceedings of the 9th International Conference on Interactive Theorem Proving,
Lecture Notes in Computer Science 10895,
pp. 160 – 177,
2018.

A verified factorization algorithm for integer polynomials with polynomial complexity

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Archive of Formal Proofs 2018.

A verified LLL algorithm

Ralph Bottesch, Jose Divasón, Max Haslbeck, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Archive of Formal Proofs 2018.

First-Order Terms

Christian Sternagel, René Thiemann

Archive of Formal Proofs,
2018.

Efficient Certification of Complexity Proofs – Formalizing the Perron-Frobenius Theorem

Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada

7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018),
pp. 2-13,
2018.

Stochastic Matrices and the Perron-Frobenius Theorem

René Thiemann

Archive of Formal Proofs 2017.

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel

Proceedings of the 14th International Symposium on Frontiers of Combining Systems,
LNCS 10483,
pp. 3-21,
2017.

Certifying Safety and Termination Proofs for Integer Transition Systems

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

Proceedings of the 26th International Confluence on Automated Deduction,
Lecture Notes in Computer Science 10395,
pp. 454-471,
2017.

Parsing and Printing of and with Triples

Sebastiaan J. C. Joosten

Relational and Algebraic Methods in Computer Science. RAMICS 2017,
Lecture Notes in Computer Science 10226,
pp. 159 – 176,
2017.

A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm

Jose Divason, Sebastiaan J. C. Joosten, Rene Thiemann and Akihisa Yamada

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017),
pp. 17 – 29,
2017.

Subresultants

Sebastiaan Joosten and René Thiemann and Akihisa Yamada

Archive of Formal Proofs 2017.

Reachability, Confluence, and Termination Analysis with State-Compatible Automata

Bertram Felgenhauer and René Thiemann

Information and Computation 253(3),
pp. 467 – 483,
2017.

Relative Termination via Dependency Pairs

José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada

Journal of Automated Reasoning 58(3),
pp. 391 – 411,
2017.

Analyzing Program Termination and Complexity Automatically with AProVE

Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann

Journal of Automated Reasoning,
58(1),
pp. 3 – 31,
2017.

The Factorization Algorithm of Berlekamp and Zassenhaus

Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada

Archive of Formal Proofs 2016.

CeTA – Certifying Termination and Complexity Proofs in 2016

Sebastiaan J.C. Joosten, René Thiemann, and Akihisa Yamada

Proceedings of the 15th International Workshop on Termination (WST 2016),
pp. 20:1,
2016.

Certifying Safety and Termination Proofs for Integer Transition Systems

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

Proceedings of the 15th International Workshop on Termination (WST 2016),
pp. 4:1 – 4:5,
2016.

TermComp 2016 Participant: NaTT

Akihisa Yamada

Proceedings of the 15th International Workshop on Termination (WST 2016),
pp. 25:1,
2016.

Greedy Combinatorial Test Case Generation using Unsatisfiable Cores

Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, and Eun-Hye Choi

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016),
pp. 614 – 624,
2016.

Certifying Exact Complexity Bounds for Matrix Interpretations

Jose Divasón, Sebastiaan Joosten, Ondrej Kuncar, René Thiemann, and Akihisa Yamada

Proceedings of the 16th International Workshop on Logic and Computational Complexity (LCC 2016),
pp. 4 – 7,
2016.

AC Dependency Pairs Revisited

Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016),
Leibniz International Proceedings in Informatics 62,
pp. 8:1 – 8:16,
2016.

A Formalization of Berlekamp’s Factorization Algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada

Isabelle Workshop 2016,
2016.

Algebraic Numbers in Isabelle/HOL

René Thiemann and Akihisa Yamada

Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016),
Lecture Notes in Computer Science 9807,
pp. 391 – 408,
2016.

Perron-Frobenius Theorem for Spectral Radius Analysis

Jose Divasón and Ondřej Kunčar and René Thiemann and Akihisa Yamada

Archive of Formal Proofs 2016.

Polynomial Factorization

René Thiemann and Akihisa Yamada

Archive of Formal Proofs 2016.

Polynomial Interpolation

René Thiemann and Akihisa Yamada

Archive of Formal Proofs 2016.

Formalizing Jordan Normal Forms in Isabelle/HOL

René Thiemann and Akihisa Yamada

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),
pp. 88 – 99,
2016.

Algebraic Numbers in Isabelle/HOL

René Thiemann and Akihisa Yamada

Archive of Formal Proofs 2015.

Formalizing Soundness and Completeness of Unravelings

Sarah Winkler and René Thiemann

Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015),
Lecture Notes in Artificial Intelligence 9322,
pp. 239 – 255,
2015.

Deriving Comparators and Show Functions in Isabelle/HOL

Christian Sternagel and René Thiemann

Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015),
Lecture Notes in Computer Science 9236,
pp. 421 – 437,
2015.

Matrices, Jordan Normal Forms, and Spectral Radius Theory

René Thiemann and Akihisa Yamada

Archive of Formal Proofs 2015.

CoCo Participant: CeTA 2.21

Julian Nagele, Christian Sternagel, Thomas Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl

Proceedings of the 4th International Workshop on Confluence (IWC 2015),
pp. 41,
2015.

Termination Competition (termCOMP 2015)

Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, and Johannes Waldmann

Proceedings of the 25th International Conference on Automated Deduction (CADE-25),
Lecture Notes in Computer Science 9195,
pp. 105 – 108,
2015.

Reducing Relative Termination to Dependency Pair Problems

José Iborra, Naoki Nishida, Germán Vidal, and Akihisa Yamada

Proceedings of the 25th International Conference on Automated Deduction (CADE-25),
Lecture Notes in Artificial Intelligence 9195,
pp. 163 – 178,
2015.

Certification of Complexity Proofs using CeTA

Martin Avanzini, Christian Sternagel, and René Thiemann

Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015),
Leibniz International Proceedings in Informatics 36,
pp. 23 – 39,
2015.

Deriving class instances for datatypes

Christian Sternagel and René Thiemann

Archive of Formal Proofs 2015.

Lifting Definition Option

René Thiemann

Archive of Formal Proofs 2014.