%0 Journal Article
%T 自动合成数组不变式
%A 李彬
%A 汤恩义
%A 汤震浩
%A 翟娟
%A 赵建华
%J -
%D 2018
%R 10.13328/j.cnki.jos.005463
%X 提出了基于抽象解释框架自动合成数组程序不变式的方法，它能够分析按照特定顺序访问一维或者多维数组的程序，然后合成不变式.该方法将性质（包括区间全称量词性质和原子性质）集合作为抽象域，通过前向迭代数据流分析合成数组性质.证明了该方法的正确性和收敛性，并通过一些实例展示了该方法的灵活性.开发了一种原型工具，该工具在各种数组程序（包括competition on software verification中的array-examples benchmark）上的实验展示了方法的可行性和有效性
%K 不变式合成 抽象解释 数组程序
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=5463&flag=1