cl-banner

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
Nach oben scrollen