General Topics on August 14, 2026

Presenter: Bohan Ma Author: Nils Froleyks et al. (CAV 2025); Krishnendu Chatterjee et al. (TACAS 2025) Abstract: Discuss the motivation and feasibility of extending the certification approach of CAV'25 to probabilistic model checking.

Presenter: Soroush Farokhnia Author: Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan (Columbia University) Venue: 15th USENIX Symposium on Operating Systems Design and Implementation (Best Paper Award)

Presenter: Yazhou Tang Author: Shenghao Yuan, Yazhou Tang, Tianci Cao (Zhejiang University); Frédéric Besson, Jean-Pierre Talpin (INRIA); Mingshuai Chen (Zhejiang University) Abstract: This paper presents a mechanized formal semantics for the Linux eBPF instruction set architecture (ISA).

Presenter: Yutao Sun Author: Valentin Gabeur, Shangbang Long, Songyou Peng, Paul Voigtlaender, Shuyang Sun, Yanan Bao, Karen Truong, Zhicheng Wang, Wenlei Zhou, Jonathan T. Barron, Kyle Genova, Nithish Kannen, Sherry Ben, Yandong Li, Mandy Guo, Suhas Yogin, Yiming Gu, Huizhong Chen, Oliver Wang, Saining Xie, Howard Zhou, Kaiming He, Thomas Funkhouser, Jean-Baptiste Alayrac, Radu Soricut

Presenter: Xiaqing Zhou Author: Prasita Mukherjee, Minghai Lu, Benjamin Delaware Abstract: We present SYNVER — a novel, general purpose synthesizer for C programs equipped with machine-checked proofs of correctness using the Verified Software Toolchain.

Presenter: Xiaoning Zhang Author: Zenan Li (Apodex); Ziran Yang (Princeton University); Peiyang Song (Caltech); Zhaoyu Li (University of Toronto); Kaiyu Yang (Apodex) Abstract: Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction.

Presenter: Tengjie Lin Author: Tengjie Lin, Zhongyi Wang (ZJU); Haokun Li (PKU); Jianwei Yin, Mingshuai Chen (ZJU) Abstract: Deductive verification scales to large software systems through modular reasoning, where formal contracts summarize the behavior of individual functions and enable their independent verification.