  In previous work, we have introduced a contract-based real- izability
checking algorithm for assume-guarantee contracts involving infinite theories,
such as linear integer/real arith- metic and uninterpreted functions over
infinite domains. This algorithm can determine whether or not it is possible to
con- struct a realization (i.e. an implementation) of an assume- guarantee
contract. The algorithm is similar to k-induction model checking, but involves
the use of quantifiers to deter- mine implementability. While our work on
realizability is inherently useful for vir- tual integration in determining
whether it is possible for sup- pliers to build software that meets a contract,
it also provides the foundations to solving the more challenging problem of
component synthesis. In this paper, we provide an initial synthesis algorithm
for assume-guarantee contracts involv- ing infinite theories. To do so, we take
advantage of our realizability checking procedure and a skolemization solver
for forall-exists formulas, called AE-VAL. We show that it is possible to
immediately adapt our existing algorithm towards syn- thesis by using this
solver, using a demonstration example. We then discuss challenges towards
creating a more robust synthesis algorithm.
