IMDEA Software

IMDEA initiative

Home > Open Positions

PhD in Automata Theory

The IMDEA Software Institute (Madrid, Spain) invites applications for a PhD position in the area of Formal Verification.

The successful candidate will work with Pierre Ganty to develop algorithms for language inclusion or emptiness problems when the languages are defined as least solution of constrained Horn clauses capturing known models like Petri nets; or even some abstraction of programs like predicate automata.

The successful PhD candidate will formally define inclusion problems, study their decidability / complexity status, define algorithmic solutions when possible and conduct experimental evaluations when appropriate.

Who should apply?

Applicants should have finished (or be close to finish) a master degree in computer science or mathematics. A passion for language / automata theory is required. Programming experience will be considered a plus as well as some good knowledge of abstract interpretation.

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 institute is English. Knowledge of Spanish is not required.


The position is intended to last for the duration of the doctoral studies, which is usually four years. The successful candidate should preferably start around mid October 2021.

How to apply?

Applicants interested in the position should submit their application at using reference code 2021-09-phd-chc-wqo. Deadline for applications is September 17th, 2021. Review of applications will begin immediately.

Want to know more

For enquiries about the position, please contact: Pierre Ganty, firstname.lastname (at)