AProVE: Non-Termination Witnesses for C Programs

To (dis)prove termination of C programs, AProVE uses symbolic execution to transform the program’s LLVM code into an integer transition system, which is then analyzed by several backends. The transformation steps in AProVE and the tools in the backend only produce sub-proofs in their domains. Hence, we now developed new techniques to automatically combine the essence of these proofs. If non-termination is proved, then they yield an overall witness, which identifies a non-terminating path in the original C program.