Constrained term rewriting tool. This paper discusses Ctrl, a tool to analyse – both automatically and manually – term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and automatically analyse various properties such as termination, confluence and quasi-reductivity. Ctrl also offers both a manual and automatic mode for equivalence tests using inductive theorem proving, giving support for and verification of “hand-written” term equivalence proofs.
Keywords for this software
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
- Kop, Cynthia; Nishida, Naoki: Constrained term rewriting tool (2015)
- Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2014)