Find out how ICT can support biomedical and clinical researchFind out more. Managing complexity by developing new tools and processes. Managing Complexity

The L4.verified project

L4.verified The University of New South Wales

These are the technical project pages. If you are looking for a general overview, please follow this link.

News

The 3rd international Workshop on Systems Software Verification (SSV08) is now accepting submissions.

Creating Trustworthy Software

The L4.verified project is providing a mathematical, machine-checked proof of the functional correctness of the L4 microkernel with respect to a high level, formal description of its expected behaviour.

Embedded systems are vital infrastructure elements in information and communications technology. They drive mobile phones, entertainment devices, cars, toys, appliances, smart cards, medical devices, network switching gear, sensors, industrial robots and many more applications.

A kernel is the central module of a computer's operating system, and a microkernel provides a minimum set of interfaces that are used by the operating system. The L4 high-performance microkernel is at the heart of NICTA's strategy for developing low-cost, reliable software for embedded systems. NICTA aims to develop a model of the kernel that is suitable for formal reasoning about software components to be built on top, and to verify the implementation of the kernel itself.

The Team

Contact

For further information, please contact Gerwin Klein: gerwin.klein(at)nicta.com.au