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

Format:

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.

Internals

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