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:

1. Increase the number of certifiable termination techniques.


2. Better integration of certifiers with termination tools.


3. Use certified proofs for establishing termination of Isabelle/HOL functions.


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

Contact

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.