Features
Ctrl is a tool to automatically prove properties of Logically Constrained Term Rewriting Systems[1] (LCTRSs).
Functions of Ctrl (as described in detail in [2]):
- 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 [1])
- analyse termination, following basic techniques in [3]:
- 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).
To translate C-programs to LCTRS, we have developed the separate tool c2lctrs (web interface). C2lctrs translates directly to the input format used by Ctrl.
The current version of Ctrl is 1.1. Downloads are built for and compiled on linux.
References
- 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]