Virtualization is technology for supporting execution of computer program code, from applications to entire operating systems, in a software-controlled environment. Such a Virtual Machine (VM) environment abstracts available system resources...
MEDIA ALERT
Who: Open Kernel Labs; Dr. Gernot Heiser
What: "Operating System Verification for Real Use" Keynote Speaker, VERIFY 2008
When: August 10-11, 2008
Where: 5th International Verification Workshop (VERIFY 2008) Sydney, Australia
Dr. Gernot Heiser will present as a Keynote Speaker at the 5th International Verification Workship (VERIFY 2008) in Sydney, Australia. He will be discussing the work done at NICTA on verifying a complete operating system microkernel aimed for real world deployment and explain the approach taken to ensure that this doesn't remain an academic exercise.
Heiser will address the conflicting goals of verifiability, general applicability and high performance. The kernel, called seL4, is designed to replace commercially-deployed high-performance L4 microkernels with no more than 10% performance degradation. The project, which has been running since early 2004, is scheduled to be completed by the end of this year.
The formal verification of critical information systems has a long tradition as one of the main areas of application for automated theorem proving. Nevertheless, the area is of still growing importance as the number of computers affecting everyday life and the complexity of these systems are both increasing. The purpose of the VERIFY workshop series is to discuss problems arising during the formal modeling and verification of information systems and to investigate suitable solutions. Possible perspectives include those of automated theorem proving, tool support, system engineering, and applications.
The Open Kernel Labs leading technology in embedded systems software and virtualization enables the development of safe, trustworthy and affordable devices. Backed by the largest, independent team of microkernel developers, OK Labs delivers OKL4, an advanced microkernel solution, which offers the highest performance combined with strong protection and security features. OKL4 provides developers with a robust, open source platform for building secure, differentiated embedded applications. For more information about OK Labs and its products visit www.ok-labs.com. OK Labs is a spin out from NICTA, Australia’s preeminent Center of Excellence for Information and Communications Technology, www.nicta.com.au.
Open Kernel Labs, OK Labs and Secure HyperCell are trademarks or registered trademarks of Open Kernel Labs or its affiliates in the U.S. and
other countries. Other names may be trademarks of their respective owners.
###