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

Format:

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.

Internals

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

Comments

License: GPL v3.0
Synthesis

Links

Last commit date

3 June 2021

Related papers

https://doi.org/10.1007/978-3-030-81685-8_40 (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.