为何仅用Boogie？中间验证语言间的翻译
计算机科学中的逻辑
2016-04-04 v3
摘要
验证系统 Boogie 和 Why3 使用各自的中间语言从高层程序生成验证条件。由于两个系统支持不同的后端证明器（如 Z3 和 Alt-Ergo）并被用于编码不同的高层语言（如 C# 和 Java），能够翻译它们的中间语言将提供一种复用某一系统特性来验证面向另一系统的程序的方式。本文描述了一种将 Boogie 翻译为 WhyML（Why3 的中间语言）的翻译，其在很大程度上保持语义、可验证性和程序结构。我们将该翻译实现为一个工具并应用于来自不同来源和大小的 194 个 Boogie 验证程序；Why3 以与 Boogie 相同的结果验证了 83% 的翻译后程序。这些结果表明该翻译通常是有效且实际适用的。
引用
@article{arxiv.1601.00516,
title = {Why Just Boogie? Translating Between Intermediate Verification Languages},
author = {Michael Ameri and Carlo A. Furia},
journal= {arXiv preprint arXiv:1601.00516},
year = {2016}
}