probabilistic programs

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions

We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring …

Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions

Latticed Craig Interpolation with an Application to Probabilistic Verification

In this work, we are primarily concerned with the question: Is Craig interpolation applicable to the automatic, quantitative …

Mingqi Yang, Kevin Batz, Mingshuai Chen, Joost-Pieter Katoen, Zhiang Wu, Jianwei Yin

Latticed Craig Interpolation with an Application to Probabilistic Verification

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite …

Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Lower Bounds for Possibly Divergent Probabilistic Programs

We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to …

Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan

Exact Probabilistic Inference Using Generating Functions

Probabilistic programs are typically normal-looking programs describing posterior probability distributions. They intrinsically code up …

Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen

Does a Program Yield the Right Distribution?

We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the …

Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler

Latticed $k$-Induction with an Application to Probabilistic Programs

We revisit two well-established verification techniques, $k$-induction and bounded model checking (BMC), in the more general setting of …

Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer

Latticed $k$-Induction with an Application to Probabilistic Programs

Latticed $k$-Induction and Probabilistic Programs

“Induction is a process of inference; it proceeds from the known to the unknown.”

– John S. Mill, 1806 – 1873

Mingshuai Chen

Apr 18, 2021

Latticed $k$-Induction and Probabilistic Programs