• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(LPAR 2005); 20051202-06; Montego Bay(JM) >Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
【24h】

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination

机译：通过SAT和增量负循环消除确定分离逻辑公式

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

摘要

Separation logic is a subset of the quantifier-free first order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipelined processor designs and timed systems. In this paper, we present a fast decision procedure for separation logic, which combines Boolean satisfiability (SAT) with a graph based incremental negative cycle elimination algorithm. Our solver abstracts a separation logic formula into a Boolean formula by replacing each predicate with a Boolean variable. Transitivity constraints over predicates are detected from the constraint graph and added on a need-to basis. Our solver handles Boolean and theory conflicts uniformly at the Boolean level. The graph based algorithm supports not only incremental theory propagation, but also constant time theory backtracking without using a cumbersome history stack. Experimental results on a large set of benchmarks show that our new decision procedure is scalable, and outperforms existing techniques for this logic.
机译：分离逻辑是无量词一阶逻辑的子集。它已成功用于具有大（或无界）整数值状态变量的系统的自动验证，例如流水线处理器设计和定时系统。在本文中，我们提出了一种分离逻辑的快速决策程序，该程序将布尔可满足性（SAT）与基于图的增量负周期消除算法相结合。我们的求解器通过将每个谓词替换为布尔变量，将分离逻辑公式抽象为布尔公式。从约束图中检测对谓词的传递性约束，并根据需要添加。我们的求解器在布尔级别统一处理布尔值和理论冲突。基于图的算法不仅支持增量理论传播，还支持恒定时间理论回溯，而无需使用繁琐的历史堆栈。在大量基准测试中的实验结果表明，我们的新决策程序具有可扩展性，并且优于该逻辑的现有技术。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号