General Topics on August 14, 2026


Location: 小慢居·茶空间（大悦城运河景观店），浙江省杭州市拱墅区隐秀路大悦城悦街2幢3楼323-327号

Online Meeting: TBD

Paper Venue Title of the Presentation Presenter Time Slot
arXiv P³: Joint Program-and-Proof Planning for Verified Code Generation Xiaoning Zhang 10:00-10:40
arXiv Image Generators are Generalist Vision Learners Yutao Sun 10:40-11:20
– Certifying on Probabilistic Program? Bohan Ma 11:20-12:00
ASE 2025 LLM-Assisted Synthesis of High-Assurance C Programs Xiaqing Zhou 14:00-14:40
OSDI 2021 (Best Paper) DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols Soroush Farokhnia 14:40-15:20
– Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification Mingqi Yang 15:20-16:00
OOPSLA 2026 Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications Yazhou Tang 16:00-16:40
Certifying on Probabilistic Program?
Presenter: Bohan Ma Author: Nils Froleyks et al.; Krishnendu Chatterjee et al. Abstract: Discuss the motivation and feasibility of transferring the witness method from CAV'25 to probabilistic programs. URL: https://link.springer.com/chapter/10.1007/978-3-031-98668-0_14 https://link.
Aug 14, 2026
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
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)
Aug 14, 2026
Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications
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).
Aug 14, 2026
Image Generators are Generalist Vision Learners
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
Aug 14, 2026
LLM-Assisted Synthesis of High-Assurance C Programs
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.
Aug 14, 2026
P³: Joint Program-and-Proof Planning for Verified Code Generation
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.
Aug 14, 2026
Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
Presenter: Mingqi Yang Author: Satoshi Kura (Waseda University); Hiroshi Unno (Tohoku University); Takeshi Tsukada (Chiba University) Abstract: Verifying lower bounds for quantitative properties of probabilistic programs is notoriously difficult. We propose a unified approach based on fixed-point uniqueness.
Aug 14, 2026