Experiments
In the following we give some experimental results for different versions of CeTA.
- Version 2.39
We tested this version of CeTA for the paper Certifying the Weighted Path Order (FSCD'20). The results within the paper have been obtained in combination with NaTT and TTT2. - Version 2.38
We tested this version of CeTA for the paper Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL (NFM'20). The results within the paper have been obtained in combination with Z3 and CVC4. - Version 2.30
We tested this version of CeTA for the paper Certifying Safety and Termination Proofs for Integer Transition Systems (CADE'17). The results within the paper have been obtained in combination with AProVE and T2 temporal prover. - Version 2.23
We tested this version of CeTA for the paper Formalizing Jordan Normal Forms in Isabelle/HOL (CPP'16). The results within the paper have been obtained in combination with AProVE, CaT and TcT. - Version 2.19
We tested this version of CeTA for the paper Certification of Complexity Proofs using CeTA (RTA'15). The results within the paper have been obtained in combination with AProVE and TcT. - Version 2.14.1
We tested this version of CeTA for the paper Certification of Nontermination Proofs using Strategies and Nonlooping Derivations (VSTTE'14). The results within the paper have been obtained in combination with AProVE and TTT2. - Version 2.13
We collected some examples for the usage of (monotone) interpretations for the paper Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs (RTA-TLCA'14).
- Version 2.4
We tested this version of CeTA on all 5413 certification problems that have been generated during the full run of termination tools on the TPDB (version 8.0.1) in 2011. This collections contains proofs generated by AProVE, CiME3, and TTT2. It turns out, that all proofs can be certified using this version of CeTA. - Version 2.3
We tested this version of CeTA for the paper Certification of Nontermination Proofs (ITP'12).
The results within the paper have been obtained in combination with AProVE. - Version 2.2
We tested this version of CeTA for the paper On the formalization of termination techniques based on multiset orderings (RTA'12).
The results within the paper have been obtained in combination with AProVE. - Version 1.18
We tested this version of CeTA for the paper Generalized and Formalized Uncurrying (FroCoS'11).
The results within the paper have been obtained in combination with TTT2. - Version 1.17
We tested this version of CeTA for the paper Modular and Certiļ¬ed Semantic Labeling and Unlabeling (RTA'11).
The results within the paper have been obtained in combination with AProVE. A rerun with a newer version of AProVE (which besides other improvements does not contain the LPO-output bug anymore) yields the following improved results. Note that the strategies to run AProVE are identical in both experiments. - Version 1.10
We tested this version of CeTA for the paper Certified Subterm Criterion and Certified Usable Rules (RTA'10).
For the experiments of CeTA in combination with AProVE we used the version that was submitted to the 2009 termination competition; for the experiments of CeTA in combination with TTT2 we used the TTT2 version corresponding to changeset a5b22ac1840e of the mercurial repository. - Version 1.03
We tested this version of CeTA for the paper Certification of Termination Proofs using CeTA (TPHOLs'09).
The results have been obtained in combination with the termination tool TTT2.