### Improving Certifiers for Termination Proofs

In a precursor project of Univ.-Prof. Middeldorp a tool CeTA for automatic certification of termination proofs has been developed. The tool is a fully verified program, where all the necessary properties have been proven in the interactive theorem prover Isabelle/HOL. This includes an Isabelle formalization IsaFoR of the mathematical theory that is used in proving termination.

This FWF project on improving automatic certification of termination is based on the previous developments and aims at the following goals:

- Increase the number of certifiable termination techniques.
- Better integration of certifiers with termination tools.
- Use certified proofs for establishing termination of Isabelle/HOL functions.
- Certify complexity bounds of terminating functions.

The whole formalization and the certifier are available on the IsaFoR/CeTA website, where parts of the formalization have also been externalized into the Archive of Formal Proofs.

Concerning goals 1 and 4, one can see continuous progress when looking at the history on versions of CeTA, where it is documented which technique was added during the project. Moreover, also at the various termination and complexity competitions and at the confluence competitions one can see the improvements of CeTA w.r.t. the continuation of this project, since the the number of certifiable proofs was continuously growing.

At both competitions one can also positive results w.r.t. goal 2: there are various automatic tools from different authors which generate certifiable proofs. And the majority of these proofs are indeed accepted by CeTA within a short amount of time, so that one overall one gets a highly reliable workflow for automated termination-, complexity-, and confluence-analysis where certification adds only a low overhead in execution time.

For goal 3 we documented our progress on a separate webpage which explains how to use external termination tools in combination with IsaFoR and CeTA to discharge termination proof obligations within Isabelle/HOL.

#### Members

- Martin Avanzini
- Benedikt Hupfauf
- Julian Nagele
- Christian Sternagel
- Thomas Sternagel
- René Thiemann

#### FWF project number

P22767#### Contact

rene dot thiemann at uibk dot ac dot at#### Publications

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

Bertram Felgenhauer and René Thiemann

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

A Framework for Developing Stand-Alone Certifiers

Christian Sternagel and René Thiemann

Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014),
Electronic Notes in Theoretical Computer Science 312,
pp. 51 – 67,
2015.

XML

Christian Sternagel and René Thiemann

Archive of Formal Proofs 2014.

Certification Monads

Christian Sternagel and René Thiemann

Archive of Formal Proofs 2014.

The Certification Problem Format

Christian Sternagel and René Thiemann

Proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP 2014),
Electronic Proceedings in Theoretical Computer Science 167,
pp. 61 – 72,
2014.

Certification of Nontermination Proofs using Strategies and Nonlooping Derivations

Julian Nagele, René Thiemann, and Sarah Winkler

Proceedings of the 6th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014),
Lecture Notes in Computer Science 8471,
pp. 216 – 232,
2014.

Haskell’s Show-Class in Isabelle/HOL

Christian Sternagel and René Thiemann

Archive of Formal Proofs 2014.

Proving Termination of Programs Automatically with AProVE

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

Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014),
Lecture Notes in Computer Science 8562,
pp. 184 – 191,
2014.

Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling

Alexander Bau, René Thiemann, and Johannes Waldmann

Proceedings of the 14th International Workshop on Termination (WST 2014),
pp. 6 – 10,
2014.

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs

Christian Sternagel and René Thiemann

Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 441 – 455,
2014.

Certification of Confluence Proofs using CeTA

Julian Nagele and René Thiemann

Proceedings of the 3rd International Workshop on Confluence (IWC 2014),
pp. 19 – 23,
2014.

Implementing field extensions of the form Q[sqrt(b)]

René Thiemann

Archive of Formal Proofs 2014.

Reachability Analysis with State-Compatible Automata

Bertram Felgenhauer and René Thiemann

Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA 2014),
Lecture Notes in Computer Science 8370,
pp. 347 – 359,
2014.

Mutually Recursive Partial Functions

René Thiemann

Archive of Formal Proofs 2014.

Formalizing Bounded Increase

René Thiemann

Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013),
Lecture Notes in Computer Science 7998,
pp. 245 – 260,
2013.

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion

Christian Sternagel and René Thiemann

Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
Leibniz International Proceedings in Informatics 21,
pp. 287 – 302,
2013.

A Formalization of Termination Techniques in Isabelle/HOL

René Thiemann

Habilitation thesis, University of Innsbruck, 2013.

Generating linear orders for datatypes

René Thiemann

The Archive of Formal Proofs, 2012.

Towards the Certification of Complexity Proofs

René Thiemann

Proceedings of the Isabelle user Workshop 2012,
2012.

Certification of Nontermination Proofs

Christian Sternagel and René Thiemann

Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012),
Lecture Notes in Computer Science 7406,
pp. 266 – 282,
2012.

Certification of Confluence Proofs using CeTA

René Thiemann

Proceedings of the 1st International Workshop on Confluence (IWC 2012),
pp. 45,
2012.

Recording Completion for Finding and Certifying Proofs in Equational Logic

Thomas Sternagel, René Thiemann, Harald Zankl, and Christian Sternagel

Proceedings of the 1st International Workshop on Confluence (IWC 2012),
pp. 31 – 36,
2012.

On the Formalization of Termination Techniques based on Multiset Orderings

René Thiemann, Guillaume Allais, and Julian Nagele

Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012),
Leibniz International Proceedings in Informatics 15,
pp. 339 – 354,
2012.

Executable Transitive Closures

René Thiemann

The Archive of Formal Proofs,
2012.

A Report on the Certification Problem Format

René Thiemann

Proceedings of the 12th International Workshop on Termination (WST 2012),
pp. 89 – 93,
2012.

A Relative Dependency Pair Framework

Christian Sternagel and René Thiemann

Proceedings of the 13th International Workshop on Termination (WST 2012),
pp. 79 – 83,
2012.

Generalized and Formalized Uncurrying

Christian Sternagel and René Thiemann

Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS 2011),
Lecture Notes in Artificial Intelligence 6989,
pp. 243 – 258,
2011.

Termination of Isabelle Functions via Termination of Rewriting

Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, and Jürgen Giesl

Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011),
Lecture Notes in Computer Science 6898,
pp. 152 – 167,
2011.

Modular and Certified Semantic Labeling and Unlabeling

Christian Sternagel and René Thiemann

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
Leibniz International Proceedings in Informatics 10,
pp. 329 – 344,
2011.

Executable Transitive Closures of Finite Relations

Christian Sternagel and René Thiemann

The Archive of Formal Proofs, 2011.

Loops under Strategies … Continued

René Thiemann, Christian Sternagel, Jürgen Giesl, and Peter Schneider-Kamp

Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010),
Electronic Proceedings in Theoretical Computer Science 44,
pp. 51 – 65,
2010.