| 自动合成数组不变式 |
| |
| 引用本文： | 李彬,翟娟,汤震浩,汤恩义,赵建华.自动合成数组不变式[J].软件学报,2018,29(6):1544-1565. |
| |
| 作者姓名： | 李彬 翟娟 汤震浩 汤恩义 赵建华 |
| |
| 作者单位： | 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023,计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023,计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023,计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023,计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 |
| |
| 基金项目： | 国家自然科学基金（61632015，61561146394）；国家重点研发计划项目课题（2016YFB1000802） |
| |
| 摘 要： | 本文提出了一个基于抽象解释框架自动合成数组程序不变式的方法.它能够分析按照特定顺序访问一维或者多维数组的程序，然后合成不变式.该方法将性质（包括区间全称量词性质和原子性质）集合作为抽象域，通过前向迭代数据流分析合成数组性质.本文证明了该方法的正确性和收敛性，并通过一些实例展示了该方法的灵活性.我们开发了一个原型工具.该工具在各种数组程序（包括Competition on Software Verification中的array-examples benchmark）上的实验展示了方法的可行性和有效性.
|
| 关 键 词： | 不变式合成 抽象解释 数组程序 |
| 收稿时间： | 2017/6/30 0:00:00 |
| 修稿时间： | 2017/9/1 0:00:00 |
Automatic Invariant Synthesis for Array Programs |
| |
| LI Bin,ZHAI Juan,TANG Zhen-Hao,TANG En-Yi and ZHAO Jian-Hua.Automatic Invariant Synthesis for Array Programs[J].Journal of Software,2018,29(6):1544-1565. |
| |
| Authors: | LI Bin ZHAI Juan TANG Zhen-Hao TANG En-Yi and ZHAO Jian-Hua |
| |
| Affiliation: | State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China,State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China,State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China,State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China and State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China |
| |
| Abstract: | This paper proposes a method of using abstract interpretation for discovering properties about array contents in programs which manipulate one-dimensional or multi-dimensional arrays by sequential traversal. The method directly treats invariant properties (including interval universally quantified formulas and atomic formulas) set as abstract domains. It synthesizes invariants by "iterating forward" analysis. Our method is sound and converges in finite time. We demonstrate the flexibility of the method by some examples. The method has been implemented in a prototype tool. The experiments applying the tool on a variety of array programs (including array-examples benchmark of Competition on Software Verification) demonstrate the feasibility and effectiveness of the approach. |
| |
| Keywords: | invariant synthesis abstract interpretation arrays programs |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
