• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Effectively-Propositional Reasoning about Reachability in Linked Data Structures
【24h】

Effectively-Propositional Reasoning about Reachability in Linked Data Structures

机译：链接数据结构中可达性的有效命题推理

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

摘要

This paper proposes a novel method of harnessing existing SAT solvers to verify reachability properties of programs that manipulate linked-list data structures. Such properties are essential for proving program termination, correctness of data structure invariants, and other safety properties. Our solution is complete, i.e., a SAT solver produces a counterexample whenever a program does not satisfy its specification. This result is surprising since even first-order theorem provers usually cannot deal with reachability in a complete way, because doing so requires reasoning about transitive closure. Our result is based on the following ideas: (1) Programmers must write assertions in a restricted logic without quantifier alternation or function symbols. (2) The correctness of many programs can be expressed in such restricted logics, although we explain the tradeoffs. (3) Recent results in descriptive complexity can be utilized to show that every program that manipulates potentially cyclic, singly- and doubly-linked lists and that is annotated with assertions written in this restricted logic, can be verified with a SAT solver. We implemented a tool atop Z3 and used it to show the correctness of several linked list programs.
机译：本文提出了一种利用现有SAT求解器来验证操纵链表数据结构的程序的可达性的新颖方法。此类属性对于证明程序终止，数据结构不变性的正确性以及其他安全属性至关重要。我们的解决方案是完整的，即只要程序不满足其规范，SAT求解器就会产生反例。这个结果令人惊讶，因为即使一阶定理证明通常也不能完全解决可达性，因为这样做需要推理传递闭包。我们的结果基于以下想法：（1）程序员必须以受限的逻辑编写断言，而不能使用量词交替或功能符号。 （2）尽管我们解释了权衡取舍，但许多程序的正确性可以用这种受限的逻辑表示。 （3）描述复杂性的最新结果可以用来表明，每个处理潜在循环，单链接和双链接列表并以此受限逻辑编写的断言进行注释的程序都可以使用SAT求解器进行验证。我们在Z3之上实现了一个工具，并用它来显示几个链表程序的正确性。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号