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]):

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.


  1. 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]
  2. 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]
  3. C. Kop. Termination of LCTRSs. In Proceedings of WST 2013, 2013. [Kop13].
  4. 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].
  5. C. Fuhs, C. Kop and N. Nishida. Verifying Procedural Programs via Constrained Rewriting Induction. Transactions on Computational Logic, 2017. To appear. [FuhKopNis17]