一句话：提出一种翻译验证方法，可为验证器前端到中间验证语言的翻译自动生成 Isabelle 可靠性证明。
自动化程序验证器通常借助 Boogie、Why3 等中间验证语言（IVL）实现：前端把输入程序与规约翻译为 IVL 程序，后端生成证明义务并交由 SMT 求解器求解。此类验证器的可靠性要求前端翻译忠实保持输入程序与规约的语义，且后端仅在 IVL 程序确实正确时才报告成功，并且这些条件必须由其真实实现满足，而非仅由所用程序逻辑满足。本文提出一种新的验证方法论：给定输入语言与 IVL 的形式语义，即可为前端实现提供形式化的可靠性保证。验证器每次运行时，方法会自动生成一个 Isabelle 证明，表明所生成 IVL 程序的正确性蕴含输入程序的正确性；该证明可独立于验证器在 Isabelle 中检查，并可与已有的后端验证工作结合，得到端到端的可靠性结论。该方法基于前向模拟，并采用多种模块化策略以应对输入语言与 IVL 之间的巨大语义鸿沟以及实际优化翻译的复杂性。作者针对广泛使用的 Viper 与 Boogie 语言给出方法，评估表明其能有效验证现有 Viper 实现所执行的翻译。
Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its actual implementation , not just the program logic it uses. In this paper, we present a novel validation methodology that, given a formal semantics for the input language and IVL, provides formal soundness guarantees for front-end implementations. For each run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier, in Isabelle, and can be combined with existing work on validating back-ends to obtain an end-to-end soundness result. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation shows that it is effective in validating the translations performed by the existing Viper implementation.
@article{paperbot2512,
title = {Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language},
author = {Gaurav Parthasarathy and Thibault Dardinier and Benjamin Bonneau and Peter Müller and Alexander J. Summers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656438}
}