Abstract

I present a novel abstract interpretation-based static analysis for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software programs. Robust Non-Termination characterizes programs where an externally-controlled input can force infinite execution, independently of other uncontrolled variables. The approach is implemented in the open-source tool FuncTion. I conclude with an overview of the bugs that we accidentally found during its development, longing for a more principled way to uncover such issues.