| 9:00 - 9:15 | Arrival and coffee |
| 9:15 | Start |
| 9:15 - 9:30 | Welcome and opening remarks |
| 9:30 - 10:00 | Formalizing Information Flow in a Haskell Hypervisor Rebekah Leslie, Portland State University; Levent Erkok and Flemming Andersen, Intel Corporation. |
| 10:00 - 10:30 | High-Performance Microkernels and Virtualisation on ARM and
Segmented Architectures Carl van Schaik, Open Kernel Labs; and Gernot Heiser, Open Kernel Labs, National ICT Australia and University of New South Wales. |
| 10:30 - 11:00 | Break (tea and coffee) |
| 11:00 - 11:30 | Automated Object Layout Optimization in a Portable
Microkernel Uwe Dannowski, Universität Karlsruhe. |
| 11:30 - 12:00 | A Memory Allocation Model For An Embedded Microkernel Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone, National ICT Australia and University of New South Wales. |
| 12:00 - 13:30 | Lunch |
| 13:30 - 14:00 | L4-Based Real Virtual Machines: An API Proposal Sebastian Biemueller and Uwe Dannowski, Universität Karlsruhe. |
| 14:00 - 14:30 | A declarative approach to extensible interface
compilation Nicholas FitzRoy-Dale, National ICT Australia and University of New south Wales. |
| 14:30 - 15:00 | Break (tea and coffee) |
| 15:00 - 15:30 | Guest Speaker Introduction to the INTEGRITY Capability System David Kleidermacher, Green Hills Software. |
| 15:30 - 16:00 | Evolution of the PikeOS Microkernel Robert Kaiser, SYSGO AG and Fachhochschule Wiesbaden; and Stephan Wagner, SYSGO AG. |
| 16:00 - 16:30 | Issues on Analysing L4 for its WCET Mohit Singal, IIT Guwahati; and Stefan Markus Petters, National ICT Australia and University of New South Wales |
| 16:30 - 16:45 | Break |
| 16:45 - 17:30 | Panel |
| 17:30 - 17:45 | Closing |
A copy of the proceedings will be made available at the workshop.