PhD Studentship in Computer Science - Verifying the Design of Concurrent Programs (CS025) - School of Computing Science (Full-time)

The successful candidate will join in an active research project that is trying to combine the advantages of several of the most promising ways of reasoning about concurrent programs. This research area is becoming ever more important because of the advent of many core systems.

One approach is Cliff Jones’ rely/guarantee thinking and another is the work on separation logics. This is not a competition – we are looking for how to get the best from a combination of the two avenues of research (and possibly others). In fact, we run a productive series of research meetings with the (London/Cambridge) researchers working on separation logics.

Cliff has successfully supervised over twenty PhDs and finds it best for the candidate/supervisor to develop the detailed thesis proposal in the first months of cooperation but likely themes include a combination with Carroll Morgan’s refinement calculus and ways of subsuming linearisability arguments.

The general project funding is expected to include ARC support for a project with University of Queensland as well as EPSRC funding.

You should have either a First class honours degree in Computing Science, Mathematics, or other relevant science or engineering subject, or a or 2.1 in Computing Science, Mathematics or other relevant science or engineering subject and a distinction level Masters degree in a related subject. Equivalent experience will also be considered.