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

Application domain/field

Type of tool

Synthesis tool

Expected input

Program sketch consisting of:


Expected output

Instantiations for the holes in the program.


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.


License: MIT


Repository: https://github.com/sedrews/digits

Related papers

Efficient Synthesis with Probabilistic Constraints (CAV '19)

Last publication date

12 July 2019

ProVerB specific

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