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.

翻译：程序验证工具通常通过将输入程序翻译为中间验证语言（IVL，如Boogie、GIL、Viper或Why3）的前端实现。生成的IVL程序随后由现有的后端验证器进行验证。此类翻译式验证器的可靠性证明需要将输入程序与验证逻辑关联至IVL的语义，并进一步与后端验证器实现的验证逻辑建立联系。由于输入输出程序与逻辑间存在巨大的语义鸿沟（特别是对于分离逻辑等复杂验证逻辑），此类证明极具挑战性。本文提出一个用于推理翻译式分离逻辑验证器的形式化框架。其核心是一个通用基础IVL，能够捕捉不同分离逻辑的本质特征。我们定义了其操作语义，并形式化地将其与两个分别采用符号执行和验证条件生成的后端验证器相连接。关键之处在于，该语义利用天使非确定性以支持后端验证器中不同证明搜索算法与启发式策略的应用。基础IVL的公理语义通过在与操作语义的等价证明中一次性完成核心证明步骤（而非为每个具体前端翻译重复执行），简化了对前端翻译过程的推理。我们通过将基础IVL实例化为Viper的要素模块，并将其连接至两个Viper后端以及一个支持并发分离逻辑的前端，展示了该形式化框架的实用性。所有技术成果（包括基础IVL及其语义、Viper子集的两个后端语义以及全部证明）均在Isabelle/HOL中完成形式化验证。