Abstract Interpretation of Temporal Safety Effects of Higher Order Programs

Explore a 15-minute conference presentation introducing a novel abstract interpretation-based approach for verifying temporal safety properties in recursive, higher-order programs. Learn about the development of an automata-based 'abstract effect domain' that summarizes context-sensitive dependent effects and can abstract relations between program environments and automaton control states. Discover how this analysis incorporates a new transformer for abstracting event prefixes to automatically computed context-sensitive effect summaries, implemented within a type-and-effect system grounded in abstract interpretation. Examine the extension of this parametric analysis to history/register automata, enabling verification of context-free properties, input-dependency, event summation, resource usage, and cost analysis beyond traditional finite state automata. Review the implementation of the evDrift prototype that computes dependent effect summaries and validates assertions for OCaml-like recursive higher-order programs. Analyze comparative performance results showing evDrift's superior verification capabilities and speed improvements over existing tools including Drift, RCaml/Spacer, MoCHi, and ReTHFL across 23 benchmarks, with evDrift successfully verifying 21 benchmarks compared to competitors' lower success rates while achieving significant speedup improvements ranging from 5.3x to 16.8x.