Probabilistic and Quantum Programming: Verification, Synthesis, and Beyond on September 18–19, 2026

Presenter: Mingqi Yang Author: Mingqi Yang, Bohan Ma, Mingshuai Chen Abstract: Exact inference for probabilistic loops is challenging in the presence of unbounded executions and infinite state spaces. Recent occupation-measure-based approaches synthesize rational closed-form candidates, but their certification relies on establishing coefficientwise nonnegativity.

Presenter: Bohan Ma Author: Darion Haase et al.; Mingshuai Chen et al. Abstract: We try to turn the higher-order fixed-point problem of synthesizing a probabilistic loop transformer into a first-order symbolic fixed-point problem over second-order generating functions.

Presenter: Tengjie Lin Abstract: Fully automated verification of large-scale software and hardware systems has long been considered a “Holy Grail” of formal methods. Although modular contract-based reasoning enables deductive verification to scale to large systems, constructing formal specifications remains a fundamental bottleneck: it still relies heavily on human experts and accounts for much of the cost of industrial verification.

Presenter: Yiyang Zhou Abstract: Quantum computing exhibits the potential to revolutionize various fields in classical computing by offering significant speed-ups. However, current quantum devices are intermediate-scale and suffer from multiple sources of noise, rendering them incapable of solving complex quantum tasks with high fidelity.