基于深度学习和反例制导的循环程序秩函数生成

程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函数;验证组件运用可满足性模理论(satisfiability modulo theories,SMT)确保候选秩函数的有效性;而由SMT返回的反例则进一步用于扩展学习组件中的训练集合,以对候选秩函数进行精化.实验结果表明,所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.