### Certifying Termination and Complexity Proofs of Programs

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. Although undecidable in general, much work has been spent on automated termination and complexity analysis. Whereas the answer to the question for a given program might be simple (yes, the program is terminating), the underlying proof is usually not that simple. In fact, most tools for automated complexity and termination analysis are complex tools, which combine several techniques while trying to analyze the behavior of a program. Consequently, these tools may contain errors and give wrong answers and proofs.

One solution to this problem is the usage of certifiers, which can check the proofs that are generated by the tools. For reliability, the soundness of the certifiers itself has to be formally proven within a theorem prover. Note that with the help of the certifiers, several bugs have been spotted, both in the implementations of the tools, as well as in soundness proofs of termination techniques. Unfortunately, so far the applicability of the available certifiers in this area is rather limited: they mainly handle termination proofs, but not complexity proofs; and they are limited to term rewriting, a simple computational model that underlies much of declarative programming and automated theorem proving.

In this project, we will extend the applicability of certifiers in two important directions: we want to support a large class of complexity proofs, and we want to support termination proofs for the widely used intermediate language LLVM via a translation to integer transition systems. To this end, we will develop several interesting formalizations. This includes a large library on linear algebra, which will be required for dealing with complexity proofs. Moreover, we will define a formal semantics of LLVM in Isabelle/HOL, and verify the translation from LLVM to integer transition systems. Finally, we will develop a certified SMT solver for linear integer arithmetic in order to validate termination proofs of integer transition systems.

Our work will drastically improve the reliability of current termination and complexity tools. Furthermore, it can serve as a starting point for performing other formalizations in the area of program analysis and program transformations.

#### Members

##### Current Members

- Ralph Bottesch
- Max Haslbeck
- René Thiemann

##### Former Members

#### FWF project number

Y757#### Contact

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

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

The 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, 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

The Archive of Formal Proofs, 2015.

Lifting Definition Option

René Thiemann

The Archive of Formal Proofs, 2014.