PV2 QuaSitries to solve a SyGuS problem with quantitative objectives

Application domain/field

Type of tool

Synthesis tool

Expected input

QSyGuS problem (SyGuS problem with quantitative objectives)


Extension of the SyGuS format

Expected output

It times out or presents the solution to the QSyGuS problem. A solution to the QSyGuS problem is a term, in the language of the provided grammar, such that the Boolean formula constraining the semantic behavior is satisfied, and such that the constraints over the weight w of the synthesized program is true.


Quasi is a tool for specifying and solving QSyGuS problems. QSyGuS: "syntax-guided synthesis problems with quantitative objectives over the syntax of the synthesized program, e.g. find the most likely program with respect to a given probability distribution" Uses CVC4, ESolver, EUSolver


Repository: Cannot find one in the paper or on the first author's website.

Related papers

Syntax-Guided Synthesis with Quantitative Syntactic Objectives

Last publication date

18 July 2018

ProVerB specific

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