Jonas Schöpf, Aart Middeldorp
Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025), Lecture Notes in Computer Science 15696, pp. 124-144, 2025.
pdf 
doi:10.46298/LMCS-21(2:10)2025doi:10.46298/LMCS-21(2:10)2025
Abstract
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.
BibTex
@inproceedings{SM-TACAS25, author = "Jonas Schöpf and Aart Middeldorp", title = "Automated Analysis of Logically Constrained Rewrite Systems using crest", booktitle = "Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Arie Gurfunkel and Marijn Heule", series = "Lecture Notes in Computer Science", volume = 15696, pages = "124--144", year = 2025, doi = "10.1007/978-3-031-90643-5_7"}