crest

The Constrained REwriting Software Tool (crest, for short) is an open-source tool to automatically analyze LCTRSs. It is written in Haskell and developed at the University of Innsbruck at the Computational Logic research group as part of the ARI project.

The aim is to provide a tool which analyzes LCTRSs with respect to a given property in an automatic and efficient way. Currently it supports (non-)confluence and (non-)termination analysis, however, extensions for the future are already planned.

What inputs are supported?

A more liberal version of the ARI LCTRS format.

What properties can be verified?

(non-)confluence and (non-)termination

What are the tool’s main techniques for the supported (input, property) pairs?

• confluence analysis: different methods on closure of (parallel) critical pairs and based on the Knuth-Bendix criterion.
• termination analysis: DP framework, value criterion, constrained reduction order, some (experimental) interpretation methods.

What external tools are used? (e.g., compilers, SMT solvers)

• SMT solvers: Z3 (default), CVC5 or Yices2

What is the tool’s URL?

http://cl-informatik.uibk.ac.at/software/crest/

Example(s)

The ARI database consists of hundreds of different (LC)TRSs of which currently more than 100 LCTRS examples are present.

References

• Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp
  Confluence for Logically Constrained Rewrite Systems Revisited
  In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), LNCS (LNAI) 14740, pp. 298 – 316, 2024. DOI

• Jonas Schöpf, Aart Middeldorp
  Confluence Criteria for Logically Constrained Rewrite Systems
  In Proceedings of the 29th International Conference on Automated Deduction (CADE-29 2023), LNCS (LNAI) 14132, pp. 474 – 490, 2023. DOI