The IMDEA Software Institute (Madrid, Spain) invites applications for a research internship in the area of Automata Theory and Verification. The successful candidate will work with Pierre Ganty and Alessio Mansutti.
The proposed internship involves developing techniques to quickly estimate the sizes of data structures produced during the execution of an algorithm on a specific input; where “quickly” here means faster than running the algorithm itself.
For instance, consider a procedure that relies on automata as data structures to, e.g., determine whether a linear arithmetic formula is satisfiable. Then, one such technique should be able to provide lower bounds on the number of states of the largest automaton generated during the execution of the procedure on that particular formula.
The successful candidate will implement their techniques in a research prototype.
Applicants should be B.Sc. or M.Sc. in computer science, mathematics or a related discipline. Basic knowledge of automata theory is required (e.g. finite state automata and their manipulations) as well as a strong commitment to research. To implement a research prototype, some experience with the Python programming language is required.
Good command of English both spoken and written is also required.
Located in the Montegancedo Science and Technology Park, it perfectly combines the sunny and vibrant city of Madrid with cutting edge research and an inspiring working environment. The institute provides an internationally competitive stipend, access to excellent public healthcare, unemployment benefits, retirement benefits, and support for research-related travel. English is the primary working language, and knowledge of Spanish is not required.
The internship duration is intended to be for 6 months. The ideal start period is Fall 2025. The work schedule can be adapted to the needs of the selected candidate.
Applicants interested in the position should submit their application at https://careers.software.imdea.org/ selecting the option Intern and using reference code 2025-03-intern-lower-bounds-automata. Deadline for applications is April 29th, 2025. Review of applications will begin immediately.
The recruitment process will comply with the IMDEA Software Institute’s OTM-R Policy.
For inquiries about the position, please contact: Pierre Ganty () or Alessio Mansutti ().
Funded by the Madrid Regional Government (César Nombela grant 2023-T1/COM-29001)
