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

• Program synthesis
• Component-based synthesis (CoS)

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.

Format:

.sketch file (own format)

Expected output

Program meeting the specification/sketch of the desired program.

Internals

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.