Several techniques have been developed to prove the termination of programs. Finding ranking functions is one of the common approaches to do so. A ranking function must be bounded and must reduce at every iteration for all the reachable program states. Since the set of reachable states is often unknown, invariants serve as an over-approximation. Further, in the case of nested loops, the initial set of program states for the nested loop can be determined by the invariant of the outer loop. So, invariants play an important role in proving the validity of a ranking function in the absence of the exact reachable states. However, in the existing techniques, either the invariants are synthesized independently, or combined with ranking function synthesis into a single query, both of which are inefficient. We observe that a guided search for invariants and ranking functions can have benefits in terms of the number of programs that can be proved to terminate and the time needed to identify a proof of termination. So, in this work, we develop Syndicate, a novel framework that synergistically guides the search for both the ranking function and an invariant that together constitute a proof of termination. Owing to our synergistic approach, Syndicate can not only prove the termination of more benchmarks but also achieves a reduction ranging from 17% to 70% in the average runtime as compared to existing state-of-the-art termination analysis tools. We also prove that Syndicate is relatively complete, i.e., if there exists a ranking function and an invariant in their respective templates that can be used to prove the termination of a program, then Syndicate will always find it if there exist complete procedures for the template-specific functions in our framework.

翻译：[摘要] 已有多种技术被开发用于证明程序的终止性。寻找秩函数是其中常用方法之一。秩函数必须满足有界性，并且在所有可达程序状态的每次迭代中保持递减。由于可达状态集合往往是未知的，不变量可作为其过度近似。此外，对于嵌套循环而言，内层循环的初始程序状态可由外层循环的不变量确定。因此，在缺乏精确可达状态的情况下，不变量对证明秩函数的有效性起着关键作用。然而现有技术中，不变量要么独立合成，要么与秩函数合成合并为单一查询，这两种方式效率均不理想。我们观察到，对不变量与秩函数进行引导式搜索，能够提升可证明终止的程序数量及识别终止证明所需时间。为此，本文提出新型框架Syndicate，通过协同引导搜索方式，同步寻找构成终止证明的不变量与秩函数。得益于协同方法，Syndicate不仅能证明更多基准程序的终止性，相比现有最先进的终止分析工具，其平均运行时间还降低了17%至70%。我们还证明了Syndicate的相对完备性：若存在符合各自模板的秩函数与不变量可用于证明程序终止性，且本框架中具备模板特定函数的完备过程，则Syndicate总能发现该证明。