Why3: Shepherd Your Herd of Provers
Why3: Shepherd Your Herd of Provers
复制标题
原因3：牧养你的证明者群
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
A. Paskevich
中科院分区：
文献类型：
--
作者：
François Bobot;J. Filliâtre;C. Marché;A. Paskevich
Why3 是下一代 Why 软件验证平台。 Why3 明确地将纯逻辑规范部分与程序验证条件的生成部分分开。本文主要讨论前一部分。 Why3 带有一种新的增强型逻辑规范语言。它具有丰富的证明任务转换库，可以链接起来为大量定理证明器（包括 SMT 求解器、TPTP 证明器以及交互式证明助手）生成合适的输入。
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.