含有析取语义循环的不变式生成改进方法

发布时间：2017-11-13 20:14

  本文关键词：含有析取语义循环的不变式生成改进方法

  更多相关文章： 抽象解释 抽象域 不变式 析取语义 循环分解

【摘要】：抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.
【作者单位】： 计算机软件新技术国家重点实验室(南京大学);南京大学计算机科学与技术系;并行与分布处理国防科技重点实验室(国防科学技术大学计算机学院);
【基金】：国家自然科学基金(61170070,61572248,61431008,61321491) 国家科技支撑计划(2012BAK26B01) 国家高技术研究发展计划(863)(2011AA1A202)~~
【分类号】：TP311.1
【正文快照】：

【参考文献】

中国期刊全文数据库 前1条

1 陈立前;王戟;侯苏宁;;单变量区间线性不等式抽象域[J];计算机学报;2010年03期

【共引文献】

中国期刊全文数据库 前5条

1 潘建东;陈立前;黄达明;孙浩;曾庆凯;;含有析取语义循环的不变式生成改进方法[J];软件学报;2016年07期

2 魏欧;石玉峰;徐丙凤;黄志球;陈哲;;软件模型检测中的抽象模型研究综述[J];计算机研究与发展;2015年07期

3 王雅文;宫云战;肖庆;;基于区间必然集的测试用例生成方法[J];计算机辅助设计与图形学学报;2013年04期

4 姜加红;陈立前;王戟;;基于浮点区间幂集抽象域的浮点程序分析[J];计算机科学与探索;2013年03期

5 崔宝江;梁晓兵;王禹;王建新;;基于回溯与引导的关键代码区域覆盖的二进制程序测试技术研究[J];电子与信息学报;2012年01期

【二级参考文献】

中国期刊全文数据库 前1条

1 姬孟洛;王怀民;李梦君;董威;齐治昌;;一种基于抽象解释和通用单调数据流框架的值范围分析方法[J];计算机研究与发展;2006年11期

【相似文献】

中国期刊全文数据库 前10条

1 王稚慧,屈延文;不变式产生器——程序验证的重要工具[J];计算机学报;1984年03期

2 邢建英;李梦君;李舟军;;基于不变式生成的循环停机性验证[J];计算机工程与科学;2012年04期

3 陈妼敏;;Abel型常微分方程的Maple求解[J];黄冈师范学院学报;2006年03期

4 张学舟;;反向验证带切变的线性时段不变式[J];科技视界;2013年34期

5 李志武,王安荣;局部公平网的充要条件研究[J];西安电子科技大学学报;2002年06期

6 刘清;一种寻找测试值断言证明程序正确的方法[J];计算机工程;1981年03期

7 杨潇潇;段振华;;良基归纳法在时序逻辑程序不变式验证中的应用[J];计算机科学;2009年06期

8 郑宇军;石海鹤;薛锦云;陈胜勇;;基于形式演算和不变式验证的可信算法程序构造(英文)[J];中国通信;2011年04期

9 明继军,朱关铭,缪淮扣;Z规格说明的系统不变式及其抽取[J];上海大学学报(自然科学版);1999年S1期

10 邹姝稚;对Wirth一个不变式的修正[J];河海大学学报(自然科学版);2000年06期

中国重要会议论文全文数据库 前1条

1 廖理几;郝伟;金泽宸;蒋毅坚;易明;;用张量不变式和协变式方法计算非磁性晶体喇曼效应的张量元[A];中国物理学会光散射专业委员会成立十周年暨第六届学术会议论文集（上）[C];1991年

中国博士学位论文全文数据库 前1条

1 付春雷;基于OWL2DL本体的OCL不变式语义不一致性自动检测研究[D];重庆大学;2014年

中国硕士学位论文全文数据库 前5条

1 田丰;基于不变式的程序验证工具的设计与实现[D];国防科学技术大学;2011年

2 王燕妮;基于不变式的软件故障检测与恢复技术研究[D];国防科学技术大学;2010年

3 杨东晓;基于Daikon的Java程序动态分析技术研究[D];吉林大学;2004年

4 张恺;模情况下二面体群D_(2p)的不变式环(?)[V]~(D_(2p))的Transfer理想[D];大连理工大学;2014年

5 罗清胜;OCL约束验证与实现方法研究[D];江西财经大学;2006年

，

本文编号：1182230