Rayna Dimitrova

(Department of Computer Science, RPTU)
hosted by Department of Computer Science

"Synthesis of Reactive Programs Beyond Boolean Domains and Specifications"

The automatic synthesis of programs from high-level specifications is a highly attractive and increasingly viable alternative to manual system design. Because it allows the developer to focus on what needs to be done instead of how, and the resulting code is guaranteed to be correct, synthesis radically simplifies the software development process. The last decade has seen a lot of progress on program synthesis in two largely disjoint research areas. On the one hand, reactive synthesis can synthesize finite-state circuits from complex temporal control requirements; on the other hand, deductive synthesis can synthesize sequential programs performing complex data transformations. Both approaches fail, however, as soon as the systems need to deal with complex control and data simultaneously, such as embedded controllers processing numerical sensor values or mobile applications that need to react to complex user inputs.
In this talk, I will give an overview of our recent progress on addressing this challenge. I will present the first reactive synthesis method that natively integrates symbolic logical reasoning about unbounded data into a fully automated reactive synthesis procedure. The underlying technical insight is a novel technique, called acceleration, for symbolic computation of the set of winning states for a player in a synthesis game. This key feature makes our method applicable to classes of reactive program synthesis problems that are beyond the scope of any prior approaches. I will also discuss recent work on synthesis algorithms that utilize quantitative measures of system correctness.

Time:	Friday, 12.01.2024, 09:00
Place:

Termin als Datei downloaden und in den Kalender importieren.