PhD Scholarship in Verification of Concurrent Algorithms

About the Project

Concurrency is increasingly prevalent in modern applications, but it is notoriously difficult to ensure that concurrent programs have been designed correctly. Compared to sequential programs, concurrent programs can exhibit behaviour that a programmer may not have anticipated. This has serious implications for applications such as safety-critical systems. Rely/guarantee reasoning is a compositional program reasoning method for concurrent programs. The aim of this project is to explore the use of rely/guarantee reasoning on non-blocking algorithms, which are particularly challenging for verification, particularly in regard to issues such as the ABA problem and handling progress properties.

One of the aims of the project is to investigate the relationship between rely/guarantee and refinement with bisimulation relations such as next-preserving branching bisimulation, which preserves full CTL*. A bisimulation relation holding between the abstract and concrete traces shows that the same progress properties which hold on the abstract trace also hold on the concrete trace. The project will involve investigating these ideas for verifying non-blocking concurrent algorithms. As well as the theoretical foundations, the project includes the development of a framework using theorem proving or model checking.

The project scope is quite flexible and applicants are welcome to discuss related project ideas. The project can be tailored to the student's interests and background, e.g. exploring the relationship between rely/guarantee and linearizability or the links to separation logic.

Student Requirements

A background in computer science, software engineering, mathematics or related fields is essential. Familiarity with formal methods and logic is desirable. Experience with program reasoning approaches, theorem proving, temporal logic or model checking would be an advantage but is not essential. The applicant will need to meet the ANU requirements for PhD admission (see https://cecc.anu.edu.au/study/phd-mphil).

The starting date is flexible but preferably before mid 2024. Later starting dates may be possible.

Environment

The School of Computing at ANU provides an excellent working environment. The successful applicant will become part of the Foundations of Computing group, a vibrant research group which holds regular seminars and PhD monitoring days to support students.

This position comes with a generous scholarship. Details will be provided on request.

To apply

Please send a full C.V., academic transcripts for all degrees and links to copies of honours or masters theses by email to Dr. Nisansala Yatapanage (nisansala.yatapanage@anu.edu.au) (visit https://yatapanage.com for more information about her research). Apply by January 19th for full consideration. Applications will continue to be accepted after that date, until the position is filled.