AProVE(KoAT+LoAT) - (Competition Contribution)

Abstract

Abstract To (dis)prove termination of programs, uses symbolic execution to transform the program’s code into an integer transition system (ITS). These ITSs are analyzed by our backend tools (for termination) and (for non-termination) which we integrated into our novel framework to replace previously used external backend tools. In this way, we benefit from the recent improvements in the backend tools and . The transformation steps in and the tools in the backend produce sub-proofs which are then combined automatically in order to generate a complete termination proof. If non-termination is proved, then a witness for a non-terminating path in the original program is returned.