自动合成数组不变式

摘要：

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

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

所属期刊栏目：29

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金61632015,61561146394;国家重点研发计划2016YFB1000802National Natural Science Foundation of China61632015,61561146394;National Key Research Program2016YFB1000802

在线出版日期：2018-07-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共22页

页码：1544-1565