ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 11:00 - 12:00 at SW2 (SYNT Camp) - Hands-on BoSy Tutorial Chair(s): Guillermo A. Perez, Leander Tentrup

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

11:00 - 12:00: SYNT Camp - Hands-on BoSy Tutorial at SW2 (SYNT Camp)
Chair(s): Guillermo A. PerezUniversity of Antwerp, Leander TentrupSaarland University
syntcompcamp-2019-tutorial11:00 - 12:00
Leander TentrupSaarland University