PV2 PAYNT: Probabilistic progrAm sYNThesizersynthesise a full program from its sketch and desired properties

Given a sketch of a program, it will synthesise (if possible) the missing parts such that a user-defined specification is satisfied.

Application domain/field

Expected input


Expected output

A satisfying realization, i.e. an assignment to the holes in the program sketch such that the program satisfies the specification. Otherwise, it will report that such a design does not exist.


PAYNT has been implemented on top of the probabilistic model checker Storm. It uses Z3.


License: GPL v3.0


Related papers

PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

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