一句话：为语言无关演绎验证器生成可独立检验的证明证书，以认证每次成功验证的正确性。
针对语言无关的演绎程序验证器潜在的实现缺陷，本文提出一种通过生成证明证书来认证每次成功验证运行正确性的方法。验证器接收程序、形式规约和编程语言形式语义，并用语言无关算法证明程序相对规约正确；该方法在验证成功时产出证明证书，使小型证明检查器能够独立复核结果。基于重写与可达性逻辑的框架，该证书机制不依赖特定语言。初步实验在命令式语言、函数式语言和汇编语言上生成证明证书，验证了方法的语言无关性。
Previous work on rewriting and reachability logic establishes a vision for a language-agnostic program verifier, which takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program is written. The verifier then uses a language-agnostic verification algorithm to prove the program correct with respect to the specification and the formal language semantics. Such a complex verifier can easily have bugs. This paper proposes a method to certify the correctness of each successful verification run by generating a proof certificate. The proof certificate can be checked by a small proof checker. The preliminary experiments apply the method to generate proof certificates for program verification in an imperative language, a functional language, and an assembly language, showing that the proposed method is language-agnostic.
@article{paperbot2043,
title = {Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier},
author = {Zhengyao Lin and Xiaohong Chen and Minh-Thai Trinh and John Wang and Grigore Roşu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586029}
}