
<html><head><style>body{font-family:Helvetica,Arial;font-size:13px}</style></head><body><div style="font-family:Helvetica,Arial;font-size:13px; ">Hi all,</div><div style="font-family:Helvetica,Arial;font-size:13px; "><br></div><div style="font-family:Helvetica,Arial;font-size:13px; ">If you have (or are) a promising undergraduate or masters student who would be interested in working with us on the lovely intersection of programming languages and formal methods, my colleague Christine has recently begun looking for PhD students. </div><div style="font-family:Helvetica,Arial;font-size:13px; "><br></div><div style="font-family:Helvetica,Arial;font-size:13px; ">The ad is attached below. Both of us will be in Berlin for the rest of the week (after ICFP), so feel free also to talk to us in person if you are around.</div><div style="font-family:Helvetica,Arial;font-size:13px; "><br></div><div style="font-family:Helvetica,Arial;font-size:13px; ">Liam</div><div style="font-family:Helvetica,Arial;font-size:13px; ">—</div><div style="font-family:Helvetica,Arial;font-size:13px; "><br></div><div style="font-family:Helvetica,Arial;font-size:13px; "><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">If only there were a place where I could prove theorems, change the world, and have </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">fun while doing it... </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Sounds too good to exist? </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">In the Trustworthy Systems team at UNSW and Data61 that's what we do for a living. We </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">are the creators of seL4, the world's first fully formally verified operating system </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">kernel with extreme performance and strong security & correctness proofs. Our highly </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">international team is located on the UNSW campus, close to the beautiful beaches of </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">sunny Sydney, Australia, one of the world's most liveable cities. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">We are offering scholarships to multiple motivated PhD students who want to join us </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">in Sydney, move things forward, and have a global impact. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Cogent is a language we designed that co-generates code and proofs in order to ease </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">the verification of systems components around seL4. Potential PhD topics include </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">designing and implementing new domain-specific programming languages extending </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Cogent, writing formal specifications and proofs in Isabelle/HOL, developing formally </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">verified infrastructure for building secure systems on top of seL4, contributing to </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">improved proof automation and reasoning techniques, and applying formal proof to </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">real-world systems and tools. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">To apply you should have (or be about to obtain) a bachelor degree (minimum 4 years) or </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">a bachelor and a masters degree in Computer Science, Mathematics, or similar. You should </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">also meet UNSW's minimum English requirements: </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><a href="https://www.unsw.edu.au/english-requirements-policy" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto; font-family: "helvetica Neue", helvetica; font-size: 14px;">https://www.unsw.edu.au/english-requirements-policy</a><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;"> </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">You should also possess a significant subset of the following skills: </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- functional programming in a language like Haskell, ML, or OCaml </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- first-order or higher-order formal logic </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- basic experience in C </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- ability and desire to quickly learn new techniques </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- ability and desire to work in a larger team </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">If you additionally have experience </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- in software verification with an interactive theorem prover such as </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Isabelle/HOL, HOL4, Coq, or Agda, and/or </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- with programming languages and verified or certifying compilers </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">you should definitely apply! </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">You will work with a unique world-leading combination of OS and formal methods </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">experts, students at undergraduate and PhD level, engineers, and researchers from </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">5 continents, speaking over 15 languages. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Trustworthy Systems is a fun, creative, and welcoming workplace with flexible </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">hours & work arrangements. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">We value diversity in all forms and welcome applications from people of all ages, </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">including people with disabilities, and those who identify as LGBTIQ. See </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><a href="https://ts.data61.csiro.au/diversity/" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto; font-family: "helvetica Neue", helvetica; font-size: 14px;">https://ts.data61.csiro.au/diversity/</a><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;"> for more information. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">For applying, email us on <</span><a href="mailto:c.rizkallah@unsw.edu.au" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto; font-family: "helvetica Neue", helvetica; font-size: 14px;">c.rizkallah@unsw.edu.au</a><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">> a copy of your CV, </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">cover letter, transcripts, and contact information for two referees. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">This round of applications closes </span><a href="http://airmail.calendar/2019-09-01%2012:00:00%20GMT+2" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto; font-family: "helvetica Neue", helvetica; font-size: 14px;">on the 1st of September 2019</a><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">For any questions on these positions, please contact Christine Rizkallah </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><</span><a href="mailto:c.rizkallah@unsw.edu.au" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto; font-family: "helvetica Neue", helvetica; font-size: 14px;">c.rizkallah@unsw.edu.au</a><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">> </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">The Cogent project is open source. </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Check it out at </span><a href="https://ts.data61.csiro.au/projects/TS/cogent.pml" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto; font-family: "helvetica Neue", helvetica; font-size: 14px;">https://ts.data61.csiro.au/projects/TS/cogent.pml</a><span style="font-family: "helvetica Neue", helvetica; font-size: 14px;"> </span><br style="font-family: "helvetica Neue", helvetica; font-size: 14px;"></div><br><div class="gmail_signature"></div></body></html>