Automated Analysis of Logically Constrained Rewrite Systems using crest
Jonas Schöpf and 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
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 Entry
@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"
}