Program non-termination is a classic undecidable problem, manifesting itself in real-world software in various forms, with a recent example being the Open SSL security vulnerability reported in March 2022. Unintended non-termination typically leads to system unresponsiveness and DoS attacks. We say a program P is non-terminating if at least one path in P does not terminate. In this talk, we first look at the typical root causes for non-termination due to loops and recursion, as surveyed in an FSE’22 paper. We then demonstrate a couple of the current state of the art non-termination checkers on benchmarks where they are unable to identify non-termination.

To address some of the challenges faced by state-of-the-art non-termination checkers, we developed a new sound technique and tool named PROTON: PRObes for Termination Or Not. PROTON works by first instrumenting a given program P with assertions inside each loop of P. These assertions are aimed at detecting recurrent states in P. A recurrent state, loosely speaking, is a program state that recurs. If a program state recurs inside a loop, it proves that the loop does not terminate as long as one keeps executing the path-segment on which a program state recurred, and one can keep on executing this path-segment, thus resulting in a non-termination run. PROTON applies bounded model checking to check if any of the recurrent state assertions get violated. For proving termination, we developed an unsound but high-confidence, bounded-value technique for checking program termination and implemented the same in PROTON. With these sound non-termination and unsound-termination checks, PROTON participated in the Termination category of SV-COMP 2024 and won the same. We present the technical details of PROTON, its architecture, and an experimental evaluation comparing PROTON against other state-of-the-art checkers that participated in SV-COMP 2024.