一句话：提出将分离逻辑综合推导系统化翻译为Coq验证器中目标证明的方法，实现对SuSLik生成堆程序的可认证验证。
自动演绎程序合成能从简洁规约生成可执行程序及正确性证明，但合成证明与验证证明的结构差异很大，导致难以直接用经过认证的验证器检查合成结果，通常需要为每个验证后端编写临时翻译。本文面向堆操作程序的合成与验证，提出一种有原则的翻译技术，将演绎合成推导（源证明）转换为交互式程序验证器逻辑中关于所合成程序的目标证明。作者基于分离逻辑指针程序合成工具SuSLik，在Coq中的三个基础验证框架HTT、Iris和VST上实现了三个认证器。结果表明，该方法能为典型合成基准生成简洁、高效且可机器检查的证明。
Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using existing proof-certification frameworks reveals significant discrepancies in how proof derivations are structured for two different purposes: program synthesis and program verification. These discrepancies make it difficult to use certified verifiers to validate synthesis results, forcing one to write an ad-hoc translation procedure from synthesis proofs to correctness proofs for each verification backend. In this work, we address this challenge in the context of the synthesis and verification of heap-manipulating programs. We present a technique for principled translation of deductive synthesis derivations (a.k.a. source proofs) into deductive target proofs about the synthesised programs in the logics of interactive program verifiers. We showcase our technique by implementing three different certifiers for programs generated via SuSLik, a Separation Logic-based tool for automated synthesis of programs with pointers, in foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST), producing concise and efficient machine-checkable proofs for characteristic synthesis benchmarks.
@article{paperbot1126,
title = {Certifying the synthesis of heap-manipulating programs},
author = {Yasunari Watanabe and Kiran Gopinathan and George Pîrlea and Nadia Polikarpova and Ilya Sergey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473589}
}