Abstract Interpretation of Temporal Safety Effects of Higher Order Programs

In recent years temporal verification has been increasingly applied to higher-order programs. Some researchers have developed automated approaches via higher-order recursion schemes, reductions to fair-termination or constrained Horn clauses, while others have extended type and effect systems to reason about liveness properties. Despite these works, today's automated tools are often limited to somewhat small examples.

In this talk I will discuss our recent work on a new abstract interpretation-based approach to verify temporal safety properties of recursive, higher-order programs. 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 evDrift 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 evDrift verified 21; evDrift also achieved a 6.3x, 5.3x, 16.8x, and 6.4x speedup over Drift, RCaml/Spacer, MoCHi, and ReTHFL, respectively, on those benchmarks that both tools could solve.

This work appeared in OOPSLA 2025 and is joint with Mihai Nicola, Chaitanya Agarwal, and Thomas Wies.

Bio

-------

Eric Koskinen is the Charles Berendsen Associate Professor of Computer Science at Stevens Institute of Technology. Previously, he was a Researcher at Yale University and a Visiting Professor at New York University. He received a Ph.D in Computer Science from the University of Cambridge (UK) and has spent time at IBM Watson, Microsoft, and from 2002-2005, was a Software Engineer at Amazon.com. Prof Koskinen's work is funded by over $6M from NSF/ONR/DARPA and yields techniques that improve the way programmers develop reliable and efficient concurrent software for multi-core and distributed systems.