The IMDEA Software Institute (Madrid, Spain) invites applications for a postdoctoral position in the areas of algorithms, arithmetic theories, and SMT solving. The successful candidate will work in collaboration with Alessio Mansutti.
The goal of the postdoc is to develop algorithmic techniques and establish complexity results for non-convex extensions of Linear Integer Arithmetic, featuring, e.g., exponential functions or divisibility relations, as well as their relaxation over the reals. Further direction of study include the development of succinct representations for solutions to formulae in these theories, and establishing model-theoretic properties of these theories (e.g., distality, finite VC dimension,…).
Arithmetic theories, such as Linear Integer Arithmetic, are first-order logics about number systems. They represent a fundamental branch in mathematical logic, and play a pivotal role in various areas of computer science, encompassing both theoretical and practical applications. They are extensively used in the areas of formal methods, optimization, combinatorics on words and automata theory.
Candidates should hold a PhD in Computer Science or be close to completing one, and have a promising publication record in the relevant areas (logic for computer science, algorithms, optimization, and computer algebra). Programming experience will be considered a plus, as well as good prior knowledge on arithmetic theories.
The positions are based in Madrid, Spain, where the IMDEA Software Institute is situated. Salaries are internationally competitive and include attractive conditions such as access to an excellent public healthcare system. The working language at the institute is English. Knowledge of Spanish is not required.
The ideal starting period is early October 2026.
Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code 2026-05-postdoc-arith. Deadline for applications is May 30th, 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: Alessio Mansutti at ().
