一句话：提出基于自动机的抽象效应域与类型-效应系统，可扩展地验证高阶递归程序的时序安全性质。
针对递归高阶程序的时序安全性质验证，既有工作虽有理论与部分自动化，但可扩展性有限。本文提出基于自动机的抽象效应域，概括上下文敏感的依赖效应，能抽象程序环境与自动机控制状态的关系；并给出新的变换器，把事件前缀抽象为自动计算的上下文敏感效应摘要，实例化为基于抽象解释的类型-效应系统。分析对自动机参数化，因而可实例化到 history/register（累加器）自动机，表达上下文无关性质、输入依赖、事件求和、资源使用与代价等。原型 ev Drift 处理类 OCaml 高阶递归程序。在 23 个基准上，ev Drift 验证 21 个，优于 Drift(12)、RCaml/Spacer(6)、MoCHi(11)、ReTHFL(18)，共同可解基准上分别取得 6.3×、5.3×、16.8×、6.4× 加速。
This paper describes a new abstract interpretation -based approach to verify temporal safety properties of recursive, higher-order programs. While prior works have provided theoretical impact and some automation, they have had limited scalability. We begin with a new automata-based “abstract effect domain” for summarizing context-sensitive dependent effects, capable of abstracting relations between the program environment and the automaton control state. Our analysis includes a new transformer for abstracting event prefixes to automatically computed context-sensitive effect summaries, and is instantiated in a type-and-effect system grounded in abstract interpretation. Since the analysis is parametric on the automaton, we next instantiate it to a broader class of history/register (or “accumulator”) automata, beyond finite state automata to express some context-free properties, input-dependency, event summation, resource usage, cost, equal event magnitude, etc. We implemented a prototype ev Drift that computes dependent effect summaries (and validates assertions) for OCaml-like recursive higher-order programs. As a basis of comparison, we describe reductions to assertion checking for higher-order but effect-free programs, and demonstrate that our approach outperforms prior tools Drift , RCaml / Spacer , MoCHi , and ReTHFL . Overall, across a set of 23 benchmarks, Drift verified 12 benchmarks, RCaml/Spacer verified 6, MoCHi verified 11, ReTHFL verified 18, and ev Drift verified 21; ev Drift also achieved a 6.3×, 5.3×, 16.8×, and 6.4× speedup over Drift , RCami/Spacer , MoCHi , and ReTHFL , respectively, on those benchmarks that both tools could solve.
@article{paperbot2879,
title = {Abstract Interpretation of Temporal Safety Effects of Higher Order Programs},
author = {Mihai Nicola and Chaitanya Agarwal and Eric Koskinen and Thomas Wies},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763140}
}