Postdoc in algorithms for arithmetic theories and SMT solving

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.