coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Research Position in Verified Confidentiality for Weak Memory Concurrency
Chronological Thread
- From: Toby Murray <toby.murray AT unimelb.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Research Position in Verified Confidentiality for Weak Memory Concurrency
- Date: Tue, 9 Apr 2019 02:15:21 +0000
- Accept-language: en-AU, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=Neutral smtp.pra=toby.murray AT unimelb.edu.au; spf=Pass smtp.mailfrom=toby.murray AT unimelb.edu.au; spf=None smtp.helo=postmaster AT au-smtp-delivery-203.mimecast.com
- Ironport-phdr: 9a23:+lUZUBBhJ/Fu8mD8oehVUyQJP3N1i/DPJgcQr6AfoPdwSPX4rsbcNUDSrc9gkEXOFd2Cra4d0qyP7+u9BSRAuc/H7ClaNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULnIduMLs9xxTGrnZIdOld2GdkKU6Okxrm6cq84YJv/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4cSGFcXMheSjZBD5u8YYUREuQBIehWoYr8p1QBsRSwChKhBP/2yjNUmnP6wbE23uQnHArb3AIgBdUOsHHModvrM6cdSuC0x7TPwzXedfNWwy3y6YjVeR0mvfGMWql/cMrLxUkqCgPFlE+QppblPj6Oy+QNtWmb7+9+WuKrkGErsR9+rSWyxss2kIbJm5sYx1bZ/it3x4Y1IMe3SE99YdO8DZtQsSCaN45oTcMmWG5kojg1xaAbuZKhZicK1ZIqzAPcZfyfa4WE/xHuWPqLLTtlh39ofKiziwix/ES61OHwSse53E5XoiZbkdTArG4B2hzP5sSdVvdx5Fqt1SqP2gzL5OFLP0M5mbbeJpMk3LI/i5QevErGEyPohkn7g7GZe0Ag9+S19evqYrDrqoKCO4J0jgzzNLkllNalDuQiKAcOWnCW+eSi273n+k30WK9FjuAvnqnCtZDaOdwbqrekDABL1oYj6gi/ACm80NUYhHULMk5JdRydg4jsOlHOJe73AuuljFS3jDdn3ezJPrrkApnVL3jDlqnufapl5kJBywc/0cpT649XB7wFOv7/REz8uMbGAhMlPQG42+PnB8981oMaV2KPGKiZMKbKvF+U4eIgOOmNaJUQuDbgMfgl/eThjH8ilF8Ae6mp3J4XZ268Hvt9OUmWf2fjgsobHWgQowoyVPbqh0GaUT5Pe3ayWLox6S08CIK/FIvMWoStgKGa0yqgBZ1XZmVGCkiWHnvydoWEXe0MaCOILcN7nDwET+vpd4h0nxqprUrxz6dtBuvS4CwR85z5npAh7OrK0Bo26DZcDsKH0mjLQXsizU0SQDpj4Kd1sARY102Z2Lkw1+BfH80V4u5TSA4rHYPazul3D9q0Vw7cON6UHgX1Cu66CC08G4pii+QFZFxwTo3730LzmhGyCrpQrISlQZk986bSxX/0fpgv1nDH0aQlhR8rTtYJPHD03/cipTiWPJbAlgCir4jvdakY23WQpm6eiHGLoFkdXAN0ULvIR2FaPBON69H4407JRqSyT78gN1kZkJLQGu5xctTsyG5+arL7It2HPTCsnWa1CBKCgL6AcczjZjdH0Q==
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/
---------
Toby Murray, DPhil (University of Oxford)
Senior Lecturer, School of Computing and Information Systems
University of Melbourne
https://people.eng.unimelb.edu.au/tobym/
toby.murray AT unimelb.edu.au
- [Coq-Club] Research Position in Verified Confidentiality for Weak Memory Concurrency, Toby Murray, 04/09/2019
Archive powered by MHonArc 2.6.18.