基于数据分类的循环不变式自动生成

作     者：路红 王承毅 黄皓 Lu Hong;Wang Chengyi;Huang Hao

作者机构：南京理工大学紫金学院江苏南京210003 南京大学计算机科学与技术系江苏南京210023 

出 版 物：《计算机应用与软件》 (Computer Applications and Software)

年 卷 期：2023年第40卷第1期

页      面：30-37页

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：江苏省高等学校自然科学研究面上项目(18KJB520022) 江苏高校“青蓝工程”项目 南京理工大学紫金学院2021年度科研项目(2021ZRKX0401002) 南京理工大学紫金学院2020年度科研项目(2020ZRKX0401001) 

主　　题：循环不变式 数据分类 软件验证 静态分析 

摘      要：生成循环不变式是实现程序验证的关键步骤,但人工撰写循环不变式不仅步骤繁琐且容易出错。为此,提出一种基于数据分类的循环不变式生成方法,可直接为C程序的循环语句自动生成循环不变式。该方法生成循环程序的后置条件,并构造其Hoare三元组,通过收集循环程序执行过程中产生的测试数据,并根据其是否满足循环不变式的三个条件进行分类,从而生成循环不变式。所提出的方法在31个基准测试程序上,与目前比较先进的循环不变式生成方法进行比较分析。实验结果表明,所提出的方法不仅能够为C程序自动生成可验证的循环不变式,而且能够为最多的基准测试程序生成有效的循环不变式。