Skip to main content

Quick links: Ex-TS members Research and Engineering Leaders, Researchers, Engineers, Visitors, Support

Research and Engineering Leaders

Corey Lewis Corey Lewis Senior Research Engineer

Corey is a senior proof engineer within the Trustworthy Systems group and is currently the lead engineer for verifying multi-core seL4. During his time at TS he has been involved in a wide variety of projects to do with seL4. These include developing the original CapDL translation tools, helping complete the information flow proofs, and contributing to the verification of the seL4 MCS extensions. His research interests include formal methods, functional programming, and program verification.

Gernot Heiser Gernot Heiser Chief Research Scientist; Scientia Professor and John Lions Chair, UNSW

Gernot's main research interests are in operating systems, especially microkernel-based systems, and their use in embedded/cyber-physical systems, OS security and robustness issues, general cyber-security, energy/power management, real-time systems, virtualization and architectural support for operating systems.

Ihor Kuz Ihor Kuz Principal Research Engineer; Conjoint Associate Professor, UNSW

Ihor's research interests include operating systems and distributed systems. With regards to operating systems, he focuses on the design of flexible and modular operating systems, as well as security and safety properties of such systems. In distributed systems, he is interested in distributed system middleware, supporting services, and management of distributed resources.

Kevin Elphinstone Kevin Elphinstone Principal Researcher; Associate Professor, UNSW

Small operating system kernels and the infrastructure required to support larger systems upon them. His current focus includes secure embedded operating systems suitable for formal verification, and for being the basis of secure systems for embedded devices. He also has interests in componentised operating systems, operating systems in general, security, real-time systems, computer architecture as it pertains to operating systems, and virtualisation.

Michael Norrish Michael Norrish Principal Researcher; Associate Professor, ANU

Michael is interested in the use of mathematics and logic to help in the specification and development of computer hardware and software. He is interested both in working on specific applications projects in this area, and in the development of tools to make all such projects easier to work on.

Yuval Yarom Researcher; Senior Lecturer, UofA

Yuval's main research interests are computer security and cryptography, with a current focus on microarchitectural attacks and defences.


Ambroise Lafont Ambroise Lafont Research Scientist; Postdoctorall fellow

Ambroise is working on the Cogent project.

Carroll Morgan Carroll Morgan Senior Principal Researcher; Professor, UNSW

Formal methods; semantics; security; program correctness; probability.

Christine Rizkallah Christine Rizkallah Researcher; Lecturer, UNSW

Christine is interested in Higher-Order Logic, - Interactive Theorem Proving, and Formal Verification. She works primarily on the Cogent project.

Johannes Åman Pohjola Johannes Åman Pohjola Research Scientist; Conjoint Lecturer, UNSW

Johannes is interested in beauty and truth. Specifically, he works on interactive theorem proving, program verification and concurrency theory.

Rob van Glabbeek Rob van Glabbeek Chief Research Scientist; Conjoint Professor, UNSW

Rob strives to create and study comprehensive models and theories of concurrent processes, thereby answering fundamental questions such as: which problems can be solved in a distributed way, using only asynchronous communication, and which cannot. These insights are applied to the modelling, verification and analysis of distributed systems, in particular to popular routing protocols in wireless mesh networks.

Scott Buckley Scott Buckley Research Scientist; Postdoctoral Fellow, UNSW

Scott works in the time protection team.


Amirreza Zarrabi Amirreza Zarrabi Proof Engineer

Amir is researching operating system architecture, and multiserver architectures for OS design. He is currently on a break from his PhD to work as a proof engineer.

Curtis Millar Curtis Millar OS Engineer; Casual Academic, UNSW

Curtis is interested in improving systems level security through advancements in platform architecture, tooling, and education.

Damon Lee Damon Lee OS Engineer

Damon is interested in operating systems, hardware, and the relationships between the two.

Matthew Brecknell Matthew Brecknell Proof Engineer

Matthew is interested in formal verification of software, using mechanised theorem provers. His current challenge is figuring out how to rapidly, yet sustainably evolve large bodies of existing proofs to meet new requirements.

Michael McInerney Proof Engineer

Michael is learning the techniques to become a proof engineer.

Miki Tanaka Miki Tanaka Senior Research Engineer

Miki is mainly interested in formal verification techniques and their application to software systems.

Milad Ketab Ghale Haji Ali Milad Ketab Ghale Haji Ali Proof Engineer

Long ago Milad divorced the mysterious TRUTH and sided with proof-objects. He became mindful of practicality as much as the correctness. After his PhD at ANU, he join TS doing proof engineering where he can practice the best of formal method techniques and tools for the sake of both the correctness and practicality.

Currently, his work concerns the CASE project where he is validating a translation of seL4 system initializer from its Isabelle specification into CakeML language..

Mitchell Buckley Mitchell Buckley Proof Engineer

Mitchell has a formal education in mathematics and a research background in category theory, Hopf algebra and formalised mathematics. He now writes proofs that verify functional correctness of the seL4 micro-kernel.

Siwei Zhuang Siwei Zhuang Research Engineer

Operating System internals, Device drivers and Embedded System Architecture.

Sylvain Gauthier OS Engineer

Sylvain is interested in working on and understanding UNIX systems and operating systems Kernels.

Victor Phan Proof Engineer

Formal verification.

Vincent Jackson Vincent Jackson Proof Engineer; Graduate Verification Engineer, UNSW

Vincent is interested in proof theory, type theory, and theorem proving.

Zilin Chen Zilin Chen Research Engineer; UNSW

Zilin's research is into functional programming, type theory, formal verification, compilers, and Embedded DSLs.

Zoltan Kocsis Zoltan Kocsis Proof Engineer

Zoltan, a non-standard analyst by training, works on the correctness proof for the seL4 kernel.


Robert Sison Robert Sison Research Scientist; Research Fellow, University of Melbourne

Robert is broadly interested in discovering how best to design and construct software systems with formally proved functional-correctness and security properties at scale. His current research concerns the formal verification of operating systems to enforce increasingly useful forms of information-flow security, also known as confidentiality.


Birgit Brecknell Birgit Brecknell Project Manager

Birgit works part time with the TS group as project manager for strategic and external projects