终止性分析概述
termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.
非终止性分析 一般和终止性分析共同使用。
由于停机问题是不可判定的，终止性也是不可判定的（且非半可判定）。在不加限制的情况下，任何可靠的终止性证明工具都不是完备的。但是，正如11年的综述文章中所说：
Unfortunately, many have drawn too strong of a conclusion about the prospects of automatic program termination proving and falsely believe we are always unable to prove termination, rather than more benign consequence that we are unable to always prove termination. Phrases like “but that’s like the termination problem” are often used to end discussions that might otherwise have led to viable partial solutions for real but undecidable problems.
Whereas in the past a software developer hoping to build practical tools for solving something related to termination might have been frightened off by a colleague’s retort “but that’s like the termination problem,” perhaps in the future the developer will instead adapt techniques from within modern termination provers in order to develop a partial solution to the problem of interest.
Proving program termination 2011
证明终止性的方法是找termination argument/proof。有很多方法尝试构造证明，本质上都是去寻找 ranking function，但形式可能不同。每一种方法只能从程序的一个方面进行考虑其终止性，无法找到程序终止的全部原因。
目前的研究分为两个大的方向：
- 限定程序的形式，或是ranking function的形式，考虑简单程序的终止性的可判定性以及求解的算法等。一般会表示为 lasso 或简单循环的形式。
- 使用上述简单程序的结论，通过组合或者模块化证明的方法，实现对general形式的程序的终止性证明。一般会提出一种算法的框架，把问题归约到简单程序的情况。
- Terminator采取的是 disjunctive well-founded transition invariant 的方法，基于Ramsey定理。在这种基于transition invariant的方法中，迭代地去为简单程序（反例）寻找ranking function，直到得到valid的 disjunctive well-founded transition invariant
- Ultimate 采取的是 trace abstraction 路径抽象 的方法，迭代地抽取简单 lasso 程序，为其生成秩函数，并用泛化算法尽可能地复用证明，通过自动机操作检查语言的包含关系，从而高效地求解终止性问题。
- Algebraic Program Analysis的框架，通过将子程序生成为 transition formula，问题自然地转换成单循环的（条件）终止性证明问题（Termination analysis without the tears）。循环体有可能不是linear的，此时一般会用到抽象的方法，把循环体的公式抽象成某种可解的子类（CAV21 paper）。
此外，并发程序的终止性 证明也得到了一些研究