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. On the other hand, program
synthesis aims at
generating programs which adhere to a given specification. The result of a
synthesis problem is therefore a program which is correct by construction. While
formal verification has received considerable attention with impressive results,
for example, in ensuring safety of device drivers [2]} and
security of
web services [3]}, program synthesis turns out to be an algorithmically
much more difficult challenge [4]}.
