您好,欢迎来电子发烧友网! ,新用户?[免费注册]

您的位置:电子发烧友网>源码下载>数值算法/人工智能>

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

大小:1.79 MB 人气: 2018-01-12 需要积分:3

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

非常好我支持^.^

(0) 0%

不好我反对

(0) 0%

      发表评论

      用户评论
      评价:好评中评差评

      发表评论,获取积分! 请遵守相关规定!