Synthesis of Reactive Programs

Objective

The automatic synthesis of correct-by-design systems is considered the holy grail of software development. It promises to revolutionize the traditional process by allowing designers to focus on what the system should do and not on how to develop an implementation with the desired behavior. Reactive synthesis – the automatic construction of systems that maintain an ongoing interaction with their environment – is successfully used in hardware design, as exemplified by case studies like the synthesis of the AMBA AHB bus controller. However, the algorithmic advances behind this success do not extend to the complex, cyber-physical, increasingly autonomous systems ubiquitous today. The main obstacle for classical synthesis methods is that such systems use data domains beyond Boolean variables. Naturally, unbounded data types render the synthesis problem undecidable. Nevertheless, the importance of reactive program synthesis, i.e., reactive synthesis in the presence of richer data domains, has sparked a strong interest in developing techniques for this setting. Current approaches, however, suffer from one or both of two significant limitations: they are either restricted in the type of correctness specifications they can handle or diverge when reasoning about unbounded data is required. We aim to address these limitations and profoundly push the boundaries of reactive program synthesis. We will do this via a fundamental shift in how reactive synthesis interacts with logical reasoning about data. Building on recent milestone results by the PI, we will develop symbolic reactive synthesis methods that reason natively about data. We will develop and employ novel constraint-solving and functional synthesis methods optimized towards integration in reactive synthesis. Our synthesis techniques will impact many application domains, such as software for medical devices, mobile applications, and industrial control.