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"
}