The overall goal of the project is to develop scalable algorithms for reactive synthesis modulo theories by coupling automata-theoretic game solving with on-demand theory reasoning.

An important area of formal methods is the synthesis of controllers for critical systems modeled using temporal logic over rich data. In the modulo theories setting, the plant is described by logical theories (e.g., linear arithmetic over signals) rather than purely Boolean variables, and the goal is to compute a strategy that satisfies an LTL specification for all behaviors of the environment. From the practitioner’s point of view, it is crucial that problems in the software requirement phase are uncovered as early as possible, which requires synthesis algorithms that scale to realistic plant models.

Previous algorithms for solving reactive synthesis modulo theories follow one of two paradigms. Either the theories are eagerly eliminated through Boolean abstractions, to which standard automata- and game-based synthesis is then applied, or a counterexample-guided abstraction refinement loop is used, iteratively refining the abstraction until a solution or a disproof of realizability is found (e.g., CEGRES). Both paradigms decouple theory reasoning from game solving: eager abstraction discards precision upfront and can lead to combinatorial explosion, while refinement repeatedly solves games on abstractions that may be irrelevant to the final strategy.

This PhD proposes a third intermediate approach to synthesis modulo theories, analogous to lazy SMT solving, which we have called coupled reactive synthesis modulo theories. Instead of abstracting the formula upfront, theory reasoning is performed during game solving: the game algorithm issues targeted queries to a theory solver only when it needs to reason about successors exploration, so that theory precision is spent only on the parts of the exploration that are relevant to the specification.

The student will investigate two main lines. (1) Jointly handling the arena description (plant)



together with the LTL specification (goals), developing a single representatio admitting a single automata-based game solving. (2) Exploring combinations of low-level automata techniques for reactive synthesis – such as Emerson-Lei style constructions and good-for-games constructions – with theory solving, exploiting structural properties of the games (e.g., memory requirements and determinacy) to guide and reduce theory queries.

The tasks will require to prove the mathematical correctness of the developed techniques as well as implementing prototypes and evaluating them against the state of the art, including both the eager and the refinement-based approaches.

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.

Who should apply?

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.

Working at IMDEA Software 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.

Dates The duration of the position will be 4 years.

How to apply?

Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code 2026-09-phd-coupledsynth . Review of applications will begin immediately and close on October 1st, 2026 .

The recruitment process will comply with the IMDEA Software Institute’s OTM-R Policy (Open, Transparent and Merit-based Recruitment).

📌 PhD in Coupled Reactive Synthesis Modulo Theories (Pozuelo de Alarcón)
🏢 IMDEA Software Institute
📍 Pozuelo de Alarcón