[CakeML] Researcher and Proof Engineer jobs at Data61 (very CakeML relevant, both!)

Sun Nov 18 10:59:25 UTC 2018

The description for the proof engineer positions follows below that for the Researcher.

- - - - - - - 
Data61 Seeking Research Scientist
=================================

We are looking for a full-time research scientist in formal verification to
join us, the Trustworthy Systems group, at Data61, CSIRO. 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.

Our vision is a world in which computer users can choose all three: correct,
secure, and fast. We believe that most current approaches to building systems
are fundamentally flawed. We aim to demonstrate a better way. Our approach is
rooted in foundational, formal verification using theorem provers (e.g.,
Isabelle, HOL4), and high-performance system design. If you find this vision
appealing, and have ideas about how to pursue it, we want to hear from you.

Our team brings together a unique combination of expertise in systems,
security, formal verification, and programming languages. We are the creators
of seL4, the world's first operating system microkernel with a
machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme performance
and foundational binary-level correctness and security proofs. We are also
involved in CakeML, the most realistic verified compiler for a functional
programming language, and a promising approach to scaling full verification
up to applications code.

We are building on these successes in various directions, including
concurrency (formal reasoning and implementation), timing (real-time
guarantees and timing channels), and whole-system verification using
component systems (e.g., CAmKES) and code+proof co-generation.

We publish in top conferences, and are involved in multiple international
research collaborations. You will have the opportunity to teach at UNSW
should you wish to take it. We have a flexible, friendly, and intellectually
stimulating work environment.

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.

The salary range for this position (plus superannuation) is
- Research Scientist: 97k-105k
- Senior Research Scientist: 111k-130k
depending on experience and qualifications.

Apply online here:
https://jobs.csiro.au/job/Sydney%2C-NSW-Research-ScientistSenior-Research-Scientist-in-Formal-Verification/518430100/

Your application should include a cover letter, CV, short research statement,
and contact information for two references.

This round of applications closes on 15 January 2019.

For any questions on this position, please contact June.Andronick at data61.csiro.au

- - - - - -

Data61 Seeking Proof Engineers

==============================

We are are hiring again!

If only there were 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 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 proof engineers who want to join

our team in Sydney, move things forward, and have global impact. You

would

  - work on industrial-scale formal proofs in Isabelle/HOL

  - develop formally verified infrastructure for building secure systems

    on top of seL4

  - contribute to improved proof automation and 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

We are hiring at two levels, so if you are more qualified or

experienced than the above would suggest, you can come in as a senior

proof engineer.

If you additionally have experience

  - in software verification with an interactive theorem prover such as

    Isabelle/HOL, HOL4, 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

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.

Salary ranges, in AUD (plus superannuation):

- Junior Proof Engineer: 73k-93k

- Senior Proof Engineer: 97k-105k

depending on experience and qualifications.

Apply online at the following link for the Proof Engineer positions:

 - https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/518443000/

 - https://jobs.csiro.au/job/Sydney%2C-NSW-DATA-61/518441000/

Your application should include a cover letter, CV, undergraduate

transcript (if applicable), and contact information for two references.

This round of applications closes on 17 December 2018.

For any questions on these positions, please contact

Rafal.Kolanski at data61.csiro.au

The seL4 code and proof are open source. Check them out at https://seL4.systems

More information about Data61's Trustworthy Systems team at

https://ts.data61.csiro.au

There are additional proof engineering positions available on the

Cogent project. Cogent is a language we designed to ease the

verification of systems components around seL4. For expressions of

interest, see contact details on

https://ts.data61.csiro.au/projects/TS/cogent.pml

Looking to do a PhD?

Data61 and UNSW (https://www.unsw.edu.au/) offer scholarships!

See https://ts.data61.csiro.au/students/research.pml for details.