Paper at CAV 2022

The paper entitled “Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions” by Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler has been accepted at CAV 2022 (Computer-Aided Verification). Out of 209 submissions, 40 regular papers have been accepted at CAV 2022. The paper leverages probability generating functions to prove that a loopy probabilistic program is equivalent to a straight-line program. It is shown that for a so-called ReDIP program, proving program equivalence is decidable. The approach is implemented in the tool Prodigy.