Internship in Fast Synthesis Modulo Simple Theories

Reactive synthesis for specifications over bounded integer domains, such as fixed-width bitvectors, is typically handled by discretization via “bit-blasting”: each bit of the bounded integer is encoded as an independent Boolean signal, and the resulting specification is solved with plain LTL synthesis tools. While bit-blasting is simple and reuses existing solvers, it destroys the arithmetic structure of the domain, and the state space explored during synthesis grows exponentially with the bitwidth, making synthesis impractical for all but the smallest domains. LTL Modulo Theories (LTL^T) generalizes reactive synthesis to reason about theory atoms directly rather than plain Booleans, and has been shown to scale to infinite domains, such as integers and reals, using SMT-based reasoning. Bounded domains, such as bitvectors, pose a different challenge: because the domain is finite and equipped with a specific modular and bit-level structure, decision procedures specialized for bounded integer arithmetic may enable synthesis algorithms that avoid the cost of bit-blasting while remaining decidable and efficient. In this internship we will explore reactive synthesis modulo bounded integer theories, such as bitvectors, using theory reasoning over the bounded domain directly rather than blasting it into individual bits, aiming for synthesis algorithms whose cost scales much more gently with the bitwidth. We will then investigate which other “simple theories” admit decidable and practically efficient synthesis procedures, with the goal of building a family of fast, specialized synthesis tools for these 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-fastsynth**. 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: .