一句话：提出以带重置向量加法系统与归纳线性势函数精确摘要递归过程，保证组合性与单调性并提升精度。
本文研究整数变量上递归过程的过程摘要问题，动机是构建更具可预测性的程序分析器，并形式化地保证摘要的组合性与单调性。方法上，作者将过程的最佳抽象计算为带重置的向量加法系统（VASR），并在该 VASR 上针对过程语法路径构成的上下文无关语言精确摘要其执行；进一步地，他们通过自动合成的线性势函数来约束合法执行中的递归调用次数，从而精化语法路径语言。作者将该摘要技术实现于一个自动程序验证工具中，实验评估表明：相比现有抽象解释器，该技术能计算出更精确的摘要，且工具的验证能力与最先进的软件模型检查器相当。
This paper presents a technique for summarizing recursive procedures operating on integer variables. The motivation of our work is to create more predictable program analyzers, and in particular to formally guarantee compositionality and monotonicity of procedure summarization. To summarize a procedure, we compute its best abstraction as a vector addition system with resets (VASR) and exactly summarize the executions of this VASR over the context-free language of syntactic paths through the procedure. We improve upon this technique by refining the language of syntactic paths using (automatically synthesized) linear potential functions that bound the number of recursive calls within valid executions of the input program. We implemented our summarization technique in an automated program verification tool; our experimental evaluation demonstrates that our technique computes more precise summaries than existing abstract interpreters and that our tool’s verification capabilities are comparable with state-of-the-art software model checkers.
@article{PimpalkhareK24,
title = {Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials},
author = {Nikhil Pimpalkhare and Zachary Kincaid},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689777}
}