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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Reactive Synthesis Background & SYNTCOMPSYNT Camp at SW2 (SYNT Camp)
Chair(s): Guillermo A. Perez University of Antwerp, Leander Tentrup Saarland University
09:00
60m
Tutorial
Reactive Synthesis Background and the Synthesis Competition
SYNT Camp
Guillermo A. Perez University of Antwerp
10:00
30m
Tutorial
Hand-on Synthesis Experience with BoSy
SYNT Camp
Leander Tentrup Saarland University
Link to publication DOI Pre-print