©ERC
WHAT IS SyReP ABOUT?
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. However, the algorithmic advances behind this success do not extend to complex, cyber-physical, increasingly autonomous systems. The main obstacle for classical synthesis methods is that such systems use data domains beyond Boolean variables.
In the SyReP project, we will develop methods for reactive program synthesis, i.e., reactive synthesis in the presence of richer data domains. The resulting techniques and tools will be able to automatically construct reactive software that achieves complex temporal tasks while processing rich user inputs and interacting with the physical world. Such reactive programs are ubiquitous in the domains of software-controlled medical devices, mobile applications, and manufacturing, to name a few. Their synthesis, however, is beyond the reach of state-of-the-art techniques. This is due to a fundamental limitation of current methods, which eagerly decouple the control and data aspects of the synthesis problem. The SyReP project will radically depart from this approach by profoundly changing how reactive synthesis interacts with logical reasoning about data. Building on a recent milestone result by the PI, we will develop symbolic reactive synthesis methods that reason natively about data. Our synthesis techniques will impact many application domains, such as software for medical devices, mobile applications, and industrial control.
©ERC
WHAT IS SyReP ABOUT?
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. However, the algorithmic advances behind this success do not extend to complex, cyber-physical, increasingly autonomous systems. The main obstacle for classical synthesis methods is that such systems use data domains beyond Boolean variables.
In the SyReP project, we will develop methods for reactive program synthesis, i.e., reactive synthesis in the presence of richer data domains. The resulting techniques and tools will be able to automatically construct reactive software that achieves complex temporal tasks while processing rich user inputs and interacting with the physical world. Such reactive programs are ubiquitous in the domains of software-controlled medical devices, mobile applications, and manufacturing, to name a few. Their synthesis, however, is beyond the reach of state-of-the-art techniques. This is due to a fundamental limitation of current methods, which eagerly decouple the control and data aspects of the synthesis problem. The SyReP project will radically depart from this approach by profoundly changing how reactive synthesis interacts with logical reasoning about data. Building on a recent milestone result by the PI, we will develop symbolic reactive synthesis methods that reason natively about data. Our synthesis techniques will impact many application domains, such as software for medical devices, mobile applications, and industrial control.
