One Logic to Use Them All
One Logic to Use Them All
复制标题
一种逻辑即可使用所有这些
DOI：
10.1007/978-3-642-38574-2_1
复制
发表时间：
2013
影响因子：
3.9
通讯作者：
J. Filliâtre
中科院分区：
文献类型：
--
作者：
J. Filliâtre
演绎程序验证这几天进展很快。其中一个原因是定理证明者在过去20年里有了巨大的进步。这包括各种类型的自动定理证明器，如ATP系统和SMT解算器，以及交互式证明助手。然而，大多数程序验证工具都是围绕单个定理证明器构建的。相反，我们捍卫这样一种观点，即协同使用几个证明者是更容易和更快验证的关键。
本文介绍了一种针对广泛的定理证明者而设计的逻辑。它是一阶逻辑的扩展，具有多态、代数数据类型、递归定义和归纳谓词。它已在工具Why3中实现，并已成功地用于许多非平凡程序的验证。
Deductive program verification is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verification are built around a single theorem prover. Instead, we defend the idea that a collaborative use of several provers is a key to easier and faster verification.
This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of first-order logic with polymorphism, algebraic data types, recursive definitions, and inductive predicates. It is implemented in the tool Why3, and has been successfully used in the verification of many non-trivial programs.
抽象状态机、Alloy、B、VDM 和 Z
DOI：
10.1007/978-3-642-30885-7_18
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Jones C
通讯作者：
Jones C
影响因子：
0.6
作者：
Blanchette J
通讯作者：
Blanchette J