一句话：提出 coherent 程序类，使未解释程序的完全自动验证可判定，并可在 Pspace 内完成。
本文研究未解释程序的完全自动验证：程序可运行在任意数据模型上，数据模型为常元、函数和关系提供解释，验证目标是无量词、带等式的最终状态后置条件，且不提供循环不变式或契约。作者首先证明该问题一般不可判定。核心贡献是定义一类 coherent 程序，使验证可判定，并可在 Pspace 内判定；进而通过自动添加 k 个 ghost 变量和赋值，将可判定性扩展到 k-coherent 程序。论文还将可判定性结果扩展到含递归函数调用的程序，并给出若干不可判定性结果，说明所加限制的必要性。
We study the problem of completely automatically verifying uninterpreted programs—programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification problem asks whether a given program satisfies a postcondition written using quantifier-free formulas with equality on the final state, with no loop invariants, contracts, etc. being provided. We show that this problem is undecidable in general. The main contribution of this paper is a subclass of programs, called coherent programs that admits decidable verification, and can be decided in Pspace. We then extend this class of programs to classes of programs that are k -coherent, where k ∈ ℕ, obtained by (automatically) adding k ghost variables and assignments that make them coherent. We also extend the decidability result to programs with recursive function calls and prove several undecidability results that show why our restrictions to obtain decidability seem necessary.
@article{paperbot621,
title = {Decidable verification of uninterpreted programs},
author = {Umang Mathur and P. Madhusudan and Mahesh Viswanathan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290359}
}