论文标题
Cuvée：将SMT-LIB与程序和最弱的先决条件融合
Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions
论文作者
论文摘要
Cuvée是一种程序验证工具，它读取类似SMT-LIB的输入文件，其中术语可能还包含高于抽象程序的最弱的先决条件运算符。 Cuvée通过象征性执行这些程序将这些输入转换为一阶SMT-Lib。 Cuvée使用的输入格式旨在实现类似的工具统一，例如合成循环摘要。 Cuvée本身的一个显着技术方面是随之而来的循环前/后条件而不是不变式，我们演示了这是如何减轻一些简单程序时的注释负担。
Cuvée is a program verification tool that reads SMT-LIB-like input files where terms may additionally contain weakest precondition operators over abstract programs. Cuvée translates such inputs into first-order SMT-LIB by symbolically executing these programs. The input format used by Cuvée is intended to achieve a similar unification of tools for that for example synthesize loop summaries. A notable technical aspect of Cuvée itself is the consequent use of loop pre-/postconditions instead of invariants, and we demonstrate how this lowers the annotation burden on some simple while programs.
