[TYPES/announce] Research Position in Verified Confidentiality for Weak Memory Concurrency

[Toby Murray]

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.murray at unimelb.edu.au
  https://people.eng.unimelb.edu.au/tobym/