Concurrency Verification

Picture of nisansala-yatapanage.md Nisansala Yatapanage

19 Feb 2023

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. Rely/guarantee reasoning is a compositional program reasoning method for concurrent programs. There are many interesting areas of research to explore, such as:

  • Exploring the relationship between rely/guarantee reasoning and linearisability. While rely/guarantee is usually a top-down approach starting from the abstract specification, linearisability is a bottom-up approach, but understanding how these two techniques intersect is an open problem.
  • Developing approaches for modelling and verifying concurrent algorithms without locks (non-blocking algorithms). These types of problems are particularly challenging.
  • Comparing the different types of concurrency approaches, e.g. separation logic and rely/guarantee reasoning, to understand the fundamental properties of concurrency.
  • Incorporating temporal logic into rely/guarantee approaches, to enable properties to be expressed involving the future and past.

Requirements

These projects are suitable for any level, from Bachelor research projects and Honours to PhD projects. You will need an ability to reason about logic, and completion of a course on discrete mathematics, including logic and set theory, e.g. MATH1005 at ANU. Previous experience with concurrent programming is beneficial but not required. Previous knowledge of Hoare logic, such as covered in COMP1600 at ANU, is also useful. PhD students should have a strong background in areas such as mathematics, logic, formal methods and software engineering.

Depending on your level, background and interests, the project could be on a more theoretical side, such as developing the theory and exploring the fundamental concepts, or practical, such as involving theorem proving or investigating particular algorithms, or a combination of both.

Scholarships are available for PhD students.

Contact

If you’re interested in this area, contact Dr. Nisansala Yatapanage.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times arrow-up