A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
summary
Describes a toolchain that uses symbolic finite automata to encode data-dependent, temporal representation invariants and integrates them into a refinement type system called Hoare Automata Types to automatically verify ADT implementations that call opaque stateful libraries. Implements a bidirectional type checker with an SMT-backed subtyping/inclusion algorithm and reports verifying full ADT APIs in 2 seconds to under 3 minutes per benchmark; artifact and OCaml implementation are available. SMT-based verification
AI-written summary · about
chapters (14)
- 0:00HAT verification framework
- 1:08Mean set ADT example
- 4:20Mean set property via traces
- 6:51Core language with effects
- 7:11Symbolic LTLF for temporal props
- 8:34Symbolic LTLF with data deps
- 9:58Add function behavior
- 11:02HAT type system
- 12:30Subtyping and atom inclusion
- 12:52Verifying representation invariants
- 13:33Performance benchmarks
- 14:19Summary and artifact
- 14:39Q&A part one
- 15:22Q&A part two
related talks
14mVerify, but test: extracting property-based tests from F* specifications
20mAutomatic Invariant Testing for Finite-State Machines
20mDerivative-Guided Symbolic Execution
51mWhen Types are Not Enough
01h 05mVerifying Infinitely Many Programs at Once
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs