  We present BoSy, a reactive synthesis tool based on the bounded synthesis
approach. Bounded synthesis ensures the minimality of the synthesized
implementation by incrementally increasing a bound on the size of the solutions
it considers. For each bound, the existence of a solution is encoded as a
logical constraint solving problem that is solved by an appropriate solver.
BoSy constructs bounded synthesis encodings into SAT, QBF, DQBF, EPR, and SMT,
and interfaces to solvers of the corresponding type. When supported by the
solver, BoSy extracts solutions as circuits, which can, if desired, be verified
with standard hardware model checkers. BoSy won the LTL synthesis track at
SYNTCOMP 2016. In addition to its use as a synthesis tool, BoSy can also be
used as an experimentation and performance evaluation framework for various
types of satisfiability solvers.
