PV2 Concordgiven a domain-specific language and specification, it synthesises a program that satisfies the specification

Application domain/field

Program synthesis

Type of tool

Program synthesis

Expected input

Expected output

A program that satisfies the specification


Synthesis algorithm based on reinforcement learning tightly coupled with statistical and deductive reasoning. It focuses on syntax-guided synthesis: given a domain-specific language (DSL) and a specification, they try to find a program that satisfies the specification. Uses Z3.

Related papers

Program Synthesis Using Deduction-Guided Reinforcement Learning

Last publication date

14 July 2020

Related tools

Compared to Neo and DeepCoder.

ProVerB specific

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