ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

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.

Sun 7 Apr (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30: SYNT Camp - Reactive Synthesis Background & SYNTCOMP at SW2 (SYNT Camp)
Chair(s): Guillermo A. PerezUniversity of Antwerp, Leander TentrupSaarland University
syntcompcamp-2019-tutorial09:00 - 10:00
Guillermo A. PerezUniversity of Antwerp
syntcompcamp-2019-tutorial10:00 - 10:30
Leander TentrupSaarland University
Link to publication DOI Pre-print