  The realizability problem in requirements engineering is to determine the
existence of an implementation that meets the given formal requirements. A step
forward after realizability is proven, is to construct such an implementation
automatically, and thus solve the problem of program synthesis. In this paper,
we propose a novel approach to pro- gram synthesis guided by k-inductive proofs
of realizability of assume- guarantee contracts constructed from safety
properties. The proof of re- alizability is performed over a set of
forall-exists formulas, and synthesis is per- formed by extracting Skolem
functions witnessing the existential quan- tification. These Skolem functions
can then be combined into an imple- mentation. Our approach is implemented in
the JSyn tool which con- structs Skolem functions from a contract written in a
variant of the Lus- tre programming language and then compiles the Skolem
functions into a C language implementation. For a variety of benchmark models
that already contained hand-written implementations, we are able to identify
the usability and effectiveness of the synthesized counterparts, assuming a
component-based verification framework.
