  Automated synthesis of reactive systems from specifications has been a topic
of research for decades. Recently, a variety of approaches have been proposed
to extend synthesis of reactive systems from proposi- tional specifications
towards specifications over rich theories. We propose a novel, completely
automated approach to program synthesis which reduces the problem to deciding
the validity of a set of forall-exists formulas. In spirit of IC3 / PDR, our
problem space is recursively refined by blocking out regions of unsafe states,
aiming to discover a fixpoint that describes safe reactions. If such a fixpoint
is found, we construct a witness that is directly translated into an
implementation. We implemented the algorithm on top of the JKind model checker,
and exercised it against contracts written using the Lustre specification
language. Experimental results show how the new algorithm outperforms JKinds
already existing synthesis procedure based on k-induction and addresses
soundness issues in the k-inductive approach with respect to unrealizable
results.
