2 PhDs + 1 Postdoc in Aarhus University on
“Algorithmic Verification and Synthesis for Concurrency”
Since I am starting a new research team at the Computer Science Department at Aarhus University, I am looking for 2 PhD students (fully paid, 3 years) and 1 Postdoc researcher (2 years). The positions are available from 1 August 2019 and the deadline for application is 1 May 2019.
Applications should be submitted online through these channels:
– PhDs: Information & online application: https://tinyurl.com/y3oht27v
– Postdoc: Information & online application: https://tinyurl.com/y4y5ayyr
It is important for me to build a truly diverse team, so all interested candidates are encouraged to apply, regardless of their personal background.
Project description:
Concurrent and distributed software systems govern large parts of our critical personal and social infrastructure, so their correct design is of utmost importance. Despite tremendous progress in automated verification, many challenges remain, due to the inherent complexity and scale of distributed data-intensive systems. A particular challenge is to handle the uncertainty on the environment in which these systems operate, like timing parameters, failure probabilities, and the (possibly malicious) behaviour of external agents.
In this project, we want to address these challenges by advancing and developing efficient parallel algorithms for symbolic reasoning and graph analysis. Moreover, we seek to study algorithms to synthesise correct solutions automatically, rather than verifying given solutions. In particular, we seek candidates for the following subprojects:
– PhD1: Parametric Verification and Parameter Synthesis. S/he will develop algorithms to verify systems with unknown parameters (time, probabilities, or other dimensions) and to synthesise constraints on such parameters, or compute optimal parameter values.
– PhD2: Strategy Synthesis for Solving Games. S/he will compute winning strategies for games that arise from the interaction between a system and its environment. Synthesised strategies form the core of test case generation, control algorithms, energy optimisation, etc.
– Postdoc: Symbolic Reasoning for Synthesis. S/he will develop and apply symbolic techniques, like SMT solving, abstract interpretation and invariant generation to the synthesis of concurrent systems. Approaches merging theorem proving and model checking are welcome.
Qualifications and specific competences:
Applicants to the PhD positions must have a relevant Master’s degree in Computer Science (or a related area).
The postdoc should have a PhD degree in a related topic and will be evaluated on her/his publication record, her/his specific ideas for this project, and the potential to pursue an independent academic career.
The successful candidate should demonstrate a strong theoretical background in logic and algorithms, broadly conceived. At the same time, s/he should not shy away from programming research prototypes, to conduct performance experiments and case studies that show the potential impact of the research. Finally, good writing and presentation skills (English) are important as well.
Since I am starting a new team in Aarhus, I am looking for curious, creative and motivated researchers, who like to share their own strong contributions within the team, in the context of local and international collaborations. The GSST will offer plenty of opportunities to train and strengthen your skills.
Place of Employment and Location:
The place of employment is the Computer Science department of Aarhus University. You will be located at the vibrant IT campus Katrinebjerg in Aarhus, the second largest city of Denmark. See for an impression: http://talent.au.dk/phd/aboutthephdatau/living-in-denmark-and-aarhus/
Aarhus University provides excellent working conditions: https://international.au.dk/research/researcher-positions/workingconditions/
Contact:
Applicants seeking further information are invited to contact:
Prof. Jaco van de Pol, jaco@cs.au.dk, https://cs.au.dk/~jaco/
