Cuvée：将 SMT-LIB 与程序和最弱前置条件相融合
计算机科学中的逻辑
2020-10-13 v1
摘要
Cuvée 是一个程序验证工具，读取类 SMT-LIB 的输入文件，其中项可额外包含关于抽象程序的最弱前置条件算子。Cuvée 通过符号执行这些程序将此类输入翻译为一阶 SMT-LIB。Cuvée 所用的输入格式旨在实现类似于工具统一的目标，例如用于合成循环摘要。Cuvée 自身一个值得注意的技术方面是连贯地使用循环前/后置条件而非不变式，我们展示了这如何降低某些简单 while 程序上的标注负担。
引用
@article{arxiv.2010.05023,
title = {Cuv\'ee: Blending SMT-LIB with Programs and Weakest Preconditions},
author = {Gidon Ernst},
journal= {arXiv preprint arXiv:2010.05023},
year = {2020}
}