Ctrl is a tool to automatically prove properties of Logically Constrained Term Rewriting Systems (LCTRSs).
Functions of Ctrl (as described in detail in ):
- rewrite a term in an LCTRS to normal form (or mostly normal, as reduction is not always decidable)
- rewrite a constrained term in an LCTRS as far as we can
- analyse confluence, by testing for orthogonality (see )
- analyse termination, following basic techniques in :
- a dependency pair framework
- the basic value criterion for arbitrary theories
- an extension of the value criterion for the integer theory
- the subterm criterion
- analyse term equivalence, that is, inductive theorem proving, both automatically and manually, following techniques in [4,5]
Ctrl uses an external SMT-solver to deal with the constraints. For this, we use Z3, although other smt-solvers can be substituted (provided they also prove unsatisfiability).
The current version of Ctrl is 1.1. Downloads are built for and compiled on linux.
- C. Kop and N. Nishida. Term Rewriting with Logical Constraints. In P. Fontaine, C. Ringeissen, and R. Schmidt, editors, Proceedings of FroCoS 2013, LNAI 8152, 2013. [KopNis13]
- C. Kop and N. Nishida. Constrained Term Rewriting tooL. In M. Davis, A. Fehnker, A. McIver, and A. Voronkov, editors, Proceedings of LPAR 2015, LNCS 9450, 2015. [KopNis15]
- C. Kop. Termination of LCTRSs. In Proceedings of WST 2013, 2013. [Kop13].
- C. Kop and N. Nishida. Automatic Constrained Rewriting Induction towards Verifying Procedural Programs. In J. Garrigue, editor, Proceedings of APLAS 2014, LNCS 8858, 2014. [KopNis14].
- C. Fuhs, C. Kop and N. Nishida. Verifying Procedural Programs via Constrained Rewriting Induction. Transactions on Computational Logic, 2017. To appear. [FuhKopNis17]