The two most
rigorous approaches for providing correct software are given by formal program
verification and program synthesis [1]}. The task of formal
verification is to prove correctness of a given program with respect to a given
logical specification [2]}, [3]}, [4]}.
On the other hand, program synthesis aims at generating programs which adhere to
a given specification [5]}, [6]}. The result of a synthesis problem is therefore a program
which is correct by construction with respect to the specification. While formal verification has received
considerable attention with impressive results, for example, in ensuring safety
of device drivers [7]} and security of web services [8]},
program synthesis turns out to be an algorithmically much more difficult
challenge [9]}.
