Email Gateway (Aug 22 2022 at 19:22): Email Gateway (Aug 22 2022 at 19:22):From: Christine Rizkallah <c.rizkallah@unsw.edu.au>
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 scholarships to multiple motivated PhD students who want 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 PhD 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 bachelor degree (minimum 4 years) or
a bachelor and masters degree in Computer Science, Mathematics, or similar.
You should also possess a significant subset of the following skills:
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, and or
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/ for more information.
For applying, email us on <c.rizkallah@unsw.edu.au<mailto:c.rizkallah@unsw.edu.au>> a copy of your CV,
cover letter, transcripts, and contact information for two referees.
This round of applications closes on the 19th of April 2019.
For any questions on these positions, 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 and
https://ts.data61.csiro.au/projects/TS/cogent.pml
More information about the Trustworthy Systems team at
https://ts.data61.csiro.au
Still studying? We also have internship opportunities!
https://ts.data61.csiro.au/students/
Email Gateway (Aug 22 2022 at 20:24):From: Christine Rizkallah <c.rizkallah@unsw.edu.au>
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 scholarships to multiple motivated PhD students who want 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 PhD 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 bachelor degree (minimum 4 years) or
a bachelor and a masters degree in Computer Science, Mathematics, or similar. You should
also meet UNSW's minimum English requirements:
https://www.unsw.edu.au/english-requirements-policy
You should also possess a significant subset of the following skills:
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/ for more information.
For applying, email us on <c.rizkallah@unsw.edu.au> a copy of your CV,
cover letter, transcripts, and contact information for two referees.
This round of applications closes on the 1st of September 2019.
For any questions on these positions, please contact Christine Rizkallah
<c.rizkallah@unsw.edu.au>
The Cogent project is open source.
Check it out at https://ts.data61.csiro.au/projects/TS/cogent.pml
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC