General Topics on January 9, 2026

Presenter: Zhongyi Wang Author: Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, Markus Püschel, and Ilya Sergey Abstract: Automated program verifiers such as Dafny, F , Verus, and Viper are now routinely used to verify real-world software.

Presenter: Xiaqing Zhou Author: Xiangdong Chen, Zhaofeng Li, Jerry Zhang (University of Utah); Vikram Narayanan (Palo Alto Networks); Anton Burtsev (University of Utah) Abstract: Recent advances in programming languages and automated formal reasoning have changed the balance between the complexity and practicality of developing formally verified systems.

Presenter: Huangying Dong Author: Chen Yang, Lin Yang, Ziqi Wang, Dong Wang, Jianyi Zhou, and Junjie Chen Abstract: Recent advances in large language models (LLMs) have enabled promising performance in unit test generation through in-context learning (ICL).

Presenter: Yazhou Tang Author: Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart Abstract: CompCert is a compiler from Clight (a large subset of the C programming language) to assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness.

Presenter: Linyu Yang Author: Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey Abstract: Multi-modal program verification is a process of validating code against its specification using both dynamic and symbolic techniques, and proving its correctness by a combination of automated and interactive machineassisted tools.

Presenter: Bohan Ma Author: Fabian Zaiser, Andrzej S. Murawski, C.-H. Luke Ong Abstract: We study the problem of bounding the posterior distribution of discrete probabilistic programs with unbounded support, loops, and conditioning.

Presenter: Mingqi Yang Author: Peixin Wang, Jianhao Bai, Min Zhang, and C.-H. Luke Ong Abstract: Probabilistic programming provides a high-level framework for specifying statistical models as executable programs with built-in randomness and conditioning.