MARCH | Mitchell Buckley

Tell us a bit about yourself?
I studied pure mathematics at Macquarie University in Sydney (‘11 to ‘14) and was a post-doctoral fellow at ULB in Brussels (‘15 to ’18). My research was focussed on category theory: finding new ways to see old problems and pulling together existing results to build unified theories. I love pulling a problem apart into many pieces so that I can clearly understand how the different parts interact and develop an elegant solution that cuts to the heart of the issue.

What gets you excited about your work/projects?
Our software analysis is so detailed that we consider what will happen when the computer’s internal clock counts past 2^64. In practice, a computer would need to run for hundreds of years (without a restart) before this happened, but our mathematical model forces us to account for this possibility. And this is just one example of what our proofs must consider! It’s exciting to establish the trustworthiness of software (seL4) in such extreme detail.

What are your qualifications?
PhD

What are your top 3 professional areas?
Software verification, mathematics (pure and applied)

What are your top 3 skills?
1. Formal verification of software (source and binary).
2. Mathematical analysis of software systems for safety and security.
3. Developing software design improvements to safeguard against programmer error and hidden bugs.

Do you have any links you would like to share?
https://orcid.org/0000-0003-0665-9749

Why do you like working at CSIRO's Data61?
Working at Data61 gives me the opportunity to look deeply into difficult problems and learn from world-class scientists while also contributing to safe, secure and trustworthy software systems.