自动合成数组不变式

来源：软件学报杂志2018年第6期北京时间：

作者：李彬,翟娟,汤震浩,汤恩义,赵建华

单位：李彬，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,翟娟，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,汤震浩，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,汤恩义，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002304,赵建华，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002305

摘要：提出了基于抽象解释框架自动合成数组程序不变式的方法，它能够分析按照特定顺序访问一维或者多维数组的程序，然后合成不变式.该方法将性质（包括区间全称量词性质和原子性质）集合作为抽象域，通过前向迭代数据流分析合成数组性质.证明了该方法的正确性和收敛性，并通过一些实例展示了该方法的灵活性.开发了一种原型工具，该工具在各种数组程序（包括competition on software verification中的array-examples benchmark）上的实验展示了方法的可行性和有效性.

关键词：不变式合成;抽象解释;数组程序

基金资助：国家自然科学基金（61632015，61561146394）；国家重点研发计划（2016YFB1000802）