Email Gateway (Aug 22 2022 at 11:26): Email Gateway (Aug 22 2022 at 11:26):From: June Andronick <June.Andronick@nicta.com.au>
[Apologies for multiple copies. Please forward to anyone interested.]
Data61 Seeking Proof Engineers
==============================
(applications close 15 October 2015)
http://ssrg.nicta.com.au/jobs/proof-engineers2015
If only there was a place where I could prove theorems for money, change the
world, and have fun while doing it...
Sounds too good to exist?
In the Trustworthy Systems team at Data61, formerly known as NICTA, 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 looking for multiple motivated entry-level proof engineers who want to
join our team, move things forward, and have global impact. We are expanding
our team, because seL4 is going places. There are active projects around the
world in
- Automotive - because cars have been hacked enough
- Aviation - for more security and safety for autonomous vehicles
- Connected consumer devices - with security built in from the start
- SCADA - for more secure intelligent industrial control automation
- Spaceflight, autonomous and crewed - because awesome
To make these projects successful, we need to scale formal verification.
You would
- work on industrial-scale formal proofs in Isabelle/HOL
- help to extend and improve existing proofs or verify new features in seL4
- contribute to improved proof automation and better reasoning techniques
- apply formal proof to real-world systems and tools
To apply for this position, you should 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
- undergraduate degree in Computer Science, Mathematics, or similar
- 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 or Coq, and/or
- with operating systems and microkernels
you should definitely apply!
If you have the right skills and background, we can provide training on the job.
Continual learning is a central component of everything we do. 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 full health insurance and flexible
hours & work arrangements.
We value diversity in all forms and welcome applications from people
of all ages, including people with a disability, and those who identify as
LGBTIQ. See http://ssrg.nicta.com.au/diversity/ for more information.
The salary range for this position is AUD 65,000 to 90,000 for recent
graduates, depending on experience and qualification.
Apply by sending your CV, undergraduate transcript (if applicable), two
references, and cover letter to <gerwin.klein@nicta.com.au> and
<june.andronick@nicta.com.au>.
This round of applications closes 15 October 2015.
The seL4 code and proof are open source. Check them out at
https://github.com/seL4
More information about NICTA's Trustworthy Systems team at
http://ssrg.nicta.com.au
Still studying? We also have internship opportunities!
http://ssrg.nicta.com.au/students/
Last updated: Nov 21 2024 at 12:39 UTC