一句话：提出核心 IVL 形式化框架，统一翻译式分离逻辑验证器的前端翻译与后端验证，并在 Isabelle/HOL 中机化。
翻译式验证器常把程序转为 Boogie、Viper 等中间验证语言再交后端验证，其可靠性证明需关联输入程序、验证逻辑、IVL 语义与后端实现；对分离逻辑而言语义鸿沟尤其大。本文提出形式化框架：以通用核心 IVL 捕捉不同分离逻辑，定义操作语义，并利用 angelic 非确定性支持不同证明搜索；再给出公理语义，使前端翻译的关键证明步骤在等价性证明中一次性完成。作者将核心 IVL 实例化到 Viper 元素，连接符号执行与验证条件生成两个后端以及并发分离逻辑前端。全部技术结果均在 Isabelle/HOL 中机化，包括核心 IVL、语义、后端子集语义与证明。
Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an existing back-end verifier. A soundness proof for such a translational verifier needs to relate the input program and verification logic to the semantics of the IVL, which in turn needs to be connected with the verification logic implemented in the back-end verifiers. Performing such proofs is challenging due to the large semantic gap between the input and output programs and logics, especially for complex verification logics such as separation logic. This paper presents a formal framework for reasoning about translational separation logic verifiers. At its center is a generic core IVL that captures the essence of different separation logics. We define its operational semantics and formally connect it to two different back-end verifiers, which use symbolic execution and verification condition generation, resp. Crucially, this semantics uses angelic non-determinism to enable the application of different proof search algorithms and heuristics in the back-end verifiers. An axiomatic semantics for the core IVL simplifies reasoning about the front-end translation by performing essential proof steps once and for all in the equivalence proof with the operational semantics rather than for each concrete front-end translation. We illustrate the usefulness of our formal framework by instantiating our core IVL with elements of Viper and connecting it to two Viper back-ends as well as a front-end for concurrent separation logic. All our technical results have been formalized in Isabelle/HOL, including the core IVL and its semantics, the semantics of two back-ends for a subset of Viper, and all proofs.
@article{paperbot3220,
title = {Formal Foundations for Translational Separation Logic Verifiers},
author = {Thibault Dardinier and Michael Sammler and Gaurav Parthasarathy and Alexander J. Summers and Peter Müller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704856}
}