12月19日:周喆
发布时间:2024-12-17 浏览量:10

报告名称:A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata

报告时间:2024年12月19日13:30-14:30

报告地点:理科大楼B1002

腾讯会议号:335 9049 1248


报告摘要:

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.


以诚为本赢在信誉9001cc
学院地址:上海中山北路3663号理科大楼

                上海市浦东新区楠木路111号
院长信箱:yuanzhang@sei.ecnu.edu.cn | 办公邮箱:office@sei.ecnu.edu.cn | 院办电话:021-62232550
Copyright 以诚为本赢在信誉9001cc(中国)有限公司