AProVE’26: Confluence Analysis in a Termination Tool
Authors: J.-C. Kassing, A. Schüßler, T. Sokolowski, and J. Giesl
AProVE (Automated Program Verification Environment) is a tool for fully automatic program verification, focusing on proving termination, analyzing (worst-case) complexity, and verifying safety or infeasibility for a variety of programming languages including term rewriting. Termination and confluence are closely related: local confluence reduces the termination analysis of overlay systems to innermost rewriting, and confluence becomes decidable once termination is guaranteed. After first participating in the Confluence Competition in 2025, AProVE has since added more techniques to both prove and disprove confluence. We present these techniques, including termination-based confluence analysis, modularity, decreasing diagrams based on polynomial interpretations, the utilization of redundant rewrite rules, and disproving confluence via dependency graph approximations and polynomial interpretations.