• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Computer Aided Verification(CAV 2006); 20060817-20; Seattle,WA(US) >Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop
【24h】

Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop

机译：在谓词抽象和优化循环内使用静态计算的不变式

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Predicate abstraction is a powerful technique for extracting finite-state models from often complex source code. This paper reports on the usage of statically computed invariants inside the predicate abstraction and refinement loop. The main idea is to selectively strengthen (conjoin) the concrete transition relation at a given program location by efficiently computed invariants that hold at that program location. We experimentally demonstrate the usefulness of transition relation strengthening in the predicate abstraction and refinement loop. We use invariants of the form ±x±y≤c where c is a constant and x,y are program variables. These invariants can be discovered efficiently at each program location using the octagon abstract domain. We observe that the abstract models produced by predicate abstraction of strengthened transition relation are more precise leading to fewer spurious counterexamples, thus, decreasing the total number of abstraction refinement iterations. Furthermore, the length of relevant fragments of spurious traces needing refinement shortens. This leads to an addition of fewer predicates for refinement. We found a consistent reduction in the total number of predicates, maximum number of predicates tracked at a given program location, and the overall verification time.
机译：谓词抽象是一种从经常复杂的源代码中提取有限状态模型的强大技术。本文报告了谓词抽象和细化循环内静态计算的不变式的用法。主要思想是通过有效计算保持在给定程序位置处的不变式，有选择地增强（合并）给定程序位置处的具体过渡关系。我们通过实验证明了过渡关系增强在谓词抽象和细化循环中的有用性。我们使用形式为±x±y≤c的不变量，其中c为常数，x，y为程序变量。使用八边形抽象域，可以在每个程序位置有效地发现这些不变量。我们观察到，由强化过渡关系的谓词抽象产生的抽象模型更加精确，从而导致更少的虚假反例，从而减少了抽象提炼迭代的总数。此外，需要完善的伪迹的相关片段的长度缩短了。这导致添加更少的谓词以进行细化。我们发现谓词总数，在给定程序位置跟踪的谓词最大数量以及总的验证时间持续减少。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号