Speaker: Andoni Rodríguez (IMDEA Software Institute)
Title: Reactive Synthesis Modulo Theories
We address the problem of developing reactive systems using formal methods. In order to do so, we built upon previous work that specified dynamics of such systems using temporal logics, and moreover were able to check consistency of such specifications (i.e., the realizability problem) and compute correct-by-construction systems in realizable instances (i.e., synthesis problem). However, most of previous work was constrained to using finite data. Therefore, we extended synthesis and realizability to using more expressive data (e.g., arithmetic). We also showed that our results can be adapted to shielding and explainability.
Andoni Rodríguez is a researcher at the IMDEA Software Institute, specializing in the intersection of artificial intelligence and formal methods. Andoni's primary research interest lies in developing mathematically rigorous methods for creating correct-by-construction systems, particularly within safety-critical contexts and reactive systems that interact with complex environments, such as autonomous systems. His Ph.D. thesis (with prof. César Sánchez) centers on building reactive synthesis modulo theories, advocating for trustworthy, interpretable, and scalable technologies. This work has garnered positive feedback from both industry and academia, with contributions to conferences such as CAV and AAAI.