• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Programming languages and systems >Solving Recursion-Free Horn Clauses over LI+UIF
【24h】

Solving Recursion-Free Horn Clauses over LI+UIF

机译：解决LI + UIF上无递归的Horn子句

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

摘要

Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively automated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexamples can be automated by a series of interpolation queries, or, alternatively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolution to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.
机译：使用依赖于虚假反例进行抽象发现的抽象和优化方​​案，可以有效地自动化具有过程，多线程程序和高阶功能程序的程序验证。可以通过一系列插值查询来自动化反示例的分析，或者通过一系列无递归的Horn子句来表示约束解决查询。 （可以将一组插值查询表述为对未知关系之间具有线性依赖性结构的Horn子句的单个约束。）在本文中，我们提出了一种基于线性实/有理算术和未解释的功能。我们的算法执行解析以处理子句结构，并依赖于部分解决方案来处理功能公理的（非本地）实例。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号