16 Jan 2024
Job Information
- Organisation/Company
The Australian National University- Department
School of Computing- Research Field
Computer science » Other
Computer science » Systems design
Mathematics » Mathematical logic
Mathematics » Discrete mathematics- Researcher Profile
First Stage Researcher (R1)- Country
Australia- Application Deadline
19 Jan 2024 - 23:59 (Australia/Sydney)- Type of Contract
Temporary- Job Status
Full-time- Is the job funded through the EU Research Framework Programme?
Not funded by an EU programme- Is the Job related to staff position within a Research Infrastructure?
No
Offer Description
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 ([email protected] ) (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.
Requirements
- Research Field
- Mathematics » Mathematical logic
- Education Level
- Master Degree or equivalent
- Research Field
- Computer science » Systems design
- Education Level
- Master Degree or equivalent
- Languages
- ENGLISH
- Level
- Excellent
Additional Information
Work Location(s)
- Number of offers available
- 1
- Company/Institute
- The Australian National University
- Country
- Australia
- City
- Canberra
- Geofield
Where to apply
[email protected]
Contact
- City
Acton- Website
https://yatapanage.com- Street
108 North Road
[email protected]
STATUS: EXPIRED