PV3 PRODIGY: PRObability DIstributions via GeneratingfunctionologYchecks whether a probabilistic program is equivalent to a given loop-free specification

Application domain/field

Probabilistic programs

Expected input

Probabilistic (non-negative) integer program


ReDiP probabilistic programming language

Expected output

PRODIGY will decide whether a given probabilistic loop is equivalent to an (invariant) specification encoded as a loop-free ReDiP program.


The tool Probably (https://github.com/Philipp15b/Probably) (forms the basis of their implementation.)
Probabilistic programs


- Repository: https://github.com/LKlinke/Prodigy

Related papers

Does a Program Yield the Right Distribution? (CAV 2022)

Last publication date

7 August 2022

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.