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 are allowed to be 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 in a call-by-value way 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.

翻译：针对C等命令式语言的程序验证器可分为两类：基于注解的验证器（将断言和不变量嵌入源文件后检查）和基于策略的验证器（在Coq等证明助手中交互式开发与程序分离的证明脚本）。注解验证器通常更自动化且便捷，但交互式验证器拥有更丰富的断言语言和严格的形式化正确性证明。我们提出VST-A，一种采用VST丰富断言语言的注解验证器，它利用VST的形式化正确性证明，同时允许用户通过插入断言直观地描述功能正确性证明。VST-A通过分析控制流图，将每个C函数分解为断言之间的控制流路径，并将程序验证问题转化为对应的线性霍尔三元组。与VST和Iris等现有基础性程序验证工具相比，VST-A允许这种分解与转化过程采用非结构化方式，从而更具使用灵活性。VST-A的分解与转化机制在Coq中定义、在Coq中完成正确性证明，并以Coq的按值调用方式执行计算。其转化正确性证明完全基于逻辑推理，独立于VST霍尔三元组复杂的语义模型（及其正确性证明）。由于采用丰富的断言语言，并非所有约简后的证明目标都能自动验证，但系统允许用户利用Coq证明助手的全部功能来证明剩余证明目标。