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

时间：2024-12-02 分类：学术活动

Title:	A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata
Speaker:	周喆（Ph.D. candidate in Computer Science at Purdue University）
Time:	2024年12月3日 (周二) 15:00
Venue:	中国科学院软件园区5号楼三层 334报告厅
Abstract:	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.
Bio:	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.