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 Standalone Project, project number

P22767

  Contact

rene.thiemann@uibk.ac.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
    The Archive of Formal Proofs, 2014.
  • Certification Monads
    Christian Sternagel and René Thiemann
    The 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
    The 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
    The 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
    The 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.
  • Computing Square Roots using the Babylonian Method
    René Thiemann
    The Archive of Formal Proofs, 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.
Nach oben scrollen