News
 2017/08/14: IsaFoR/CeTA version 2.31 has been released.
 2017/05/29: IsaFoR/CeTA version 2.30 has been released.
 2017/02/23: IsaFoR/CeTA version 2.29 has been released.
 2016/10/11: IsaFoR/CeTA version 2.28 has been released.
 2016/05/12: IsaFoR/CeTA version 2.27 has been released.
 2016/04/15: IsaFoR/CeTA version 2.26 has been released.
Introduction
Welcome to the IsaFoR/CeTA website.
CeTA is a tool that certifies (non)termination or (non)confluence or completion or complexity proofs provided by some automated (termination/complexity/...) tool.
The development is supported by the following projects of the Austrian Science Fund (FWF):
 Certifying Termination and Complexity Proofs of Programs (Y757)
 Certification Redux (P27502)
 Improving Certifiers for Termination Proofs (P22767, finished)
 Formalizing Open Induction, The Tree Theorem, and Simple Termination (J3202, finished)
It mainly consists of two parts.
 An Isabelle/HOL formalization of
abstract results and concrete techniques from the rewriting literature,
in form of the IsaFoR (Isabelle
Formalization of Rewriting) library. Currently the following techniques are supported:
 Termination (rewrite systems, relative rewrite systems, conditional rewrite systems, rewriting modulo AC, integer transition systems):
 Dependency Pairs (incl. Dershowitz' refinement)
 Dependency Pair Framework
 Dependency Graph Processor (E(I)DG^{***}estimation, i.e., using tcap and using both forward and backward directions, and in the innermost case additionally icap)
 Reduction Pair Processors in several variants
 Polynomial interpretations over naturals, rationals, arctic and arcticbelowzero semiring, and over matrices of all these domains. Moreover, for interpretations over the rationals and naturals, negative constants are allowed.
 Lexicographic, multiset, and recursive path order with argument filters and arbitrary permutations of arguments
 KnuthBendix order with subterm coefficient functions, argument filters and arbitrary permutations of arguments
 Usable Rules (also with respect to argument filterings)
 Subterm Criterion
 Semantic Labeling
 Flat Context Closure (for every TRS and for DP problems with leftlinear Rcomponent)
 RootLabeling
 SizeChange Termination (also the SizeChange in NP variant which allows to delete only some pairs)
 String Reversal
 Uncurrying
 Match and roofbounds
 Switch between full and innermost rewriting
 DP Transformations Narrowing, Rewriting, and (Forward)Instantiation
 Bounded Increase
 Unravelings
 Cooperation Graphs
 Lexicographic ranking functions
 Invariants via Impact algorithm
 Fresh variable and location addition
 SCC decomposition of program graph
 Nontermination (rewrite systems and relative rewrite systems):
 Loops (also for innermost and outermost strategy and forbidden patterns)
 Nonlooping infinite rewrite sequences
 Regular languages which are closed under rewriting and do not contain normal forms
 TRSs violating the variable condition
 String reversal
 Rule removal
 Dependency pairs
 DP Transformations Narrowing, Rewriting, and (Forward)Instantiation
 Switch from innermost to full rewriting
 Partial nontermination proofs
 Complexity:
 Weak dependency pairs and dependency tuples
 Usable rules and usable replacement maps
 Strongly linear polynomial interpretation (in case of runtime complexity: arbitrary interpretations for defined symbols)
 Matrix interpretations of arbitrary shape
 Runtime complexity and derivational complexity
 Rule shifting for relative rewriting
 (Relative) Matchbounds
 Confluence and nonconfluence:
 Unravelings for ultra leftlinear deterministic conditional TRSs of type 3
 Addition and removal of redundant rules
 Rule labeling and relative termination (valley and conversion versions)
 Local confluence via critical pairs
 Weak orthogonality
 Linear + strongly closed
 Leftlinear + almost parallel closed
 Terminating criticalpairclosing systems
 Nonjoinable forks using tcap, tree automata techniques, usable rules, interpretations, or discrimination pairs
 Modularity of nonconfluence
 Newman's Lemma
 Completion:
 Requires rewrite sequences how to obtain R from E, and a termination proof of R
 Equational Reasoning:
 Birkhoff's theorem
 certification via completed rewrite system, proof tree using equational logic, or derivation
 Safety:
 Invariants via Impact algorithm
 Termination (rewrite systems, relative rewrite systems, conditional rewrite systems, rewriting modulo AC, integer transition systems):
 The certifier CeTA, an automatically generated Haskell program (using the code generation feature of Isabelle) for certifying proofs.
Publications

J. Nagele, B. Felgenhauer, and H. Zankl
Certifying Confluence Proofs via Relative Termination and Rule Labeling
Logical Methods in Computer Science 13(2:4), pp. 1–27, 2017.
 A. Yamada, C. Sternagel, R. Thiemann, and K. Kusakari
AC Dependency Pairs Revisited.
In Proc. of the 25th EACSL Annual Conference on Computer Science Logic (CSL'16), LIPIcs 62, pages 8:1–8:16. 
J. Nagele and A. Middeldorp
Certification of Classical Confluence Results for LeftLinear Term Rewrite Systems.
In Proc. of the 7th International Conference on Interactive Theorem Proving (ITP'16), LNCS 9807, pages 290–306, 2016. © SpringerVerlag  R. Thiemann and A. Yamada.
Algebraic Numbers in Isabelle/HOL
In Proc. of the 7th International Conference on Interactive Theorem Proving (ITP '16), Lecture Notes in Computer Science 9807, pages 391408, 2016. © SpringerVerlag  R. Thiemann and A. Yamada.
Formalizing Jordan Normal Forms in Isabelle/HOL
In Proc. of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '16), pages 8899, 2016.  C. Sternagel and T. Sternagel
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion.
In Proc. of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD'16), LIPIcs 52, pages 29:1–29:16.  S. Winkler and R. Thiemann.
Formalizing Soundness and Completeness of Unravelings
In Proc. of the 10th International Symposium on Frontiers of Combining Systems (FroCoS '15), Lecture Notes in Artificial Intelligence 9322, pages 239255, 2015. © SpringerVerlag  C. Sternagel and R. Thiemann
Deriving Comparators and Show Functions in Isabelle/HOL.
In Proc. of the 6th International Conference on Interactive Theorem Proving (ITP'15), LNCS 9236, pages 421–437, 2015. © SpringerVerlag  M. Avanzini, C. Sternagel, and R. Thiemann
Certification of Complexity Proofs using CeTA.
In Proc. of the 26th International Confluence of Rewriting Techniques and Applications (RTA'15), LIPIcs 36, pages 23–39, 2015.  J. Nagele, B. Felgenhauer, and A. Middeldorp
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules.
In Proc. of the 26th International Confluence of Rewriting Techniques and Applications (RTA'15), LIPIcs 36, pages 257–268, 2015.  J. Nagele and H. Zankl
Certified Rule Labeling.
In Proc. of the 26th International Confluence of Rewriting Techniques and Applications (RTA'15), LIPIcs 36, pages 269–284, 2015.  C. Sternagel and R. Thiemann
A Framework for Developing StandAlone Certifiers.
Electronic Notes in Theoretical Computer Science, 312:5167, 2015.  C. Sternagel and R. Thiemann.
The Certification Problem Format.
In Proc. of the 11th Workshop on User Interfaces for Theorem Provers (UITP'14), EPTCS 167, pages 61–72, 2014.  J. Nagele and R. Thiemann.
Certification of Confluence Proofs using CeTA.
In Proc. of the 3rd International Workshop on Confluence (IWC'14), pages 19–23, 2014.  J. Nagele, R. Thiemann, and S. Winkler
Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations
In Proc. of the 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '14), LNCS 8471, pages 216–232, 2014. © SpringerVerlag  C. Sternagel and R. Thiemann.
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs.
In Proc. of the Joint 25th International Conference on Rewriting Techniques and Applications (RTA'14) and 12th International Conference on Typed Lambda Calculi and Applications (TLCA'14), LNCS 8560, pages 441–455, 2014. © SpringerVerlag  R. Thiemann.
Formalizing Bounded Increase.
In Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13), LNCS 7998, pages 245–260, 2013. © SpringerVerlag  C. Sternagel and R. Thiemann.
Formalizing KnuthBendix Orders and KnuthBendix Completion.
In Proc. of the 24th International Conference on Rewriting Techniques and Applications (RTA'13), LIPIcs 21, pages 287–302, 2013.  C. Sternagel and R. Thiemann.
Certification of Nontermination Proofs.
In Proc. of the 3rd International Conference on Interactive Theorem Proving (ITP'12), LNCS 7406, pages 266–282, 2012. © SpringerVerlag  T. Sternagel, R. Thiemann, H. Zankl and C. Sternagel.
Recording Completion for Finding and Certifying Proofs in Equational Logic.
In Proc. of the 1st International Workshop on Confluence (IWC'12), pages 31–36, 2012.  R. Thiemann, G. Allais, and J. Nagele.
On the formalization of termination techniques based on multiset orderings.
In Proc. of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12), LIPIcs 15, pages 339–354, 2012.
 C. Sternagel and R. Thiemann.
A Relative Dependency Pair Framework.
In Proc. of the 12th International Workshop on Termination (WST'12), 2012.
 C. Sternagel and R. Thiemann.
Generalized and Formalized Uncurrying.
In Proc. of the 8th International Symposium Frontiers of Combining Systems (FroCoS'11), LNAI 6989, pages 243–258, 2011. © SpringerVerlag  A. Krauss, C. Sternagel, R. Thiemann, C. Fuhs, and J. Giesl.
Termination of Isabelle Functions via Termination of Rewriting.
In Proc. of the 2nd International Conference on Interactive Theorem Proving (ITP'11), LNCS 6898, pages 152–167, 2011. © SpringerVerlag  C. Sternagel and R. Thiemann.
Modular and Certified Semantic Labeling and Unlabeling.
In Proc. of the 22nd International Conference on Rewriting Techniques and Applications (RTA'11), LIPIcs 10, pages 329–344.  C. Sternagel.
Automatic Certification of Termination Proofs.
PhD Thesis, 2010.  C. Sternagel and R. Thiemann.
Signature Extensions Preserve Termination  An Alternative Proof via Dependency Pairs.
In Proc. of the 19th EACSL Annual Conferences on Computer Science Logic (CSL '10), LNCS 6247, pages 514–528, 2010. © SpringerVerlag  C. Sternagel and R. Thiemann.
Certified Subterm Criterion and Certified Usable Rules.
In Proc. of the 21st International Conference on Rewriting Techniques and Applications (RTA'10), LIPIcs 6, pages 325–340, 2010.  H. Zankl, C. Sternagel, D. Hofbauer, and A. Middeldorp.
Finding and Certifying Loops.
In Proc. of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'10), LNCS 5901, pages 755–766, 2010. © SpringerVerlag  R. Thiemann and C. Sternagel.
Certification of Termination Proofs using CeTA.
In Proc. of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), LNCS 5674, pages 452–468, 2009. © SpringerVerlag  C. Sternagel, R. Thiemann, S. Winkler, and H. Zankl.
CeTA  A Tool for Certified Termination Analysis.
In Proc. of the 10th International Workshop on Termination (WST'09), 2009.
Downloads
The current version is 2.31. To access previous versions of CeTA and see the differences please visit this site.
Binaries of our tool are available for the following platforms:
 Linux (x86 64bit)
 Mac OS X (x86 64bit)
 Windows 10 (x86 64bit)
Alternatively, you may download the sourcecode for CeTA. Please have a look into the README for installation instructions.
You can directly browse or download the sources of all releases and the current development snapshot of our Isabelleformalization IsaFoR in the Mercurial repository.
Contact
For general questions to the developers send a mail to ceta@informatik.uibk.ac.at. You can also subscribe and send messages to the CeTA users mailing list where your messages will be posted to all CeTA users, and where the developers will inform you about updates, ... .
LaTeX Macros for Typesetting IsaFoR/CeTA
In order to refer to our library and our certifier in your LaTeX documents correctly, please use the following macros:\newcommand\isafor{\textsf{Isa\kern0.2exF\kern0.2exo\kern0.2exR}} \newcommand\ceta{\textsf{C\kern0.2exe\kern0.5exT\kern0.5exA}}The results should look approximately as follows:
Old News
 Using a special version of AProVE which only uses supported techniques, CeTA can certify 1395 proofs for the 2132 TRSs in the TPDB version 7.0 (1242 termination proofs and 153 nontermination proofs). The total certification time for all these proofs is about one minute, where the average time is 0.05 seconds.
 Using TTT2, CeTA can certify 1444 proofs for the 2132 TRSs in the TPDB version 7.0 (1223 termination proofs and 221 nontermination proofs).
 When combining AProVE and TTT2, CeTA can certify proofs for 1522 TRSs (1289 termination proofs and 233 nontermination proofs), i.e., for over 70% of the TRSs in the TPDB.

Using CeTA, we obtained the first automatically certified proof of Touzet's SRS (
TRS/Zantema_04/z090.xml
in the TPDB7.0.2). This is the first (and currently only) automatic proof of this SRS. It incorporates the following processors: monotonic reduction pairs, reduction pairs with usable rules, closure under flat contexts, and rootlabeling.
 2012/04/19: IsaFoR/CeTA version 2.4 has been released. This version can certify all 5413 certification problems that have been generated during the full run of termination tools on the TPDB (version 8.0) in 2011. Moreover, it can certify complexity proofs and proofs including KnuthBendix orders and nonlooping nonterminating derivations.
 2011/02/19: IsaFoR provides a link between the proof assistant Isabelle and external termination provers. The approach is described in the paper Termination of Isabelle Functions via Termination of Rewriting and examples of its usage may be found here.