Learning Programming Abstractions for Automating Formal Verification

In this seminar from the Alberta Machine Intelligence Institute and the Department of Computing Science, Jocelyn Qiaochu Chen, Assistant Professor at the University of Alberta and Amii Fellow, explains that effective formal-verification automation requires learning and using project-specific abstractions. She presents techniques for mining reusable custom tactics from existing proofs and VeriSoftBench, a benchmark showing that current models still struggle to exploit abstractions in real-world verification projects.

BIO: Jocelyn Qiaochu Chen is an Assistant Professor at the University of Alberta, an Amii Fellow, and a CIFAR AI Chair. Her research lies at the intersection of programming languages, formal methods, and artificial intelligence, with a current focus on AI-assisted programming. She studies how advances in machine learning and large language models can enable new programming abstractions, and how program synthesis and formal reasoning can make these abstractions reliable, scalable, and practical. Her research has appeared at venues including PLDI, OOPSLA, NeurIPS, and ACL. She is a recipient of the EECS Rising Stars award and received her PhD from the University of Texas at Austin.