Internship in Best-Effort Synthesis Modulo Theories

Reactive synthesis typically asks for a strategy that guarantees a temporal specification against every possible behavior of an adversarial environment. When no such strategy exists, that is, when the specification is unrealizable, classical synthesis algorithms simply report failure, even though a controller that performs well against the environments that actually occur in practice may still be valuable. Best-effort synthesis addresses this limitation: rather than giving up when a winning strategy does not exist, it produces a strategy that is guaranteed to do as well as possible given how the environment actually behaves, winning whenever winning is still possible at each point of the interaction. This notion has recently been studied for LTLf (LTL on finite traces), including settings with multiple or layered environment specifications. A complementary notion, maximally permissive controller synthesis, instead seeks, among all strategies that do guarantee the specification, the one that restricts the system’s behavior as little as possible. In this internship we will adapt best-effort synthesis from LTLf to LTL modulo theories, where specifications combine temporal goals with constraints over data, and compare the resulting notion and algorithms against our recent work on maximally permissive controller synthesis. We will study the relationship between these two notions of doing well under uncertainty, and explore unified or complementary synthesis procedures for LTL 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. ### **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 6 months. ### **How to apply?** Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code **2026-07-intern-besteffortsynth**. Deadline for applications is **September 10th, 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 inquiries about the position, please contact: .