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

• Program synthesis
• Probabilistic programs
• Oracle-guided synthesis

Expected input

• Program sketch, concisely describing a finite family of finite Markov chains (MCs)
• Specification, as a temporal logic constraint

Format:

• Program sketch: extension of the PRISM language or JANI language
• Specification: PRISM syntax

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