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

Ranking Function Synthesis for Loop Programs via Counterexample Guided Deep Learning

作　　者：林开鹏 梅国泉 林望 丁佐华 LIN Kai-Peng;MEI Guo-Quan;LIN Wang;DING Zuo-Hua(School of Information Science and Technology,Zhejiang Sci-Tech University,Hangzhou 310018,China)

机构地区：[1]浙江理工大学信息学院,浙江杭州310018

出　　处：《软件学报》2022年第8期2918-2929,共12页Journal of Software

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

摘　　要：程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函数;验证组件运用可满足性模理论(satisfiability modulo theories,SMT)确保候选秩函数的有效性;而由SMT返回的反例则进一步用于扩展学习组件中的训练集合,以对候选秩函数进行精化.实验结果表明,所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.This study proposes a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks.The approach employs a counter example-guided synthesis procedure,where a learner and a verifier interact to synthesize ranking function.The learner trains a candidate ranking function that satisfies the ranking function conditions over a set of sampled data,and the verifier either ensures the validity of the candidate ranking function or yields counterexamples,which are passed back to further guide the learner.The procedure leverages efficient supervised learning algorithm,while guaranteeing formal soundness via SMT solver.The tool SyntheRF is implemented,then,its scalability and effectiveness are evaluated over a set of benchmark examples.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]