• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Combining decision procedures by (model-)equality propagation
【24h】

Combining decision procedures by (model-)equality propagation

机译：通过（模型）等价传播组合决策程序

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

摘要

Formal methods in software and hardware design often generate formulas that need to be validated, either interactively or automatically. Among the automatic tools, SMT (Satisfiability Modulo Theories) solvers are particularly suitable to discharge such proof obligations, as their input language is equational logic with symbols from various useful decidable fragments such as uninterpreted symbols, linear arithmetic, and usual data structures like arrays or lists. In this paper, we present an approach to combine decision procedures and propositional solvers into an SMT-solver, based not only on the exchange of deducible equalities between decision procedures, but also on the generation of model equalities by decision procedures. This extends nicely the classical Nelson-Oppen combination procedure in a simple platform to smoothly combine convex and non-convex theories. We show the soundness and completeness of this approach using an original abstract framework to represent and reason about SMT-solvers. We then describe an algorithmic translation of this method, implemented in the kernel of the veriT solver (Bouton et al. (2009)) [9].
机译：软件和硬件设计中的形式化方法通常会生成需要交互或自动验证的公式。在自动工具中，SMT（可满足性模理论）求解器特别适合履行此类证明义务，因为它们的输入语言是方程式逻辑，具有来自各种有用可确定片段的符号，例如未解释的符号，线性算术以及诸如数组或列表。在本文中，我们提出一种将决策程序和命题求解器组合成SMT求解器的方法，不仅基于决策程序之间可推导的相等性交换，而且基于决策程序生成模型相等性。这在一个简单的平台上很好地扩展了经典的Nelson-Oppen组合过程，以平滑地组合凸和非凸理论。我们使用原始的抽象框架来表示和推理有关SMT求解器的方法来证明这种方法的正确性和完整性。然后，我们描述了在veriT求解器的内核中实现的该方法的算法翻译（Bouton等人（2009））[9]。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号