The classical setting of
program synthesis has been to synthesize programs from proofs of logical
specifications that relate the inputs and the outputs, in short inputs-outputs,
of the program [1]}.
Thanks to recent successful trends in formal verification based on automated
reasoning [2]}, [3]}, [4]}, this traditional view of program synthesis
has been refined to the setting of syntax-guided synthesis
(SyGuS) [5]}. In addition to logical
specifications, SyGuS approaches consider further constraints on the program
templates to be synthesized, thus limiting the search space of possible
solutions.
A wide range of efficient
applications of SyGuS have so far emerged, for example programming by
examples [6]}, component-based synthesis [7]}
with learning [8]} and sketching [9]}.
