CSI: New Evidence - A Progress Report

CSI is a strong automated confluence prover for rewrite systems which has been in development since 2010. In this paper we report on recent extensions that make CSI more powerful, secure, and useful. These extensions include improved confluence criteria but also support for uniqueness of normal forms. Most of the implemented techniques produce machine-readable proof output that can be independently verified by an external tool, thus increasing the trust in CSI. We also report on CSI(boolean AND)oho, a tool built on the same framework and similar ideas as CSI that automatically checks confluence of higher-order rewrite systems.