基于机器学习的循环不变式自动生成方法

摘要

本发明公开了基于机器学习自动生成循环不变式的方法。首先对含循环语句的计算机程序依据一定的算法得到循环语句的后置条件，构造循环语句对应的Hoare三元组；然后依据循环语句的前置条件随机生成测试数据，以这些测试数据为循环变量的初始值运行循环语句，收集程序状态，构造数据集SV；对数据集SV中的每一组数据依据Hoare三元组进行分类标注形成分类数据集；利用KSVM算法对所收集的分类数据集进行分类，生成候选循环不变式；利用反证法对生成的候选不变式进行有效性验证，得到经验证的有效循环不变式。本发明实现了面向可运行的C程序的自动生成循环不变式，且支持生成提供形式更加丰富的循环不变式，能够大大减少形式化验证中循环语句自动验证的工作量。