Reactive synthesis is the problem of automatically creating a system from a temporal logic specification. The overall goal of the project is to extend temporal logic reactive synthesis modulo theories with machine learning techniques to (1) improve the scalability and explanability of the solutions, and (2) to apply reactive synthesis to shielding, where a reinforcement learning behavioral componen, for example in autonomous vehicles, is combined with a shield obtained using synthesis.
The extension of reactive systems with theories allows to define much richer classes of reactive synthesis problems, at the price of higher complexity. The first problem that the student will study is the use of machine learning techniques to improve the performance of tools for reactive synthesis modulo theories. The second problem is the application of these tools, in composition with controllers obtained using machine learning to craft safer systems.
Applications are invited to apply for a PhD position at the IMDEA Software Institute, Madrid, Spain.
Selected candidates will work with César Sánchez and an international team of graduate students and researchers focusing on formal methods.
Candidates should have an excellent MSc or BSc degree (or be close to complete one) in computer science, mathematics, or a related discipline, with an interest in the above area, and a strong commitment to research. Proven top programming skills as well as ability to understand and develop algorithms are required. Good teamwork and communication skills, including excellent spoken and written English are also required.
The position is based in Madrid, Spain, where the IMDEA Software Institute is situated. The institute provides for travel expenses and an internationally competitive stipend. The working language at the IMDEA Software Institute is English.
The duration of the position will be 4 years.
Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code 2025-03-phd-neurosymbolic. Deadline for applications is April 29th, 2025. Review of applications will begin immediately.
The recruitment process will comply with the IMDEA Software Institute’s OTM-R Policy.
For enquiries about the position, please contact:
