28 citations · 48 across the 13 of their papers we have counts for
5 papers · 1 filter
Towards the Certification of Complexity Proofs
René Thiemann
We report on our formalization of matrix-interpretation in Isabelle/HOL. Matrices are required to certify termination proofs and we wish to utilize them for complexity proofs, too.…
Recording Completion for Finding and Certifying Proofs in Equational Logic
Thomas Sternagel, René Thiemann, Harald Zankl +1
When we want to answer/certify whether a given equation is entailed by an equational system we face the following problems: (1) It is hard to find a conversion (but easy to certify…
A Relative Dependency Pair Framework
Christian Sternagel, René Thiemann
In this paper we generalize the DP framework to a relative DP framework, where a so called split is possible.
Certification extends Termination Techniques
Christian Sternagel, René Thiemann
There are termination proofs that are produced by termination tools for which certifiers are not powerful enough. However, a similar situation also occurs in the other direction. W…
CeTA - A Tool for Certified Termination Analysis
Christian Sternagel, René Thiemann, Sarah Winkler +1
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 increas…