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}
}