CeTA - A Tool for Certified Termination Analysis

TL;DR

CeTA is an automated certification tool for termination proofs, leveraging Isabelle/HOL to verify complex proofs generated by various termination techniques, ensuring correctness and reliability.

Contribution

The paper introduces CeTA, a formal certification tool for termination proofs, integrating it with IsaFoR and Isabelle/HOL for automated correctness verification.

Findings

CeTA successfully certifies complex termination proofs.

It reduces manual effort in proof verification.

The tool enhances trust in automated termination analysis.

Abstract

Since the first termination competition in 2004 it is of great interest, whether a proof that has been automatically generated by a termination tool, is indeed correct. The increasing number of termination proving techniques as well as the increasing complexity of generated proofs (e.g., combinations of several techniques, exhaustive labelings, tree automata, etc.), make certifying (i.e., checking the correctness of) such proofs more and more tedious for humans. Hence the interest in automated certification of termination proofs. This led to the general approach of using proof assistants (like Coq and Isabelle) for certification. We present the latest developments for IsaFoR/CeTA (version 1.03) which is the certifier CeTA, based on the Isabelle/HOL formalization of rewriting IsaFoR.