If only there were a place where I could prove theorems, change the world, and have fun while doing it... Sounds too good to exist? In the Trustworthy Systems team at UNSW and Data61 that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities. We are offering a two-year postdoctoral researcher position that would allow you to join us in Sydney, move things forward, and have a global impact. Cogent is a language we designed that co-generates code and proofs in order to ease the verification of systems components around seL4. Potential topics include designing and implementing new domain-specific programming languages extending Cogent, writing formal specifications and proofs in Isabelle/HOL, developing formally verified infrastructure for building secure systems on top of seL4, contributing to improved proof automation and reasoning techniques, and applying formal proof to real-world systems and tools. To apply you should have (or be about to obtain) a PhD degree in Computer Science, Mathematics, or similar. You should also possess a significant subset of the following skills: - functional programming in a language like Haskell, ML, or OCaml - first-order or higher-order formal logic - basic experience in C - ability and desire to quickly learn new techniques - ability and desire to work in a larger team If you additionally have experience - in software verification with an interactive theorem prover such as Isabelle/HOL, HOL4, Coq, or Agda, and/or - with programming languages and verified or certifying compilers you should definitely apply! You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements. We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See https://ts.data61.csiro.au/diversity/ <https://ts.data61.csiro.au/diversity/> for more information. For applying, use the following link: http://external-careers.jobs.unsw.edu.au/cw/en/job/497074/postdoctoral-fello... <http://external-careers.jobs.unsw.edu.au/cw/en/job/497074/postdoctoral-fellow-computer-programming> -Salary range depending on experience and qualifications: $95,449 - $102,091 (AUD) + 17% superannuation (retirement funds) - 2-year fixed term contract - the start date is negotiable - flexible hours and work arrangements This round of applications closes on the 13th of July 2019, 11:50pm AEST. For any questions on this position, please contact Christine Rizkallah <c.rizkallah@unsw.edu.au <mailto:c.rizkallah@unsw.edu.au>> The seL4 code and proof, and the Cogent project, are open source. Check them out at https://seL4.systems <https://sel4.systems/> and https://ts.data61.csiro.au/projects/TS/cogent.pml <https://ts.data61.csiro.au/projects/TS/cogent.pml> More information about the Trustworthy Systems team at https://ts.data61.csiro.au <https://ts.data61.csiro.au/> Still studying? We also have internship opportunities! https://ts.data61.csiro.au/students/ <https://ts.data61.csiro.au/students/>