PV2 ⊧ 𝜏-DIGITSfill holes a given loop-free program from a probabilistic specification of its desired behaviour

Application domain/field

• Program synthesis
• Probabilistic synthesis
• Distribution-guided inductive synthesis (DIGITS)
• Sketch-based synthesis

Type of tool

Synthesis tool

Expected input

Program sketch consisting of:

• a program written in a loop-free language with "holes". These "holes" represent some constant terminals in expressions.
• Precondition?
• Postcondition: Boolean probabilistic correctness property

Format:

• Program sketch: .fr file where the program is defined in a method D(args). Holes can be indicated with Hole(...)
• Postcondition: in a method post(Pr) in the same .fr file
• Precondition: in a method pre() in the same .fr file

Expected output

Instantiations for the holes in the program.

Internals

The algorithm roughly follows the following steps to reduce the problem of probabilistic synthesis to non-probabilistic synthesis:

1. Approximate the input probability distribution with a finite sample set
2. Synthesize a program for various possible output assignments of the finite sample set
3. Invoke a probabilistic verifier to check if one of the synthesized programs adheres to the given specification.

As a back-end, you can use Z3 and CVC4. 𝜏-DIGITS is an improved version of DIGITS. It reduces the number of synthesis queries performed by the algorithm.

Comments

License: MIT