AProVE: Becoming Open Source and Recent Improvements
Authors: F. Frohn, C. Fuhs, J. Giesl, J.-C. Kassing, N. Lommen
AProVE (Automated Program Verification Environment) is a tool for fully automatic program verification. More precisely, AProVE is able to analyze termination, complexity, and safety of different programming languages, e.g., Java, C, Haskell, and Prolog. To ensure the correctness of its analysis, AProVE can generate certificates that can be checked by external certification tools. Since the last workshop on termination, several improvements were developed within AProVE: we announce that AProVE is being released as an open source tool, present its first participation in the annual Confluence Competition (CoCo), and describe improved termination and complexity analysis for probabilistic, relative, and standard term rewriting, as well as improved analysis of C programs through new versions of the tools KoAT and LoAT.