BoSy is 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.

In this tutorial, we explain, step by step, the transformation of a specification given in linear-time temporal logic (LTL) to a constraint system that represents the synthesis problem. We give an overview of implemented optimizations, possible enhancements and parts that can be re-used to create a new synthesis tool.