• Welcome
• Research
  • Past Projects
  • Publications
  • Program Committees
• Students
• Teaching
• Contact

Publications

My Google Scholar Profile.

• Stefan S. Petters, Kevin Elphinstone, and Gernot Heiser. Advances in Real-time Systems, chapter Trustworthy Real-time Systems, pages 191–206. Springer, Heidelberg, Germany, 2012.
• June Andronick, David Greenaway, and Kevin Elphinstone. Towards proving security in the presence of large untrusted components. In Gerwin Klein, Ralf Huuck, and Bastian Schlich, editors, Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October 2010. USENIX.
• Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz, and Leonid Ryzhyk. The road to trustworthy systems. In Proceedings of the 5th Workshop on Scalable Trusted Computing, Chicago, IL, USA, October 2010.
• Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. Communications of the ACM, 53(6):107–115, June 2010.
• Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October 2009. ACM.
• Gerwin Klein, Philip Derrin, and Kevin Elphinstone. Experience report: seL4 — formally verifying a high-performance microkernel. In Proceedings of the 14th International Conference on Functional Programming, Glasgow, UK, August 2009.
• Stefan M. Petters, Martin Lawitzky, Ryan Heffernan, and Kevin Elphinstone. Towards real multi-criticality scheduling. In Proceedings of the 15th IEEE Conference on Embedded and Real-Time Computing and Applications, Beijing, China, August 2009.
• Dhammika Elkaduwe, Gerwin Klein, and Kevin Elphinstone. Verified protection model of the seL4 microkernel. In Jim Woodcock and Natarajan Shankar, editors, VSTTE 2008 — Verified Softw.: Theories, Tools & Experiments, Lecture Notes in Computer Science, Toronto, Canada, October 2008. Springer.
• Dhammika Elkaduwe, Philip Derrin, and Kevin Elphinstone. Kernel design for isolation and assurance of physical memory. In Proc. 1st Workshop on Isolation and Integration in Embedded Systems, Glasgow, UK, April 2008. (PDF, 131425 bytes)
• Kevin Elphinstone, David Greenaway, and Sergio Ruocco. Lazy scheduling and direct process switch — merit or myths? In Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications, Pisa, Italy, July 2007. (PDF, 247564 bytes)
• Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein, and Stefan M. Petters. Towards trustworthy computing systems: Taking microkernels to the next level. Operating Systems Review, 41(4):3–11, July 2007.
• Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, and Gernot Heiser. Towards a practical, verified kernel. In Proc. 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May 2007. (PDF, 107509 bytes)
• Timothy Roscoe, Kevin Elphinstone, and Gernot Heiser. Hype and virtue. In Proc. 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May 2007. (PDF, 70629 bytes)
• Dhammika Elkaduwe, Philip Derrin, and Kevin Elphinstone. A memory allocation model for an embedded microkernel. In Proc. 1st International Workshop on Microkernels for Embedded Systems, pages 28–34, Sydney, Australia, January 2007. NICTA. (PDF, 82374 bytes)
• Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. Running the manual: An approach to high-assurance microkernel development. In Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, Oregon, USA, September 2006. (PDF, 276235 bytes)
• Kevin Elphinstone, Gerwin Klein, and Rafal Kolanski. Formalising a high-performance microkernel. In Rustan Leino, editor, Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Microsoft Research Technical Report MSR-TR-2006-117, pages 1–7, Seattle, USA, August 2006. (PDF, 239322 bytes)
• Dhammika Elkaduwe, Philip Derrin, and Kevin Elphinstone. Kernel data – first class citizens of the system. In Proceedings of the 2nd International Workshop on Object Systems and Software Architectures, pages 39–43, Victor Harbor, South Australia, Australia, January 2006. (PDF, 43123 bytes)
• Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters, and Sergio Ruocco. L4cars. In Embedded Security in Cars (escar 2005) Workshop, Cologne, Germany, November 2005. (PDF, 110083 bytes)
• Ben Leslie, Peter Chubb, Nicholas Fitzroy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone, and Gernot Heiser. User-level device drivers: Achieved performance. Journal of Computer Science and Technology, 20(5):654–664, September 2005.
• Kevin Elphinstone. Future directions in the evolution of the l4 microkernel. In Gerwin Klein, editor, Proc. NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October 2004. National ICT Australia. (PDF, 133462 bytes)
• Kevin Elphinstone and Stefan Götz. Initial evaluation of a user-level device driver framework. In P. Yew and J. Xue, editors, Advances in Computer Systems Architecture, Proc. 9th Asia-Pacific Conference, ACSAC'04, Lecture Notes in Computer Science, volume 3189, Beijing, China, September 2004. (PDF, 163450 bytes)
• Andreas Haeberlen and Kevin Elphinstone. User-level management of kernel memory. In Advances in Computer System Architecture (Proc. ACSAC'03), Lecture Notes in Computer Science, volume 2823. Springer-Verlag, October 2003. (PDF, 160840 bytes)
• J. Liedtke, U. Dannowski, K. Elphinstone, G. Liefländer, E. Skoglund, V. Uhlig, C. Ceelen, A. Haeberlen, and M. Völp. The L4Ka Vision. Available: http://l4ka.org/, April 2001. (PDF, 81378 bytes)
• Mohit Aron, Jochen Liedtke, Yoonho Park, Luke Deller, Kevin Elphinstone, and Trent Jaeger. The SawMill framework for virtual memory diversity. In Australasian Computer Systems Architecture Conference, Gold Coast, Australia, January 2001. IEEE Computer Society Press. (PDF, 57494 bytes)
• A. Gefflaut, T. Jaeger, Y. Park, J. Liedtke, K. Elphinstone, V. Uhlig, J.E. Tidswell, L. Deller, and L. Reuther. The SawMill multiserver approach. In 9th SIGOPS European Workshop, Kolding, Denmark, September 2000.
• T. Jaeger, J.E. Tidswell, A. Gefflaut, Y. Park, J. Liedtke, and K. Elphinstone. Synchronous IPC over transparent monitors. In 9th SIGOPS European Workshop, Kolding, Denmark, September 2000.
• J. Liedtke, M. Völp, and K. Elphinstone. Preliminary thoughts on memory-bus scheduling. In 9th SIGOPS European Workshop, Kolding, Denmark, September 2000.
• Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko, and Yoonho Park. Flexible access control using IPC redirection. In 7th Workshop on Hot Topics in Operating Systems, Rio Rico, Arizona, March 1999.
• J. Liedtke, V. Uhlig, K. Elphinstone, T. Jaeger, and Y. Park. How to schedule unlimited memory pinning of untrusted processes or provisional ideas about service-neutrality. In 7th Workshop on Hot Topics in Operating Systems, Rio Rico, Arizona, March 1999.
• K. Elphinstone, G. Heiser, and J. Liedtke. Page tables for 64-bit computer systems. In John Morris, editor, Australasian Computer Architecture Conference, Auckland New Zealand, January 1999. Springer Verlag, Singapore.
• Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell, and Jochen Liedtke. The Mungi single-address-space operating system. Software Practice and Experience, 28(9), July 1998.
• K. Elphinstone, G. Heiser, and J. Liedtke. L4 reference manual – MIPS R4x00, version 1.0, kernel version 70. Technical Report UNSW-CSE-TR-9709, School of Computer Science and Engineering, University of New South Wales, 1997.
• K. Elphinstone, S. Russell, G. Heiser, and J. Liedtke. Supporting persistent object systems in a single address space. In Proc. 7th Int'l Workshop on Persistent Object Systems, Cape May, 1997.
• G. Heiser, J. Vochteloo, K. Elphinstone, and S. Russell. The Mungi kernel API, release 1.0. Technical Report UNSW-CSE-TR-9701, School of Computer Science and Engineering, University of New South Wales, 1997.
• Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell, and Jochen Liedtke. Implementation and performance of the Mungi single-address-space operating system. Technical Report UNSW-CSE-TR-9704, University of NSW, June 1997.
• Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Hermann Härtig, Gernot Heiser, Nayeem Islam, and Trent Jaeger. Achieved IPC performance. In 6th Workshop on Hot Topics in Operating Systems (HotOS), Chatham, Massachusetts, May 1997.
• Jerry Vochteloo, Kevin Elphinstone, Stephen Russell, and Gernot Heiser. Protection domain extensions in Mungi. In Proc. 5th Int'l Workshop on Object Orientation in Operating Systems, Seattle, WA, USA, October 1996.
• J. Liedtke and K. Elphinstone. Guarded page tables on the MIPS R4600 or an exercise in architecture-dependent micro optimization. Operating Systems Review, January 1996.
• Jochen Liedtke and Kevin Elphinstone. Guarded page tables on the MIPS R4600. Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, University of New South Wales, November 1995.
• Kevin Elphinstone, Stephen Russell, and Gernot Heiser. Issues in implementing virtual memory. Technical Report UNSW-CSE-TR-9411, Shool of Computer Science and Engineering, University of New South Wales, 1994.
• G. Heiser, K. Elphinstone, S. Russell, and J. Vochteloo. Mungi: A distributed single address-space operating system. In Proc. 17th Australasian Computer Science Conference, Christchurch, New Zealand, January 1994.
• Kevin Elphinstone. Address space management issues in the Mungi operating system. Technical Report 9312, School of Computer Science and Engineering, University of New South Wales, November 1993.
• G. Heiser, K. Elphinstone, S. Russell, and G. Hellestrand. A distributed single address-space operating system supporting persistence. Technical Report UNSW-CSE-TR-9302, School of Computer Science and Engineering, University of New South Wales, March 1993.
• S. Russell, A. Skea, K. Elphinstone, G. Heiser, K. Burston, I. Gorton, and G. Hellestrand. Distribution + Persistence = Global Virtual Memory. In Proc. Int'l Workshop on Object Orientation in Operating Systems, Dourdan, France, 1992. IEEE.