Skip to main content


Warning, some of this information may be out of date

Quick links: Research and Engineering Leaders, Engineers, Research Students, Support

Research and Engineering Leaders

Gerwin Klein Gerwin Klein Chief Research Scientist; Conjoint Professor, UNSW

Gerwin has left CSIRO. See his personal web page for contact info.

Gerwin's research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, semantics of programming languages, and in the emerging field of proof engineering. Generally, he wants software systems to be dependable, and thinks that formal specification and proof can make a significant contribution towards that goal.

June Andronick June Andronick Chief Research Scientist; Conjoint Professor, UNSW

June has left CSIRO's Data61 in April 2021. She had joined the Trustworthy Systems research group in 2008 (in NICTA), and led the group from end of 2016 to end of 2020. Her main research interest is in formal verification and certification of software systems, more precisely in formal proof of correctness and security properties of programs using interactive theorem proving, as well as concurrency reasoning, targeting interruptible and multicore systems.

Rafal Kolanski Rafal Kolanski Proof Engineer

Rafal worked as a proof engineer at Data61 until April 2021. He led the Proof Engineering team at Trustworthy Systems from 2016 until 2021.

Rafal is interested in the formal verification of high assurance, system-level software, both from the perspective of verification in practice, but also proof maintenance and increasing the proof coverage of already verified systems.


Anna Lyons Anna Lyons Senior Research Engineer

Anna was a senior engineer on the seL4 team, taking the role after completing her PhD on the mixed-criticality API and design for seL4. Anna is dedicated to bringing seL4 to the world, by building a strong team of engineers who together build a great platform and community. Anna left Trustworthy Systems in June 2019 to join Ghost Locomotion

Chi Kam Chi Kam Research Assistant

Felix's research interests include operating system design, embedded systems in general and formal methods, particularly interactive theorem proving.

Hesham Almatary OS Engineer

Hesham left the TS group in 2018 to go to Cambridge University for further study. His work while here, and before joining the group, was mostly around the RISC-V port of seL4.

Joel Beeren Joel Beeren Research Engineer

Joel's research interests include the application of formal mathematical principles (especially number theoretic concepts) to computing design, as well as the use of formal methods in operating systems.

Kent Mcleod Kent Mcleod Research Engineer

Kent left TS to work for a startup in July 2020.

Shanush Prema Thasarathan Shanush Prema Thasarathan Intern; Undergraduate @ UNSW - BE ME Electrical Engineering

Xin Gao Xin Gao Research Engineer

symbolic computation and fourier analysis.

Yutaka Nagashima Research Assistant

Yutaka's research interests include proof assistants and proof automation.

Research Students

Aaron Carroll Aaron Carroll PhD Student
Supervised by Gernot Heiser

Aaron works on smartphone energy management, and is primarily interested in how multi-core applications processors can be used to reduce energy consumption when combined with well-established techniques such as frequency/voltage scaling. He also works on understanding how energy is consumed within smartphones, using physical instrumentation and measurement on real-world devices. Recently, Aaron has been exploring techniques which exploit multi-core CPUs to improve sequential performance.

Mohammad Abdulaziz Mohammad Abdulaziz PhD Student
Supervised by Michael Norrish

I am interested in Interactive theorem proving. My PhD project is about mechanizing optimality properties in SAT based planning algorithms.


Peter Chubb Peter Chubb Principal Research Engineer; Conjoint Senior Lecturer, UNSW

Peter's research interests include operating system abstractions for, intra alia, storage, scheduling, memory management, and locking. He is also interested in capacity planning, systems performance measurement and optimisation. His main expertise is in Unix and Linux kernels, and low level system support built on these. He also maintained the Trustworthy Systems website and internal infrastructure.