###
Journal of Software:2016.27(7):1741-1756

含有析取语义循环的不变式生成改进方法
潘建东,陈立前,黄达明,孙浩,曾庆凯
(计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 210023;并行与分布处理国防科技重点实验室(国防科学技术大学 计算机学院), 湖南 长沙 410073)
Improving Invariant Generation for Loops Containing Disjunctive Semantics
PAN Jian-Dong,CHEN Li-Qian,HUANG Da-Ming,SUN Hao,ZENG Qing-Kai
(State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China;Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China;National Laboratory for Parallel and Distributed Processing(School of Computer Science, National University of Defense Technology), Changsha 410073, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 2176   Download 1332
Received:December 12, 2014    Revised:March 02, 2015
> 中文摘要: 抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.
Abstract:Abstract interpretation provides a general framework to generate program invariants automatically. However, most existing numerical abstract domains under this framework can only express constraint sets that are geometrically convex. Therefore, using convex abstract domains to analyze special program structures involving disjunctive semantics (whose constraint sets are non-convex) may lead to imprecise results. This paper presents a novel approach based on loop decomposition and deduction to improve invariant generation for loop structures with explicit and implicit disjunctive semantics. This approach can alleviate the problem of great semantic loss during abstract interpretation of loop structures with disjunctive semantics. Compared with existing approaches, experimental results show that the presented approach can generate more precise invariants for loop structures involving disjunctive semantics, which is also helpful for reasoning about certain security properties.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61170070,61572248,61431008,61321491);国家科技支撑计划(2012BAK26B01);国家高技术研究发展计划(863)(2011AA1A202) 国家自然科学基金(61170070,61572248,61431008,61321491);国家科技支撑计划(2012BAK26B01);国家高技术研究发展计划(863)(2011AA1A202)
Foundation items:National Natural Science Foundation of China (61170070, 61572248, 61431008, 61321491); National Key Technology Research and Development Program of the Ministry of Science and Technology of China (2012BAK26B01); National High Technology Research and Development Program of China (863) (2011AA1A202)
Reference text:

潘建东,陈立前,黄达明,孙浩,曾庆凯.含有析取语义循环的不变式生成改进方法.软件学报,2016,27(7):1741-1756

PAN Jian-Dong,CHEN Li-Qian,HUANG Da-Ming,SUN Hao,ZENG Qing-Kai.Improving Invariant Generation for Loops Containing Disjunctive Semantics.Journal of Software,2016,27(7):1741-1756