Applications are invited for a PhD fellowship/scholarship at Graduate School of Natural Sciences, Aarhus University, Denmark, within the Computer Science programme. The position is available from August 2026 or later.
Title:
Formal Verification of Concurrent and Distributed Systems
Research area and project description:
Modern software systems — from operating systems and distributed databases to concurrent applications and security-critical infrastructure — are notoriously difficult to reason about correctly. The goal of formal program verification is to provide rigorous mathematical guarantees about the behavior of such systems, going beyond testing to establish correctness by proof. This PhD project is situated at the foundational end of this endeavor: rather than applying existing verification tools, the aim is to develop the logical and mathematical foundations that make principled verification possible.
The research will focus on separation logic and its application to the verification of concurrent and distributed programs. Separation logic is a powerful program logic that supports modular, compositional reasoning about programs that manipulate shared state. The work is mathematical in nature and combines ideas from logic, type theory, and programming language semantics. Recent advances — exemplified by the works building on the Iris framework, which is developed in part at Aarhus University — have extended separation logic to handle higher-order programs, fine-grained concurrency, and distributed computation, e.g., the Trillium and Aneris program logic frameworks. The PhD project will contribute to this line of work, with possible directions including the design of new program logics, the development of semantic models, and the mechanized verification of programs in the Rocq proof assistant.
Please upload a project description (½-4 pages). This document should describe your ideas and research plans for this specific project. If you wish to, you can indicate an URL where further information can be found.
Qualifications and specific competences:
Applicants to the PhD position must have:
- A BSc or MSc degree in computer science, mathematics, or a related field
- Strong background in mathematics and mathematical logic
- Experience with programming languages theory and/or program verification
- Familiarity with proof assistants (especially Rocq) is a plus but not strictly required
Place of employment and place of work:
The place of employment is Aarhus University, and the place of work is Department of Computer Science, Åbogade 34, 8200 Aarhus N, Denmark.
Contacts:
Applicants seeking further information for this project are invited to contact: Associate Professor, Amin Timany, timany@cs.au.dk
How to apply:
For information about application requirements and mandatory attachments, please see the Application guide. Please read the Application guide thoroughly before applying.
When ready to apply, go to https://phd.nat.au.dk/for-applicants/apply-here/ (Note, the online application system opens 1 March 2026)
Please note:
At the Faculty of Natural Science at Aarhus University, we strive to support our scientific staff in their career development. We focus on competency development and career clarification and want to make your opportunities transparent. On our website, you can find information on all types of scientific positions, as well as the entry criteria we use when assessing candidates. You can also read more about how we can assist you in your career planning and development.
Aarhus University’s ambition is to be an attractive and inspiring workplace for all and to foster a culture in which each individual has opportunities to thrive, achieve and develop. We view equality and diversity as assets, and we welcome all applicants. All interested candidates are encouraged to apply, regardless of their personal background.
