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

来源：软件学报杂志2016年第7期北京时间：

作者：潘建东,陈立前,黄达明,孙浩,曾庆凯

单位：潘建东，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002311,陈立前，并行与分布处理国防科技重点实验室(国防科学技术大学 计算机学院), 湖南 长沙 41007302,黄达明，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002303,孙浩，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002304,曾庆凯，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002305

摘要：抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.

关键词：抽象解释;抽象域;不变式;析取语义;循环分解

基金资助：国家自然科学基金(61170070,61572248,61431008,61321491);国家科技支撑计划(2012BAK26B01);国家高技术研究发展计划(863)(2011AA1A202)