A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata - PLDI 2024

Explore a 17-minute conference talk from PLDI 2024 that introduces Hoare Automata Types (HATs), a novel approach to automatically verify representation invariants in functional programs interacting with stateful libraries. Learn how symbolic finite automata (SFA) can capture fine-grained temporal and data-dependent histories of these interactions. Discover the integration of SFAs into a refinement type system for modular and compositional reasoning. Understand the development of a bidirectional type checking algorithm that enables efficient subtyping inclusion checks over HATs and their translation for SMT-based automated verification. Examine experimental results demonstrating the feasibility of type-checking complex OCaml data structure implementations using HAT specifications layered on stateful library APIs.