一句话：提出首个支持非平凡状态编码的翻译式分离逻辑验证器可靠性形式化框架，并以 Isabelle/HOL 机器化验证。
翻译式（translational）程序验证器通常分为前端与后端：前端把输入程序编码进某种中间验证语言（IVL），后端再证明 IVL 程序正确。其整体可靠性既要后端验证可靠，也要求 IVL 程序的正确性能推出原程序的正确性。已有针对分离逻辑翻译式验证器的形式化只关注前者，而后者的现有支持依赖一个过强的假设：存在一个与原程序状态模型相同的分离逻辑，这在实践中（尤其考虑到状态模型还决定了支持的分离逻辑资源）并不现实。本文提出首个可处理非平凡状态编码的可靠性形式化框架。为适配多种前端与 IVL，框架仅假设前端与 IVL 的状态模型之间存在同态编码关系，并引入核心新条件——后向可满足性（backward satisfiability）来保证前端翻译的可靠性。作者针对基于并发分离逻辑的前端与分离逻辑 IVL（如 Raven、VeriFast、Viper）形式化该框架，通过为三种常见状态编码证明可靠性展示其表达力，全部证明在 Isabelle/HOL 中机器化。
Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2603-20001,
title = {Sound State Encodings in Translational Separation Logic Verifiers},
author = {Hongyi Ling and Thibault Dardinier and Ellen Arlt and Peter Müller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839462}
}