Reactive systems are often required to satisfy specifications that combine ordering constraints among events with constraints over data values, such as counters, timers, or sensor readings. Linear Temporal Logic (LTL) is the standard formalism used to specify and automatically synthesize reactive controllers, but plain LTL can only express Boolean propositions and cannot relate data values across time. LTL Modulo Theories (LTL^T) extends LTL with atomic propositions drawn from a first-order theory, but synthesizing controllers for LTL^T is substantially harder than for plain LTL, since realizability must reason jointly about discrete control choices and data constraints.
One successful approach to LTL^T synthesis is CEGRES (Counterexample-Guided Reactive Synthesis), which combines an abstraction of the theory predicates into Boolean propositions with a discrete LTL synthesis engine, refining the abstraction iteratively using counterexamples until a sound and complete controller is produced, or unrealizability is established. The discrete engine that solves the abstracted Boolean problem at the core of this loop currently relies on classical automata-based synthesis algorithms.
In this internship we will explore bounded synthesis as the discrete engine inside CEGRES: instead of solving the abstracted Boolean LTL realizability problem via automata constructions, we will search for implementations of increasing bounded size using constraint solving, an approach that has proven effective and scalable for plain LTL synthesis. We will first integrate a bounded synthesis engine as a drop-in replacement for the discrete component of CEGRES, and then investigate how to extend bounded synthesis to reason about theory atoms directly, without first abstracting them away, aiming for a more direct and efficient algorithm for reactive synthesis modulo theories.
Applications are invited to apply for an intern 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 6 months.
Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code 2026-06-intern-boundedsynth. Review of applications will begin immediately and close on July 15th, 2026.
The recruitment process will comply with the IMDEA Software Institute’s OTM-R Policy (Open, Transparent and Merit-based Recruitment).
For inquiries about the position, please contact:
