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

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

来源：软件学报, 2016, 27(07): 1741-1756.

DOI：10.13328/j.cnki.jos.004836

• 抽象解释
• 抽象域
• 不变式
• 析取语义
• 循环分解

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

• 单位
  计算机软件新技术国家重点实验室; 南京大学; 国防科学技术大学计算机学院