Applications are invited for postdoc and PhD positions at the IMDEA
Software Institute, Madrid, Spain.

The successful candidates will work under the supervision of Aleks
Nanevski ( The topic of the
research, to be determined based on the common interests of the
candidate and the supervisor, will be in the areas of software
verification of concurrent programs, separation logic, and
language-based security. The research will be funded by Aleks' ERC
Consolidator grant "MATHADOR: Type and Proof Structures for Concurrent
Software Verification", which aims to investigate the type-theoretic
foundations for concurrency.

PhD candidates should have an excellent MSc or BSc degree in computer
science or a related subject, with an interest in the above areas, and
a strong commitment to research. An MSc or a BSc thesis is a plus. PhD
positions are for four years.

Postdoc candidates should have, or expect shortly to obtain, a PhD in
computer science. The ideal candidate will have expertise in program
semantics and program logics, concurrent or distributed computing,
type theory or interactive theorem proving, as they apply to the above
areas. Postdoc positions are initially for one year, with
possibilities for extension (depending on performance).

The positions require good teamwork and communication skills,
including excellent spoken and written English. Salaries at IMDEA
Software Institute are internationally competitive.

Interested applicants should contact Aleks directly (aleks dot
nanevski at imdea dot org). Formal applications should be submitted
online at

and mention this announcement in the submitted materials. Review of
applications will begin immediately.