自动合成数组不变式

• 作者: 李彬 汤恩义 汤震浩 翟娟 赵建华
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 不变式合成 抽象解释 数组程序
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 形式化方法的理论基础专题
• 页码范围: 1544-1565
• 页数: 22页
• 分类号: TP301
• 字数: 19802字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005463

摘要

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