CiME 3 is a rewriting toolbox that
provides Coq certificates for termination, local confluence and
convergence, and equality proofs (standard rewriting).
Termination proofs may be obtained using various criteria:
as well as various orderings:
- Dependency pairs:
- graphs refinements with or without extended sub-term criterion,
- Polynomial interpretations,
- (extended) Matrix interpretations,
- Full RPO with status, with AFS refinements.
CiME 3 may be used alone (searching for proofs and producing
certificates) or in conjunction with your own prover via xml
input/output and translation to .v files.
supports CPF v2 for the aformentioned techniques.
Output are in Coq scripts only regarding proofs of confluence and of equality.
CiME 3 "release" is here! new syntax for heuristics and ordering parameters, certified proofs of local confluence and convergence, certified proofs of equality (example)...
Binary executables of the tool are available
under CeCill-C licence
(don't hesitate to ask for a binary dedicated to your architecture).
These versions can discover and certify termination proofs of more
than 620 problems of the TRS section (1391 problems) of the TPDB.
Require minisat 2.0. No confluence. Obsolete syntax.
- CiME 3 binaries for i686 64 bits linux: [static]
- CiME 3 binaries for i686 32 bits linux: [static]
- CiME 3 binaries for intel mac OS X: [dynamic]
- Relevant Coccinelle 8.2 version: [tar.gz] (21/01/11)
For any requests, information, announcement, you may subscribe to the cime-club mailing list.