PV3 ⊧ PRODIGY: PRObability DIstributions via GeneratingfunctionologYchecks whether a probabilistic program is equivalent to a given loop-free specification
Application domain/fieldProbabilistic programs
Expected inputProbabilistic (non-negative) integer program
ReDiP probabilistic programming language
Expected outputPRODIGY will decide whether a given probabilistic loop is equivalent to an (invariant) specification encoded as a loop-free ReDiP program.
InternalsThe tool Probably (
https://github.com/Philipp15b/Probably) (forms the basis of their implementation.)