[isabelle] PhD Position in Formal Verification of Concurrent Systems at Uppsala University

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
for further details. Applications close on December 14, 2014.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.