一句话：提出 VST-A，一个基于 VST 丰富断言语言和 Coq 可靠证明的注解验证器，可将 C 函数验证归约为直线 Hoare 三元组。
面向 C 等命令式语言的程序验证中，注解验证器更自动化，但断言语言和可靠性证明常较弱；基于策略的验证器虽有丰富断言与形式可靠性，却依赖交互式证明脚本。VST-A 结合二者：采用 VST 的丰富断言语言和形式可靠性证明，让用户以插入断言的方式描述函数正确性证明。它分析控制流图，将每个 C 函数分解为断言之间的控制流路径，并把验证问题归约为直线 Hoare 三元组。相比 VST 和 Iris，其分解与归约可以是非结构化的，因而更灵活；该过程在 Coq 中定义、证明可靠并按值调用计算。归约的可靠性证明完全逻辑化，独立于 VST Hoare 三元组的复杂语义模型。由于断言语言丰富，并非所有归约后的目标都能自动检查，剩余目标可在 Coq 中证明。
Program verifiers for imperative languages such as C may be annotation-based , in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively developed in a proof assistant such as Coq. Annotation verifiers have been more automated and convenient, but some interactive verifiers have richer assertion languages and formal proofs of soundness. We present VST-A, an annotation verifier that uses the rich assertion language of VST, leverages the formal soundness proof of VST, but allows users to describe functional correctness proofs intuitively by inserting assertions. VST-A analyzes control flow graphs, decomposes every C function into control flow paths between assertions, and reduces program verification problems into corresponding straightline Hoare triples . Compared to existing foundational program verification tools like VST and Iris, in VST-A such decompositions and reductions can nonstructural, which makes VST-A more flexible to use. VST-A’s decomposition and reduction is defined in Coq, proved sound in Coq, and computed call-by-value in Coq. The soundness proof for reduction is totally logical, independent of the complicated semantic model (and soundness proof) of VST’s Hoare triple. Because of the rich assertion language, not all reduced proof goals can be automatically checked, but the system allows users to prove residual proof goals using the full power of the Coq proof assistant.
@article{paperbot2615,
title = {VST-A: A Foundationally Sound Annotation Verifier},
author = {Litao Zhou and Jianxing Qin and Qinshi Wang and Andrew W. Appel and Qinxiang Cao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632911}
}