AProVE25: Confluence Analysis in a Termination Tool
Authors: J.-C. Kassing, T. Sokolowski
AProVE (Automated Program Verification Environment) is a tool for fully automatic program verification, with a primary focus on proving termination, analyzing (worst-case) complexity, and verifying safety or infeasibility of different programming languages including term rewriting. Termination and confluence are two closely related properties: local confluence allows us to reduce the analysis of termination to innermost rewrite sequences, and confluence is decidable once termination is guaranteed. We present the confluence and reachability analysis currently implemented in AProVE, which relies on three main techniques: termination-based confluence analysis, modularity results for confluence, and joinability and reachability analysis. In the future, we want to investigate confluence in the probabilistic setting.