PV2 PLearnsynthesises a program conforming to a subgrammar of a given grammar

Black-box framework that runs multiple parallel instances of a SyGuS (syntax-guided synthesis) tool with different grammars

Application domain/field

Type of tool

? Synthesis tool? Metatool?

Expected input

Expected output

First solution that was found or if no solution could be found.


The idea behind the tool is that SyGuS tools are sensitive to the choice of grammar. Sometimes increasing the grammar expressiveness allows the tool to solve some problems that are unsolvable with less expressive grammars. However, it is possible that the tool can no longer solve some problems that could be solved with less expressive grammars.


Related papers

Overfitting in Synthesis: Theory and Practice (CAV '19)

Last publication date

12 July 2019

ProVerB specific

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