-

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

组织者

蒋瀚如

演讲者

Zhe Zhou

时间

2024年12月05日 14:00 至 15:00

地点

A3-2a-302

线上

Zoom 518 868 7656 (BIMSA)

摘要

Functional programs typically interact with stateful libraries that hide state behind typed abstractions. However, because the specifications of the methods provided by these libraries are necessarily general and rarely specialized to the needs of any specific client, any required application-level invariants must often be expressed in terms of additional constraints on the (often) opaque state maintained by the library. This paper addresses the specification and verification of such invariants using symbolic finite automata (SFA), which succinctly capture temporal and data-dependent histories of client-library interactions. To enable modular reasoning, we integrate SFAs into a refinement type system, qualifying stateful computations. Our approach, Hoare Automata Types (HATs), facilitates the specification and automatic type-checking of datatype invariants, even when implementations rely on stateful library methods with hidden state.

演讲者介绍

Zhe Zhou is currently a Ph.D. candidate in Computer Science at Purdue University, advised by Prof. Suresh Jagannathan and working closely with Prof. Benjamin Delaware. He earned his bachelor's degree from Peking University in 2017, where he was advised by Prof. Guangyu Sun. His research interests include programming languages (PL), particularly program verification and synthesis, property-based testing, and refinement types.