循环和递归的分析方法研究

Based on the challenges in loop summarization, recursive function summarization and termination analysis, this project will conduct the research on the key technologies of modeling and analyzing loops and recursive function. Specially, the research include three topics: 1) the difficulties of loop analysis including the summarization of non-induction integer variables, the summarization of integer array variables, the relationship between loop invariant and loop summary, and the loop summarization based on machine learning. 2) The difficulties of termination analysis based on the loop analysis and recursive function analysis including cycle reduction on the path dependent automaton (PDA), ranking function inference based on PDA and the lightweight termination analysis based on PDA. 3) The difficulties of recursive function including how to model, analyze and summarize recursive function. The team has made some achievements on the loop summarization and termination analysis in the previous research. We hope to continue to solve the challenges in loop analysis and recursive function analysis in this project. By applying the techniques in program correctness verification, software testing and termination analysis, we can improve the effectiveness and performance. Finally, the software quality can be better guaranteed.

本项目围绕循环总结，递归函数总结以及程序终止性分析三个问题来开展对循环和递归函数建模以及分析的关键技术进行研究。具体研究包括以下三方面：一，循环分析的难点问题：包括不可归纳整型变量的总结，整型数组变量的总结，循环不变量以及循环总结的关系研究以及基于机器学习的循环总结方法研究；二，基于循环与递归函数分析的程序终止性判定的难点问题：包括路径依赖自动机中环约减，基于路径依赖自动机的秩函数计算以及基于路径依赖自动机的轻量级终止性分析方法研究；三，递归函数分析的难点问题：包括递归函数建模、分析与总结。本团队在前期关于循环总结与终止性分析上已经取得了有效的成果，望在本课题中对循环与递归函数分析中的难点问题进一步攻克，并将该理论应用于程序正确性验证、软件测试以及终止性分析等实际应用中以提高其效果及性能，从而更好的保证软件质量。

为了解决程序分析中循环和递归的难点问题，本项目围绕循环分析与总结，递归分析与总结，以及程序终止性分析三个方面对循环和递归问题进行了研究。具体内容包括以下三个方面：1） 循环分析与总结：针对路径依赖自动机的环结构的分类和约减策略，基于路径依赖的整型数组循环总结方法，以及基于路径依赖的循环不变量生成方法。2）递归函数的分析与总结：包括现实程序中，针对非终止递归的细粒度分类，基于路径依赖的递归函数建模方法，以及基于路径依赖的递归函数总结和中终止性分析。3）程序终止性分析：包括基于路径依赖自动机的多路径线性循环终止性分析方法，并对现实程序的非终止性循环进行了分类，最后提出并实现了基于强化学习的程序性能退化性检测和定位技术。本团队在该课题上取得了一系列研究成果，该成果在国际顶级会议ASE， FSE，以及国际顶级期刊TSE，TOSEM， TDSC上发表。此外，课题组2019年获得CCF计算机学会优博论文1篇，2020年获得天津市科技进步一等奖1项。 本项目的研究，部分解决了1）如何对循环问题进行分类，建模，抽象，以及简化，2）如何对递归函数分类和建模，3）如何检测和分析实际程序中的循环与递归的非终止问题，三个主要的科学问题，为未来的相关研究提供了解题思路和研究方法。