This is an umbrella project under which a number of PhD projects are available. These are largely concerned with the design, implementation, analysis, formal verification and evaluation of seL4-based operating systems and development frameworks. Specific topics include

  • robust, highly-modular, high-performance I/O systems
  • high-assurance resource management
  • models and frameworks for reasoning about timeliness in mixed-criticality systems
  • systems programming languages that aid verification
  • formal verification of OS components
  • end-to-end security- and safety proofs

This list is not exclusive.


This is a top-up scholarship.

The value will be determined based on the track record (academic and otherwise) of the applicant and the alignment of their research topic to the externally-funded projects, and will be in the range of $10,000 per annum up to the maximum allowed topup rate ($26,250 per annum at present).

Eligibility Criteria

  • Domestic candidates 
  • PhD only

How to apply

Email a copy of CP, academic transcripts, and specific topic interest to Scientia Professor Gernot Heiser at

School / Research Area

Computer Science & Engineering