This program is tentative and subject to change.

Fri 19 Jun 2026 14:00 - 14:20 at Flatirons 3 - Probabilistic Inference and Verification

We propose new supermartingale-based certificates for verifying almost sure satisfaction of $\omega$-regular properties: (1) \emph{generalised Streett supermartingales} (GSSMs) and their lexicographic extension (LexGSSMs), (2) \emph{distribution-valued Streett supermartingales} (DVSSMs), and (3) \emph{progress-measure supermartingales} (PMSMs) and their lexicographic extension (LexPMSMs). GSSMs, LexGSSMs, and DVSSMs are derived from least-fixed point characterisations of positive recurrence and null recurrence of Markov chains with respect to given Streett conditions; and PMSMs and LexPMSMs are probabilistic extensions of parity progress measures. We study the hierarchy among these certificates and existing certificates, namely Streett supermartingales, by comparing the classes of problems that can be verified by each type of certificates. Notably, we show that our certificates are strictly more powerful than Streett supermartingales. We also prove completeness of GSSMs for positive recurrence and of DVSSMs for null recurrence: DVSSMs are, in theory, the most powerful certificates in the sense that for any Markov chain that almost surely satisfies a given $\omega$-regular property, there exists a DVSSM certifying it. We provide a sound and relatively complete algorithm for synthesising LexPMSMs, the second most powerful certificates in the hierarchy. We have implemented a prototype tool based on this algorithm, and our experiments show that our tool can successfully synthesise certificates for various examples including those that cannot be certified by existing supermartingales.

This program is tentative and subject to change.

Fri 19 Jun

Displayed time zone: Mountain Time (US & Canada) change

13:40 - 15:20
Probabilistic Inference and VerificationPLDI Research Papers at Flatirons 3
13:40
20m
Talk
[SIGPLAN] Probabilistic Inference for Datalog with Correlated Inputs
PLDI Research Papers
Jingbo Wang Purdue University, Shashin Halalingaiah UT Austin, IIT Madras, Weiyi Chen Purdue University, Chao Wang University of Southern California, Işıl Dillig University of Texas at Austin
14:00
20m
Talk
A Hierarchy of Supermartingales for ω-Regular Verification
PLDI Research Papers
Satoshi Kura Waseda University, Hiroshi Unno Tohoku University
DOI
14:20
20m
Talk
Incremental Density Calculation for Efficient Programmable Inference in Probabilistic Programs
PLDI Research Papers
Fabian Zaiser Massachusetts Institute of Technology, Jack Czenszak Yale University, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Alexander K. Lew Yale University
DOI
14:40
20m
Talk
GradInf: Gradient Estimation as Probabilistic Inference
PLDI Research Papers
Gaurav Arya Carnegie Mellon University, Mathieu Huot Massachusetts Institute of Technology, Moritz Schauer Chalmers University of Technology - University of Gothenburg, Alexander K. Lew Yale University, Feras A. Saad Carnegie Mellon University
DOI
15:00
20m
Talk
Categorical Semantics of Probabilistic Symbolic Execution
PLDI Research Papers
John Li Northeastern University, Jack Czenszak Yale University, Steven Holtzen Northeastern University
DOI