
Adrian Danis Senior Research Engineer 
Adrian is interested in the development of operating systems, especially when it involves microkernels, Intel architecture and virtualization. 


Anna Lyons Research Engineer 
Anna is a PHD student working on converting seL4 to a realtime operating system for mixedcriticality systems. An example of a mixedcriticality system is a autonomous helicopter. To do this, seL4 requires a realtime scheduler with mixedcriticality support, a realtime API, primitives for trusted realtime locking, and capabilities for managing CPU time. 


Corey Lewis Research Engineer 
Corey's research interests include formal methods, functional programming and program verification. He is also interested in mathematically analysing graph models of large real world networks. 


Daniel Matichuk Research Engineer 
Daniel is interested in interactive theorem provers and proof automation. His current work is in increasing the scalability and maintainability of formal machinechecked proofs through refactoring. 


Ihor Kuz Senior Research Engineer; Conjoint Senior Lecturer, 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. 


Japheth Lim Proof Engineer 
Japheth is interested in programming languages for trustworthy systems. 


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 Research Engineer 
Kent is mostly concerned with lowlevel operating systems and drivers. 


Kofi Doku Atuah OS Engineer 
Microkernels, Drivers, Scalability, Realtime. Kofi cares about coordinating the currently disjoint world of drivers, and unifying the Free and Open Source world and strengthening opensource Operating Systems' ability to work with hardware vendors to get the drivers they need. 


Maksym Bortin Proof Engineer 
formal software development,
software verification,
formal reasoning 


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. 


Miki Tanaka Senior Research Engineer 
Miki is mainly interested in formal verification techniques and their application to software systems. 


Pang Luo Proof Engineer 
Pang's interests include formal verification and software engineering. 


Partha Susarla Ajay OS Engineer 
Partha's research interests include Operating Systems, File Systems, Multimedia codecs and Distributed computing. 


Peter Chubb Principal Research Engineer; Adjunct Senior Lecturer, UNSW 
Peter's research interests include operating system algorithms for scalability, including storage, scheduling, memory management, and locking. He is also interested in systems performance measurement and optimisation. His main expertise is in Unix and Linux kernels, and low level system support built on these.



Rafal Kolanski Senior Research Engineer 
Rafal is interested in the formal verification of high assurance, systemlevel software, both from the perspective of verification in practice, but also proof maintenance and increasing the proof coverage of already verified systems. 


Seb Holzapfel Research Assistant 
Sebastian is interested in low level & embedded systems, RTOS development & hardware design. 


Sidney Amani Research Engineer 
Sidney's research focuses on finding a practical approach to make file systems amenable to a functional correctness proof formalised in an interactive theorem prover. His previous research includes developing a framework to automatically verify device drivers interactions with the rest of the operating system. 


Siwei Zhuang Research Engineer 
Operating System internals, Device drivers and Embedded System Architecture. 


Thomas Sewell Proof Engineer 
Thomas is interested in program verification, programming languages and operating systems. His PhD thesis is to prove that compilation preserves the properties proved of the source code in projects such as L4.verified. 


Zilin Chen Research Engineer; PhD Student, UNSW 
Functional programming, type theory, compilers, Embedded DSLs. 
