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
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.