Programming errors which cause non-termination can compromise software systems by making them irresponsive. Notorious examples are the Microsoft Zune Z2K bug and the Microsoft Azure Storage service interruption. Termination bugs can also be exploited in denial-of-service attacks. Therefore, proving program termination is important for ensuring software reliability.
The traditional method for proving termination is based on the synthesis of a ranking function, a well-founded metric which strictly decreases during the program execution. The goal of the project was the development of a static analyzer which automatically infers ranking functions and sufficient precondition for program termination (and other liveness properties) by means of abstract interpretation. The static analyzer is open-source and available on GitHub.
- Samuel Ueltschi
Proving Temporal Properties by Abstract Interpretation
Master’s Thesis, ETH Zurich, SS 2017
- Nathanaëlle Courant
Precise Widenings for Proving Termination by Abstract Interpretation
L3 Internship, ETH Zurich, 2016
- Lukas Neukom
Termination Analysis of Heap-Manipulating Programs by Abstract Interpretation
Master’s Thesis, ETH Zurich, SS 2016