Reactive Synthesis of Graphical User Interface Glue Code

We present an approach to synthesize glue code for graphical user interfaces. Such code starts computation and I/O threads in response to user interface events and changes the state of the interface according to the interaction scheme envisioned by the UI designer. Our approach integrates several ideas that work best in combination. For instance, by translating all specification parts to universal very-weak (UVW) automata and building a game from them, we obtain a natural order over the positions in the game that enables us to prune the game graph substantially while constructing it. Furthermore, we present an approach to compute kind strategies that constrain the environment as little as possible and hence make the UIs as responsive as possible. The use of UVWs gives rise to a simple formalization of this idea. We apply our approach to a case study with an Android (cell phone) application and show experimentally that previous reactive synthesis tools are unable to synthesize controllers for this application.