PV2 SYNUDICsynthesises a loop-free program based on a sketch of the desired program

Tool for synthesis of small loop-free programs

Application domain/field

Type of tool

Synthesis tool

Expected input

Sketch of the desired program. This consists of a description of the library and a template of a straight-line program. A library describes all the available components that can be used in the program.


.sketch file (own format)

Expected output

Program meeting the specification/sketch of the desired program.


Uses Yices or Z3. SYNUDIC converts the input file into a (EF-)Yices formula or an exists SMT formula. It then calls an SMT solver.


Repository: https://github.com/adriagascon/synudic

Related papers

Last publication date

13 July 2017

ProVerB specific

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