AProVE: Termination and memory safety of C programs (competition contribution

Abstract. AProVE is a system for automatic termination and complex-ity proofs of C, Java, Haskell, Prolog, and term rewrite systems. The particular strength of AProVE when analyzing C is its capability to rea-son 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. 1 Verification Approach and Software Architecture To analyze programs with explicit pointer arithmetic, one has to handle the interplay between addresses and the values they point to. AProVE uses an ap-proach based on symbolic execution and abstraction to transform the input program into a symbolic execution graph that over-approximates all possible program runs. Language-specific features (such as pointer arithmetic in C) are handled when generating this graph. The nodes of the symbolic execution graph are abstract states that represent sets of actual program states, and paths in the graph correspond to evaluations in the program. To keep the graph finite, w