Skip to content

CeTA

Jump to bottom Edit New page
rene edited this page Jul 16, 2024 · 4 revisions

CeTA is an abbreviation for Certified Tool Assertions. CeTA is a Haskell program that has completely been verified in Isabelle/HOL using the IsaFoR, the Isabelle Formalization of Rewriting. It is developed at the University of Innsbruck by the research group Computional Logic, with Christian Sternagel and René Thiemann being the main developers.

The main usage of CeTA is to validate untrusted proofs or to report erroneous reasoning steps. The untrusted proofs are usually generated by tools during the termination competition and the confluence competition, and CeTA is used as a certifier in both competitions since several years.

What inputs are supported?

The untrusted proofs have to be provided in the certification problem format (CPF), an XML-based format that covers several kinds of different proof techniques.

For which programming languages has it support?

Proofs may be given as properties of

  • term rewrite systems,
  • integer transition systems or
  • LLVM (this requires a special version of CeTA).

What properties can be verified?

CeTA certifies validity of proofs of

  • (non-)termination,
  • upper bounds on complexity,
  • (non-)confluence,
  • (non-)reachability or
  • safety.

What are the tool’s main techniques for the supported (input, property) pairs?

CeTA combines various algorithms, which all have fully been verified, including

  • several algorithms known from the TRS community,
  • a linear integer arithmetic solver, and
  • a symbolic evaluation engine for LLVM

What external tools are used? (e.g., compilers, SMT solvers)

  • the Haskell compiler GHC is required for compiling CeTA
  • Isabelle/HOL is required to produce the source of CeTA from IsaFoR
  • during execution of CeTA no further external tools are required

What is the tool’s URL?

Example

CeTA is able to certify the correctness of this confluence proof in a few milliseconds. Note that the example confluence proof also includes a termination proof. There are thousands of example proofs when looking at the certified results of the confluence competition and the termination competition.

References

  • René Thiemann and Christian Sternagel.
    Certification of Termination Proofs using CeTA
    In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), LNCS 5674, pages 452–468, 2009. DOI
Add a custom footer

list of tools

list of challenges

Clone this wiki locally