一句话：提出中间验证语言 Coma，用显式抽象屏障分离接口与实现，并生成正确且更紧凑的验证条件。
本文提出 Coma，一种形式化定义的中间验证语言。其规格注解以断言形式与可执行代码混合，并引入“抽象屏障”构造：在子程序内把每次调用点都需验证的接口部分与在定义点只需验证一次的实现部分分开。相较于传统基于契约的规格，该设计允许对不同执行路径分别给出规格，甚至省略规格。作者定义了 Coma 的验证条件生成过程并证明其正确性：当抽象屏障位于函数边界时，生成的验证条件与经典最弱前置条件演算相似；当屏障位于函数体中间时，用户规格会与暴露代码的验证条件无缝结合。该过程还能在生成过程中因式分解选定子目标，得到更紧凑的验证条件。最后通过二阶正则表达式引擎和非结构化汇编排序算法两个非平凡示例展示其可用性。
We present Coma , a formally defined intermediate verification language. Specification annotations in Coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths. We define a verification condition procedure for Coma and prove its correctness. For programs with a specification given in a traditional way, with an abstraction barrier at the function boundary, our verification conditions are similar to those produced by a classical weakest-precondition calculus. For programs where abstraction barriers are put in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. Moreover, our procedure can factorize selected subgoals on the fly, which leads to more compact verification conditions. We illustrate the use of Coma on two non-trivial examples, formalized and verified using our implementation: a second-order regular expression engine and a sorting algorithm written in unstructured assembly code.
@article{PaskevichPF25,
title = {<scp>Coma</scp>
, an Intermediate Verification Language with Explicit Abstraction Barriers},
author = {Andrei Paskevich and Paul Patault and Jean-Christophe Filliâtre},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {3},
year = {2026},
doi = {10.1145/3816735}
}