|
Carroll Morgan Professor |
Carroll's research is on formal methods, semantics, security, program correctness and probability. |
|
|
Craig McLaughlin Research Associate |
Craig's research interests include type theory, logic, programming languages, compilers, and formal verification. He presently works on a formal security framework for a provably secure operating system |
|
|
Johannes Åman Pohjola Lecturer |
Johannes is interested in beauty and truth. He works on interactive theorem proving, program verification and concurrency theory, specifically for the Pancake language |
|
|
Kevin Elphinstone Associate Professor |
Kevin works on operating system microkernels 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. |
|
|
Robert Sison Senior Research Associate |
Rob is a postdoctoral researcher who is broadly interested in discovering how best to design and construct software systems with formally proved functional-correctness and security properties at scale. |
|
|
Alex Brown Research Assistant |
Alex is investigating virtIO interfaces on top of the Lions OS |
|
|
Alwin Joshy OS Engineer |
Alwin is working on fast paths in seL4 and on a secure multi-server OS on seL4 |
|
|
Ben Nott Research Assistant |
Ben has deep research interests in formal methods and metamathemtics. Ben is working on Pancake language semantics and program verification. |
|
|
Cheng Li Research Assistant |
Cheng is working on adding persistence to seL4 components. |
|
|
Courtney Darville OS Engineer |
Courtney works on secure multi-server operating system design, and on applying model checking to verify inter-component communication in a highly modular seL4-based OS. |
|
|
Eric Chan Research Assistant |
Eric is working on device virtualisation for the Microkit. |
|
|
Isitha Subasinghe Research Assistant |
Isitha's research interests include Operating Systems, Distributed Systems and Formal Verification. He presently works on verifying OS code using SMT solvers |
|
|
Ivan Velickovic Senior OS Engineer |
Ivan is working on the seL4 Microkit and device driver virtualisation on seL4. |
|
|
James Archer OS Engineer |
James is working to improve the locking in multicore seL4. |
|
|
Jingyao Zhou OS Engineer |
Jingyao is interested in real-time operating systems and hardware. She presently works on device virtualisation for seL4 |
|
|
Junming Zhao Research Engineer |
Junming is interested in memory management and formal methods. She is currently learning about seL4. |
|
|
Krishnan Winter OS Engineer |
Krishnan is working on OS development infrastructure, especially support for profiling. |
|
|
Miki Tanaka Senior Proof Engineer |
Miki is interested in formal verification techniques and their application to software systems, and broadly proof engineering as a discipline. Miki has contributed to the verification of architecture porting for seL4 and also the verification of the seL4 MCS extensions as the technical lead. Miki is currently involved in a project for device driver verification using the Pancake language (based on cakeML/HOL4). |
|
|
Peter Chubb Senior Systems Consultant |
Peter's research interests include operating system abstractions for, intra alia, storage, scheduling, memory management, and locking. He is also interested in capacity planning, and in systems performance measurement and optimisation. His main expertise is in Unix and Linux kernels, and low level system support built on these. He also maintains the Trustworthy Systems website and internal infrastructure. |
|
|
|
Anuraag Ganesh Honours Thesis Student |
Supervised by
Gernot Heiser
|
Anuraag is working on Driver VMs: Re-use of unmodified Linux device drivers in seL4 |
|
|
Dan Shea Honours Thesis Student |
Supervised by
Gernot Heiser
|
Dan is working on adding an IRQ fast path to seL4. |
|
|
Gordon Sau Honours Thesis Student |
Supervised by
Johannes Åman Pohjola
|
Gordon is working on adding support for memory-mapped IO for Pancake. |
|
|
Mathieu Paturel Honours Thesis Student |
Supervised by
Gernot Heiser
|
Mathieu is interested in formal methods, in particular bringing its cost down. He is currently working on verifying user level components built on top of seL4 using SMT solvers. |
|
|
Michael He Honours Thesis Student |
Supervised by
Gernot Heiser
|
Michael is working on adding PD Templates to the seL4 Microkit. |
|
|
Nila Riahi Honours Thesis Student |
Supervised by
Gernot Heiser
|
Nila is working on core management in Lions OS. |
|
|
Temmie Yao Special Project Student |
Supervised by
Gernot Heiser
|
Temmie is working on improving the performance of TCP under seL4. |
|
|
Terry Bai Masters Student |
Supervised by
Gernot Heiser
|
Terry is doing a master's thesis in TS. |
|
|
Adam Stucci Student Intern |
Supervised by
Johannes Åman Pohjola
|
Adam is interested in programming language theory and is working on adding continuations to Pancake. |
|
|
Bill Nguyen Student Intern |
Supervised by
Peter Chubb
|
Bill is working on the Client programming model for Microkit. |
|
|
Charran Kethees Student Intern |
Supervised by
Johannes Åman Pohjola
|
Charran is working on the development and verification of Hoare Logic over interaction trees. |
|
|
Damjan Stevanoski Student Intern |
Supervised by
Peter Chubb
|
Damjan is working on improving VMM performance |
|
|
Halogen Truong Student Intern |
Supervised by
Johannes Åman Pohjola
|
Halogen is working on adding support for multiple entry points in the Pancake compiler stack. |
|
|
James Milosavljevic Student Intern |
Supervised by
Peter Chubb
|
James is a 4th year undergraduate student completing a degree in computer engineering. He is currently working on a project to enable booting virtual machines off disk. |
|
|
Joong Do Chiang Student Intern |
Supervised by
Johannes Åman Pohjola
|
Joong Do is working on a ring buffer library in Pancake. |
|
|
Ken Li Student Intern |
Supervised by
Johannes Åman Pohjola
|
Ken is working on evaluating Pancake by implementing device drivers on top of seL4. |
|
|
Michael Maher Student Intern |
Supervised by
Peter Chubb
|
Michael is working on improving TCP performance for seL4. |
|
|
Ronald Chiang Student Intern |
Supervised by
Johannes Åman Pohjola
|
Ronald is working on connecting interaction trees and state machines for Pancake device drivers. |
|
|
Ryan Shi Student Intern |
Supervised by
Peter Chubb
|
Ryan is assisting in developing a native file system on the seL4 core platform. In one line, Ryan wants to research more in the intersection of maths and CS. Ryan currently is pursuing a Pure Maths major and is exploring the areas of: - Functional Analysis - Topological Spaces - Time Series - Measure Theory In the realm of CS, Ryan has a shallow background in Networking and Data Analysis. Ryan would like to learn more about the following areas: - Haskell / OCaml - Rust - C |
|
|
Thomas Qu Student Intern |
Supervised by
Johannes Åman Pohjola
|
Thomas Qu is interested in type theory and software verification. |
|
|
Xavier Cooney Student Intern |
Supervised by
Gernot Heiser
|
Xavier is working on using SMT solvers for verification. |
|
|
Xianghao Wang Student Intern |
Supervised by
Peter Chubb
|
Xianghao is working on POSIX-style interfaces to seL4 I/O system |
|
|
Corey Lewis Visiting Fellow |
Corey was a senior proof engineer and 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. Corey now works at Proofcraft. |
|
|
Gerwin Klein Adjunct Professor; Founder and Chief Scientist at Proofcraft |
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 Adjunct Professor; Founder and CEO at Proofcraft |
June 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. |
|
|
Michael Norrish Adjunct Associate Professor; 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. Michael now is a Associate Professor at ANU. |
|
|
Rafal Kolanski Adjunct Lecturer; Founder at Proofcraft |
Rafal worked as a proof engineer at Trustworthy Systems until April 2021. He led the Proof Engineering team 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. |
|
|
Zoltan Kocsis Adjunct Lecturer |
Zoltan, a non-standard analyst by training, working on the correctness proof seL4-based OS code. |
|