软件学报

作者：林开鹏，梅国泉，林望，丁佐华

单位：林开鹏，浙江理工大学 信息学院, 浙江 杭州 31001811,梅国泉，浙江理工大学 信息学院, 浙江 杭州 31001802,林望，浙江理工大学 信息学院, 浙江 杭州 31001803,丁佐华，浙江理工大学 信息学院, 浙江 杭州 31001804

关键词：秩函数;反例制导方法;深度神经网络;终止性分析;循环程序

基金：浙江省自然科学基金(LY20F020020);上海工业控制系统安全创新功能型平台开放课题;上海工业控制安全创新科技有限公司资助课题

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

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期