<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; ">My research group is currently looking for postdocs. The ad is attached below. Please direct all enquiries to Christine Rizkallah (<a href="mailto:c.rizkallah@unsw.edu.au">c.rizkallah@unsw.edu.au</a>). </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; "><br></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; "><br></div><div style="font-family:Helvetica,Arial;font-size:13px; "><div class="" 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</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">fun while doing it...</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Sounds too good to exist?</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" 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</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">are the creators of seL4, the world's first fully formally verified operating system</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">kernel with extreme performance and strong security & correctness proofs. Our highly</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">international team is located on the UNSW campus, close to the beautiful beaches of</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">sunny Sydney, Australia, one of the world's most liveable cities.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">We are offering a two-year postdoctoral researcher position that would allow you to join</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">us in Sydney, move things forward, and have a global impact.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" 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</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">the verification of systems components around seL4. Potential PhD topics include</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">designing and implementing new domain-specific programming languages extending</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Cogent, writing formal specifications and proofs in Isabelle/HOL, developing formally</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">verified infrastructure for building secure systems on top of seL4, contributing to</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">improved proof automation and reasoning techniques, and applying formal proof to</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">real-world systems and tools.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">To apply you should have (or be about to obtain) a PhD degree in Computer Science,</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Mathematics, or similar.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">You should also possess a significant subset of the following skills:</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- functional programming in a language like Haskell, ML, or OCaml</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- first-order or higher-order formal logic</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- basic experience in C</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- ability and desire to quickly learn new techniques</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- ability and desire to work in a larger team</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">If you additionally have experience</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- in software verification with an interactive theorem prover such as</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><span style="position: static !important; margin: 0px !important; padding: 0px !important; opacity: 1 !important; float: inherit !important; font-family: inherit !important; font-size: inherit !important; font-style: inherit !important; font-variant-caps: inherit !important; font-stretch: inherit !important; line-height: inherit !important;"> Isabelle/HOL, HOL4, Coq, or <span style="background-image: -webkit-gradient(linear, 0% 0%, 0% 100%, from(rgba(255, 255, 0, 0.498039)), to(rgba(255, 255, 0, 0.498039))) !important; position: static !important; margin: 0px !important; padding: 0px !important; opacity: 1 !important; float: inherit !important; font-family: inherit !important; font-size: inherit !important; font-style: inherit !important; font-variant-caps: inherit !important; font-stretch: inherit !important; line-height: inherit !important;">Agda</span>, and/or</span></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- with programming languages and verified or certifying compilers</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">you should definitely apply!</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">You will work with a unique world-leading combination of OS and formal methods</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">experts, students at undergraduate and PhD level, engineers, and researchers from</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">5 continents, speaking over 15 languages.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Trustworthy Systems is a fun, creative, and welcoming workplace with flexible</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">hours & work arrangements.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">We value diversity in all forms and welcome applications from people of all ages,</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">including people with disabilities, and those who identify as LGBTIQ. See</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><a href="https://ts.data61.csiro.au/diversity/" class="" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">https://ts.data61.csiro.au/diversity/</a> for more information.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">For applying, use the following link:</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><a href="http://external-careers.jobs.unsw.edu.au/cw/en/job/497074/postdoctoral-fellow-computer-programming" class="" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">http://external-careers.jobs.unsw.edu.au/cw/en/job/497074/postdoctoral-fellow-computer-programming</a></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">-Salary range depending on experience and qualifications: </div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"> $95,449 - $102,091 (AUD) + 17% superannuation (retirement funds)</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- 2-year fixed term contract</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- the start date is negotiable</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">- flexible hours and work arrangements</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">This round of applications closes on the <b class=""><a href="http://airmail.calendar/2019-07-13%2023:50:00%20AEST" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">13th of July 2019, 11:50pm</a> AEST</b>.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">For any questions on this position, please contact Christine Rizkallah </div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><<a href="mailto:c.rizkallah@unsw.edu.au" class="" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">c.rizkallah@unsw.edu.au</a>></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">The seL4 code and proof, and the Cogent project, are open source.</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Check them out at <a href="https://sel4.systems/" class="" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">https://seL4.systems</a> and </div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><a href="https://ts.data61.csiro.au/projects/TS/cogent.pml" class="" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">https://ts.data61.csiro.au/projects/TS/cogent.pml</a></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">More information about the Trustworthy Systems team at</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><a href="https://ts.data61.csiro.au/" class="" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">https://ts.data61.csiro.au</a></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><br class=""></div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;">Still studying? We also have internship opportunities!</div><div class="" style="font-family: "helvetica Neue", helvetica; font-size: 14px;"><a href="https://ts.data61.csiro.au/students/" class="" style="overflow-wrap: break-word; word-wrap: break-word; word-break: break-word; -webkit-hyphens: auto;">https://ts.data61.csiro.au/students/</a></div><div><br></div></div><br><div class="gmail_signature"></div></body></html>