The UK Research Institute in Verified Trustworthy Software Systems and the UK's National Cyber Security Centre have provided a PhD studentship to work with Mark Batty at the University of Kent in Canterbury, UK. The position is part of the "Specification and verification of C++ data structure libraries" project.
The studentship covers UK/EU fees, a travel budget and a stipend for 3.5 years. There is an option to teach, but no requirement. Non-EU students are welcome to apply but are subject to higher fees and would need to find funding for the difference. The position starts in September 2018. Applicants must have, or be about to complete a degree in Computer Science or Mathematics at the BSc or MSc level.
Topic: Concurrency in C/C++ and Java is broken: the language specifications do not adequately describe when the programmer can rely on the compiler to leave program dependencies in place, or when they cannot and the optimiser is free to remove them. Removing dependencies can lead to weak-memory concurrency behaviour. Industry bodies like the International Standards Organisation (ISO) keenly await a new candidate C/C++ concurrency specification that fixes these problems.
Using skills in formal specification, verification, mechanised proof and tool building, we are developing a specification of concurrency that fixes current flaws. This studentship focusses on this area of research: the work is theoretical, but has the potential to impact an important mainstream language.
For a broader view of Batty's work, see his Royal Society paper.
Interested candidates should contact Batty.