一句话：提出基于支持向量机的通用框架 SVMRanker，可为线性与多项式更新的循环程序合成多种秩函数以证明终止性。
程序终止性判定是计算机科学中的经典难题，而合成秩函数是证明终止性的标准手段。现有方法通常针对特定程序类型（如线性更新用线性规划、多项式更新用半定规划）与特定秩函数类型分别设计专用合成算法，每当出现新程序或新秩函数类型便需重复投入大量精力。为此，作者提出 SVMRanker：一个基于支持向量机（SVM）的通用终止性证明框架，能为具有线性与多项式变量更新的循环程序合成不同类型的秩函数。作者在标准基准集上与最先进工具 LassoRanker 对比，实验表明：线性更新程序上两者性能相当，多项式更新程序上 SVMRanker 能处理更多实例，可作为 LassoRanker 的有效补充。
Deciding termination of programs is probably the most famous problem in computer science. Synthesizing ranking functions for programs is a standard way to prove termination of programs. Currently, specific synthesis algorithms have to be developed for each specific type of programs. For instance, the synthesis of ranking functions for programs with linear variables updates is usually based on linear programming techniques and the like, while for programs with polynomial updates, it usually relies on semi-definite programming and the like. The same also applies to the synthesis of different types of ranking functions needed for proving program termination. Each time faced with a new type of programs and a new type of ranking functions, researchers have to spend a considerable amount of effort to develop specialized synthesis algorithms. In this paper, to save this extra effort, we present SVMRanker, a general framework for proving termination of programs, which is able to synthesize different types of ranking functions for programs with both linear and polynomial updates, based on Support-Vector Machines (SVM). We compare SVMRanker with the state-of-the-art tool LassoRanker on standard benchmarks. Empirical results show that SVMRanker is comparable with LassoRanker on programs with linear updates and can manage more programs with polynomial updates, making SVMRanker a valid complement to LassoRanker in proving program termination.
DOI 原文 ·
@inproceedings{paperbot5727,
title = {SVMRanker: a general termination analysis framework of loop programs via SVM},
author = {Xie Li and Yi Li and Yong Li and Xuechao Sun and Andrea Turrini and Lijun Zhang},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3417930}
}