AProVE: Termination and Memory Safety of C Programs

AProVE is a system for automatic termination and complexity proofs of C, Java, Haskell, Prolog, and term rewrite systems. The particular strength of AProVE when analyzing C is its capability to reason about pointer arithmetic combined with direct memory accesses as, e.g., in standard implementations of string algorithms. As a prerequisite for termination, AProVE also proves memory safety of C programs.