Program
Verification
Book

PV2 ⊧ DIGITS: DIstribution-Guided InducTive Synthesisrepairs a given loop-free program from a probabilistic specification of its desired behaviour

An algorithm & tool for automatically repairing loop-free programs under uncertain inputs and probabilistic postconditions.

Application domain/field

Probabilistic specifications
Program synthesis
Probabilistic synthesis

Type of tool

Program repair/synthesis tool

Internals

Uses Z3.

Comments

License: MIT

Probabilistic Program repair

Links

Paper doesn't seem to link to the implementation. Link found on first author's webpage: https://github.com/sedrews/digits
Last commit date: 14 Oct 2019 (default branch)
Last commit date: 14 Oct 2019 (last activity)

Related papers

Efficient Synthesis with Probabilistic Constraints (CAV '19)
Repairing Decision-Making Programs Under Uncertainty (CAV '17)

Last publication date

12 July 2019

Related tools

τ-DIGITS: improved version of DIGITS.

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

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