Core Concepts
Symbolic finite automata can be used to succinctly and precisely capture fine-grained temporal and data-dependent histories of interactions between functional clients and stateful libraries, enabling automated verification of representation invariants.
Abstract
The paper presents a new trace-based specification framework for expressing representation invariants of functional clients of stateful libraries that manage hidden state. It embeds this framework within a compositional and fine-grained effect-tracking refinement type system, by encoding specifications as symbolic automata and instantiating them as Hoare Automata Types (HATs) in the type system.
The key highlights are:
The authors formalize a new trace-based specification framework for expressing representation invariants of functional clients of stateful libraries that manage hidden state.
They show how this framework can be embedded within a compositional and fine-grained effect-tracking refinement type system, by encoding specifications as symbolic automata and instantiating them as HATs in the type system.
They develop a bidirectional type-checking algorithm that translates the declarative type system into efficient subtype inclusion checks amenable to SMT-based automated verification.
Using a tool (Marple) that implements these ideas, the authors present a detailed evaluation study over a diverse set of non-trivial OCaml datatype implementations that interact with stateful libraries. Marple is the first system capable of automated verification of sophisticated representation invariants for realistic OCaml programs.