[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Research Position in Verified Confidentiality for Weak Memory Concurrency
https://people.eng.unimelb.edu.au/tobym/researcher19-weak-memory.html
I am seeking an exceptional researcher (either a graduate or a
postdoc) to research methods for verifying information flow security
for shared-memory concurrent programs executing on weak memory
consistency models. The methods will be applied to verify the security
of seL4-based critical embedded devices.
The position is for two years in the first instance, based at the
University of Melbourne under Dr Toby Murray
(https://people.eng.unimelb.edu.au/tobym/). This project will provide
the opportunity to collaborate with researchers at Australian National
University (ANU), Canberra; Data61's Trustworthy Systems Group (the
"seL4 team"), Sydney; and Australia's Defence Science and Technology
(DST) Group, Brisbane.
Candidates should have experience in at least one of the following:
- program verification (e.g. Hoare logic),
- information flow security,
- interactive proof assistants (e.g. Isabelle, Coq, etc.),
- concurrent program verification methods (e.g. Owicki-Gries,
Rely-Guarantee, Concurrent Separation Logic, etc.),
- weak memory consistency models (e.g. x86 TSO, etc.)
The following are indicative, entry-level salary figures:
Research Assistant (Bachelor's graduate): $65K (AUD)
Research Assistant (Master's graduate): $71K (AUD)
Postdoctoral Research Fellow: $90K (AUD)
Besides salary, total remuneration also includes 9.5% employer
superannuation contribution.
Applications close on April 30, 11:55pm Australian Eastern Standard
Time (GMT +10)
Further details, including how to apply, are available here:
https://people.eng.unimelb.edu.au/tobym/researcher19-weak-memory.html
Informal enquiries should be directed to
Toby Murray
toby.mur...@unimelb.edu.au
https://people.eng.unimelb.edu.au/tobym/
