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⁸ – 5x⁶ + 7x³ – 17 without any rounding errors.
• 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

Contact

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.