[isabelle] Research Position in Verified Confidentiality for Weak Memory Concurrency

Research Position in Verified Confidentiality for Weak Memory Concurrency

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:

Informal enquiries should be directed to
  Toby Murray
  toby.murray at unimelb.edu.au

Toby Murray, DPhil (University of Oxford)
Senior Lecturer, School of Computing and Information Systems
University of Melbourne

toby.murray at unimelb.edu.au

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.