Project Area
The verification of programs is essential, as software now controls everything in our lives. It is particularly important to ensure that safety-critical systems do not pose any danger to human lives. Verification provides a guarantee that a program will do what it was supposed to do.
Multiple projects are available in this area, supervised by Dr. Nisansala Yatapanage (see my website). Some example projects include:
- Investigating the verification of non-blocking concurrent algorithms using various techniques including model checking and rely-guarantee reasoning (a method for reasoning about concurrent programs based on Hoare logic).
- Developing approaches for the verification of safety-critical systems, including determining the effects of hardware component faults on the system.
Please come and have a chat with me and I can explain some of the ideas. The exact details of the project will depend on your study level, background and interests.
Suitability
Students of any level are welcome to come and have a chat with me, including undergraduate and PhD. Recommended background is discrete maths, logic and set theory, but we can talk about your suitability in detail when we meet. Email me at nisansala.yatapanage@anu.edu.au.
Related Course
If you are going to be in 4th year in 2025, have a look at the new Special Topics course COMP4011/8011 that I’ll be running on Specification and Verification Approaches for Concurrency. See the description on this page (scroll down to Sem. 1, 2025): https://comp.anu.edu.au/study/special-topics/