Machine learning (ML), including reinforcement learning and supervised learning, has shown significant potential for a wide range of synthesis tasks, including controller synthesis and program synthesis. A promising line of work has combined ML with traditional formal verification in a CEGIS-style loop: ML is used to efficiently explore the space of candidate solutions, while formal verification checks their correctness and provides counterexamples to guide further learning. This demonstrates how ML and formal methods can complement each other in a tightly integrated framework, combining the flexibility and scalability of learning with the rigorous guarantees of formal verification. Applications are invited to apply for one phd position at the IMDEA Software Institute, Madrid, Spain.
However, existing learning-enabled synthesis frameworks have largely been developed independently for specific domains, resulting in a fragmented landscape of domain-specific techniques. This project aims to take a step towards a more general approach based on Skolem function synthesis, which provides a general formulation of synthesis problems and can encompass problems beyond the domains traditionally considered, including applications such as solving partial differential equations. The goal of this PhD position is therefore to develop a learning-enabled CEGIS framework for Skolem function synthesis, and to use this general framework to address synthesis problems across a range of different domains.
The PhD student will be jointly supervised by Kaushik Mallik and Alessio Mansutti.
Candidates with master’s degrees in CS are welcome to apply. Prior backgrounds in formal verification and/or machine learning will be appreciated but not necessary.
The positions are based in Madrid, Spain, where the IMDEA Software Institute is situated. Salaries are internationally competitive and include attractive conditions such as access to an excellent public healthcare system. The working language at the institute is English. Knowledge of Spanish is not required.
Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code 2026-09-phd-lns. Deadline for applications is September 30th, 2026. Review of applications will begin immediately.
The recruitment process will comply with the IMDEA Software Institute’s OTM-R Policy (Open, Transparent and Merit-based Recruitment).
For enquiries about the position, contact Kaushik Mallik and Alessio Mansutti .
