We present crest, a tool for automatically proving (non-)confluence and termination of logically constrained rewrite systems. We compare crest to other tools for logically constrained rewriting. Extensive experiments demonstrate the promise of crest.
@article{arxiv.2501.05240,
title = {Automated Analysis of Logically Constrained Rewrite Systems using crest},
author = {Jonas Schöpf and Aart Middeldorp},
journal= {arXiv preprint arXiv:2501.05240},
year = {2025}
}
Comments
Accepted at the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025