A tool for applying Rewriting Induction (RI) for Logically Constrained Term Rewriting Systems (LCTRSs).
Based on the paper "Verifying Procedural Programs via Constrained Rewriting Induction" by Fuhs, Kop and Nishida [1] and the Ctrl-tool [2].
Made by Jörg Endrullis and Wouter Brozius.
For citing, please see the CITATION.cff
file
[1] C. Fuhs, C. Kop, N. Nishida "Verifying Procedural Programs via Constrained Rewriting Induction" https://dl.acm.org/doi/pdf/10.1145/3060143
[2] C. Kop "Ctrl: Constrained Term Rewriting tooL" http://cl-informatik.uibk.ac.at/software/ctrl/