Email Gateway (Aug 19 2022 at 16:31): Email Gateway (Aug 19 2022 at 16:31):From: Tjark Weber <tjark.weber@it.uu.se>
PhD position in Formal Verification of Concurrent Systems
at Uppsala University, Sweden
Multi-core processors are ubiquitous, but writing correct concurrent
code is hard. Multi-threaded applications are prone to subtle bugs,
such as deadlocks and race conditions. These bugs are notoriously
difficult to find. Consequently, there is great interest in formal
verification techniques for concurrent code. The objective of this
project is to build a trustworthy framework that supports the
interactive and semi-automated verification of programs that utilize
low-level concurrency.
The work will be carried out in the Modeling of Concurrent Computation
research group (http://www.it.uu.se/research/group/mobility), which is
part of the Uppsala Programming for Multicore Architectures Research
Centre (http://www.it.uu.se/research/upmarc).
Qualifications: The candidate should have a Master of Science in
Computer Science, Computer Engineering or equivalent, ideally with a
strong background in logic, formal semantics and concurrent/parallel
programming. Experience with interactive theorem proving (e.g.,
Isabelle, Coq) is a plus.
Please see the official announcement at
http://www.uu.se/en/about-uu/join-us/jobs-detail-page/?positionId=46736
for further details. Applications close on December 14, 2014.
Last updated: Apr 26 2024 at 08:19 UTC