Synthesis of ranking functions using extremal counterexamples
Synthesis of ranking functions using extremal counterexamples
复制标题
使用极值反例综合排名函数
DOI：
10.1145/2737924.2737976
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Gabriel Radanne
中科院分区：
文献类型：
--
作者：
L. Gonnord;D. Monniaux;Gabriel Radanne
我们提出了一种完整的方法，用于合成词典线性排名函数（从而证明终止），并由电感不变性支持，如果程序的过渡关系包括分离和存在（控制流的大块编码），则在情况下支持。先前的工作要么将在每个基本块头上合成排名函数，而不仅仅是循环标头，从而降低了可能被证明是终止的程序的范围，或者扩展了包括测试在内的大块过渡，以前（指数为许多）基本过渡计算排名函数，从而产生非常大的全局约束系统。相比之下，根据极端反例，我们的算法会逐步完善全局线性约束系统：仅包括排除虚假解决方案的约束。与其他系统相比，我们工具白蚁的实验显示出明显的性能和可伸缩性。
We present a complete method for synthesizing lexicographic linear ranking functions (and thus proving termination), supported by inductive invariants, in the case where the transition relation of the program includes disjunctions and existentials (large block encoding of control flow). Previous work would either synthesize a ranking function at every basic block head, not just loop headers, which reduces the scope of programs that may be proved to be terminating, or expand large block transitions including tests into (exponentially many) elementary transitions, prior to computing the ranking function, resulting in a very large global constraint system. In contrast, our algorithm incrementally refines a global linear constraint system according to extremal counterexamples: only constraints that exclude spurious solutions are included. Experiments with our tool Termite show marked performance and scalability improvements compared to other systems.