Trustworthy Systems

Paper/Talk Abstract		Paper in PDF format
Presentation slides		Video of the presentation
A reference to a location		Paper yet to be published

Publications related to Operating Systems @ SSRG

2024

Peter Chubb Running your own mailserver Everything Open, Gladstone, QLD, AU, April, 2024

2023

		Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus Myreen, Michael Norrish and Gernot Heiser Pancake: verified systems programming made sweeter Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023
		Gernot Heiser The seL4 microkernel: Provable security for the real world Keynote at the International Workshop on Advanced Industrial Science and Technology, September, 2023
		Lucy Parker The seL4 device driver framework Talk at the 5th seL4 Summit, September, 2023
		Ivan Velickovic The seL4 Microkit Talk at the 5th seL4 Summit, September, 2023
		Mathieu Paturel, Isitha Subasinghe and Gernot Heiser First steps in verifying the seL4 Core Platform Asia-Pacific Workshop on Systems (APSys), Seoul, KR, August, 2023
		Gernot Heiser Intelligent vehicle security needs a verified operating system Keynote at the International Workshop on Safety and Security of Intelligent Vehicles, June, 2023
		Gernot Heiser seL4 update: Foundation and TS R&D news Invited talk at the Trusted Computing Center of Excellence 2023 Summit, May, 2023
		Jason Belt, John Hatcliff, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren Cofer, David Hardin, Karl Hoech, Konrad Slind, Ihor Kuz and Kent Mcleod Model-driven development for the seL4 microkernel using the HAMR framework Journal of Systems Architecture, Volume 134, pp. 102789, 2023
		Gernot Heiser R&D update from Trustworthy Systems Talk at the 5th seL4 Summit, 2023

2022

		Gernot Heiser, Lucy Parker, Ivan Velickovic, Peter Chubb and Ben Leslie Can we put the "S" into IoT? IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022
		Gernot Heiser State of seL4-related research Keynote at the seL4 Summit, October, 2022
		Gernot Heiser seL4 overview: Principles, abstractions, use Invited talk at the seL4 Summit, October, 2022
		Lucy Parker The seL4 device driver framework Talk at the 4th seL4 Summit, October, 2022
		Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer and John Shackleton Cyberassured systems engineering at scale IEEE Security and Privacy, Volume 20, Number 3, pp. 52–64, March, 2022
		Gernot Heiser The seL4 report: State of the seL4 ecosystem Keynote at the Trusted Computing Center of Excellence 2022 Summit, February, 2022
		Gernot Heiser The seL4 Foundation – growing through upheaval On-line, January, 2022

2020

		Gernot Heiser The formally verified seL4 microkernel – a high-assurance foundation for MCS Keynote at IEEE Conference on Embedded and Real-Time Computing and Applications, August, 2020
		Gernot Heiser, Toby Murray and Gerwin Klein Towards provable timing-channel prevention ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020
		Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser Prevention of microarchitectural covert channels on an open-source 64-bit RISC-V core Workshop on Computer Architecture Research with RISC-V (CARRV), Valencia, Spain, May, 2020
		Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020
		Gernot Heiser Verified seL4 on secure RISC-V processors at linux.conf.au, Gold Coast, January, 2020

2019

		Yanyan Shen, Gernot Heiser and Kevin Elphinstone Fault tolerance through redundant execution on COTS multicores: Exploring trade-offs International Conference on Dependable Systems and Networks (DSN), pp. 188-200, Portland, Oregon, USA, June, 2019
		Gernot Heiser, Gerwin Klein and Toby Murray Can we prove time protection? Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019
		Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award
		Yanyan Shen Microkernel mechanisms for improving the trustworthiness of commodity hardware PhD Thesis, UNSW, Sydney, Australia, March, 2019
		Gernot Heiser What's new in the world of seL4? Talk at FOSDEM'19, Brussels, February, 2019

2018

		Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart A formal approach to constructing secure air vehicle software IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018
		Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez Formally verified software in the real world Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
		Simon Biggs, Damon Lee and Gernot Heiser The jury is in: Monolithic OS design is flawed Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018
		Gernot Heiser The quest for the perfect API Invited "Fireside Talk" at VMware on occasion of the virtualisation pioneer's 20th anniversary, April, 2018
		Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time EuroSys Conference, Porto, Portugal, April, 2018
		Gernot Heiser For safety's sake: we need a new hardware-software contract! IEEE Design and Test, Volume 35, Issue 2, pp. 27-30, March, 2018
		Gernot Heiser Flying autonomous aircraft: Mixed-criticality support in seL4 at linux.conf.au, Sydney, January, 2018
		Anna Lyons Mixed-criticality scheduling and resource sharing for high-assurance operating systems PhD Thesis, UNSW, 2018

2017

		Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson Secure mathematically-assured composition of control models Technical Report, Data61, CSIRO, September, 2017
		Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser A performance evaluation of rump kernels as a multi-server OS building block on seL4 Asia-Pacific Workshop on Systems (APSys), India, September, 2017
		Thomas Sewell, Felix Kam and Gernot Heiser High-assurance timing analysis for a high-assurance real-time OS Real-Time Systems, Volume 53, Issue 5, pp. 812-853, September, 2017
		Aaron Carroll Understanding and reducing smartphone energy consumption PhD Thesis, UNSW, Sydney, Australia, May, 2017
		Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, 2017

2016

		Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016
		Gernot Heiser and Kevin Elphinstone L4 microkernels: The lessons from 20 years of research and deployment ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
		Thomas Sewell, Chi Kam and Gernot Heiser Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016 Outstanding Paper award

2015

		Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach From non-preemptive to preemptive scheduling using synchronization synthesis International Conference on Computer Aided Verification, San Francisco, USA, July, 2015
		Sean Peters, Adrian Danis, Kevin Elphinstone and Gernot Heiser For a microkernel, a big lock is fine Asia-Pacific Workshop on Systems (APSys), Tokyo, JP, July, 2015
		Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk SAT-based strategy extraction in reachability games AAAI, Austin, TX, USA, January, 2015

2014

		Anna Lyons and Gernot Heiser Mixed-criticality support in a high-assurance, general-purpose microkernel Workshop on Mixed Criticality Systems, pp. 9–14, Rome, Italy, December, 2014
		Matthias Daum, Nelson Billing and Gerwin Klein Concerned with the unprivileged: User programs in kernel refinement Formal Aspects of Computing, Volume 26, Number 6, pp. 1205–1229, October, 2014
		Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm and Mona Vij User-guided device driver synthesis USENIX Symposium on Operating Systems Design and Implementation, pp. 661–676, Broomfield, CO, USA, October, 2014
		Adam Christopher Walker and Leonid Ryzhyk Predicate abstraction for reactive synthesis Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014
		Adam Christopher Walker and Leonid Ryzhyk Predicate abstraction for reactive synthesis Technical Report NRL-8281, NICTA, August, 2014
		Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach Regression-free synthesis for concurrency International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
		Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk Interpolants in two-player games Abstract, iPRA workshop, July, 2014.
		Alexander Legg, Nina Narodytska and Leonid Ryzhyk Practical CNF interpolants via BDDs Abstract, iPRA workshop, July, 2014.
		Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Christopher Walker Solving games without controllable predecessor International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
		Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu Automatic verification of active device drivers ACM Operating Systems Review, Volume 48, Number 1, May, 2014
		Bernard Blackham, Mark Liffiton and Gernot Heiser Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 169–178, Berlin, Germany, April, 2014
		Aaron Carroll and Gernot Heiser Unifying DVFS and offlining in mobile multicores IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 287–296, Berlin, Germany, April, 2014
		Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014

2013

		Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Christopher Walker and Alexander Legg Device driver synthesis Intel Technology Journal, Volume 17, Number 2, pp. 136–157, December, 2013
		Michael von Tessin The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2013
		Aaron Carroll and Gernot Heiser Mobile multicores: Use them or waste them Workshop on Power Aware Computing and Systems, pp. 5, Farmington, PA, USA, November, 2013 A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 44-48.
		Kevin Elphinstone and Gernot Heiser From L3 to seL4 – what have we learnt in 20 years of L4 microkernels? ACM Symposium on Operating Systems Principles, pp. 133–150, Farmington, PA, USA, November, 2013
		Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013
		Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick Towards a verified component platform Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
		Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013
		Bernard Blackham Towards verified microkernels for real-time mixed-criticality systems PhD Thesis, UNSW, Sydney, Australia, October, 2013 2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation
		Aaron Carroll and Gernot Heiser The systems hacker’s guide to the Galaxy: Energy usage in a modern smartphone Asia-Pacific Workshop on Systems (APSys), pp. 7, Singapore, July, 2013 Best Student Paper Award
		Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach Efficient synthesis for concurrency by semantics-preserving transformations Proceedings of the 25th International Conference on Computer Aided Verification, pp. 1–16, Saint Petersburg, Russia, July, 2013
		Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013
		Bernard Blackham and Gernot Heiser Sequoll: A framework for model checking binaries IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 97–106, Philadelphia, USA, April, 2013 Best Paper Award
		Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie and Gustavo Alonso RapiLog: reducing system complexity through verification EuroSys Conference, pp. 323–336, Prague, Czech Republic, April, 2013

2012

		Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012
		Bernard Blackham and Gernot Heiser Correct, fast, maintainable — choose any three! Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
		Bernard Blackham, Vernon Tang and Gernot Heiser To preempt or not to preempt, that is the question Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
		Bernard Blackham, Yao Shi and Gernot Heiser Improving interrupt response time in a verifiable protected microkernel EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012
		Michael von Tessin The clustered multikernel: An approach to formal verification of multiprocessor OS kernels 2nd Workshop on Systems for Future Multi-core Architectures, pp. 1–6, Bern, Switzerland, April, 2012
		Gernot Heiser, Toby Murray and Gerwin Klein It's time for trustworthy systems IEEE Symposium on Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012
		Etienne Le Sueur and Simon Rodgers Operating system support for the heterogeneous OMAP4430: A tale of two micros 13th Linux.conf.au, Ballarat, Australia, January, 2012

2011

		Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser Timing analysis of a protected operating system kernel IEEE Real-Time Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011
		Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein seL4 enforces integrity International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
		Bernard Blackham, Yao Shi and Gernot Heiser Protected hard real-time: The next frontier Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011
		Prashant Varanasi and Gernot Heiser Hardware-supported virtualization on ARM Asia-Pacific Workshop on Systems (APSys), pp. 5 pages, Shanghai, China, July, 2011
		Etienne Le Sueur An analysis of the effectiveness of energy management on modern computer processors MSc Thesis, UNSW, Sydney, Australia, June, 2011
		Etienne Le Sueur and Gernot Heiser Slow down or sleep, that is the question USENIX Technical Conference, Portland, Oregon, USA, June, 2011
		Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski What if you could actually Trust your kernel? Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011
		Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood Provable security: How feasible is it? Workshop on Hot Topics in Operating Systems (HotOS), pp. 5, Napa, USA, May, 2011
		Ihor Kuz, Zachary Anderson, Pravin Shinde and Timothy Roscoe Multicore OS benchmarks: we can do better Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011
		Nicholas FitzRoy-Dale Architecture optimisation PhD Thesis, UNSW, Sydney, Australia, March, 2011
		Etienne Le Sueur and Bernard Blackham e4meter: Power management for the people 12th Linux.conf.au, Brisbane, Australia, January, 2011

2010

		Etienne Le Sueur and Gernot Heiser Dynamic voltage and frequency scaling: The laws of diminishing returns Workshop on Power Aware Computing and Systems, pp. 1–5, Vancouver, Canada, October, 2010
		Gernot Heiser and Ben Leslie The OKL4 microvisor: Convergence point of microkernels and hypervisors Asia-Pacific Workshop on Systems (APSys), pp. 19–24, New Delhi, India, August, 2010
		Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker capDL: A language for describing capability-based systems Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010
		Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser The case for active device drivers Asia-Pacific Workshop on Systems (APSys), pp. 25–30, New Delhi, India, August, 2010
		Michael von Tessin Towards high-assurance multiprocessor virtualisation 6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010
		Aaron Carroll and Gernot Heiser An analysis of power consumption in a smartphone USENIX Annual Technical Conference, pp. 271–284, Boston, MA, US, June, 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 operating-system kernel Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010 Research Highlights paper
		Dhammika Elkaduwe A principled approach to kernel memory management PhD Thesis, UNSW, Sydney, Australia, May, 2010
		Dave Snowdon OS-level power management PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, March, 2010
		Leonid Ryzhyk On the construction of reliable device drivers PhD Thesis, UNSW, Sydney, Australia, January, 2010

2009

		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 ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award
		Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic device driver synthesis with Termite ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009
		Gerwin Klein, Philip Derrin and Kevin Elphinstone Experience report: seL4 — formally verifying a high-performance microkernel Proceedings of the 14th International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009
		Stefan M. Petters, Martin Lawitzky, Ryan Heffernan and Kevin Elphinstone Towards real multi-criticality scheduling IEEE Conference on Embedded and Real-Time Computing and Applications, pp. 155–164, Beijing, China, August, 2009
		Matthew Chapman and Gernot Heiser vNUMA: A virtual shared-memory multiprocessor USENIX Annual Technical Conference, pp. 349–362, San Diego, USA, June, 2009
		Joshua LeVasseur Device-driver reuse via virtual machines PhD Thesis, UNSW, Sydney, Australia, May, 2009
		Dave Snowdon, Etienne Le Sueur, Stefan M. Petters and Gernot Heiser Koala: A platform for OS-level power management EuroSys Conference, pp. 289–302, Nuremberg, DE, April, 2009
		Matthew Chapman vNUMA: Virtual shared-memory multiprocessors PhD Thesis, UNSW, Sydney, Australia, March, 2009
		Gernot Heiser Many-core chips — a case for virtual shared memory Workshop on Managed Many-Core Systems, pp. 4 pages, Washington, DC, USA, March, 2009
		Gernot Heiser Hypervisors for consumer electronics IEEE Consumer Communications and Networking Conference, pp. 1–5, Las Vegas, NV, USA, January, 2009

2008

		Joshua LeVasseur, Volkmar Uhlig, Yaowei Yang, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser Pre-virtualization: Soft layering for virtual machines Asia-Pacific Computer Systems Architecture Conference, pp. 1–9, Hsinchu, Taiwan, August, 2008 Best Paper Award
		Ian Wienand Transparent large-page support for Itanium Linux ME Thesis, UNSW, Sydney, Australia, July, 2008
		Gernot Heiser Do microkernels suck? Other Conference Presentation, Linux.conf.au, Melbourne, Australia, January, 2008.

2007

		Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: Taking microkernels to the next level ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
		Stefan M. Petters, Patryk Zadarnowski and Gernot Heiser Measurements or static analysis or both? Workshop on Worst-Case Execution-Time Analysis, pp. 5–11, Pisa, Italy, December, 2007
		Dave Snowdon, Godfrey van der Linden, Stefan M. Petters and Gernot Heiser Accurate run-time prediction of performance degradation under frequency scaling Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 58–64, Pisa, Italy, December, 2007
		Dave Snowdon, Stefan M. Petters and Gernot Heiser Accurate on-line prediction of processor and memory energy usage under voltage scaling International Conference on Embedded Software, pp. 84–93, Salzburg, Austria, December, 2007
		Gernot Heiser Virtualisation for embedded systems Technical Report, Open Kernel Labs, November, 2007
		Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, San Diego, CA, USA, May, 2007
		Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
		Ihor Kuz, Yan Liu, Ian Gorton and Gernot Heiser CAmkES: A component model for secure microkernel-based embedded systems Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems, Volume 80, Number 5, pp. 687–699, May, 2007 Preprint
		Timothy Roscoe, Kevin Elphinstone and Gernot Heiser Hype and virtue Workshop on Hot Topics in Operating Systems (HotOS), pp. 19–24, San Diego, USA, May, 2007
		Peter Chubb, Matthew Chapman and Myrto Zehnder [para]virtualisation without pain 8th Linux.conf.au, Sydney, NSW, January, 2007
		Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone A memory allocation model for an embedded microkernel International Workshop on Microkernels for Embedded Systems, pp. 28–34, Sydney, Australia, January, 2007
		Nicholas FitzRoy-Dale A declarative approach to extensible interface compilation International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007
		Stefan M. Petters Execution-time profiles Technical Report, NICTA, January, 2007
		Mohit Singal and Stefan M. Petters Issues in analysing L4 for its WCET International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007
		Carl van Schaik and Gernot Heiser High-performance microkernels and virtualisation on ARM and segmented architectures International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007

2006

		Sergio Ruocco User-level fine-grained adaptive real-time scheduling via temporal reflection Proceedings of the 27th IEEE Real-Time Systems Symposium, Rio De Janeiro, Brazil, December, 2006
		Ian Wienand, Adam Wiggins Paul Davies and Peter Chubb The GPT and superpages Gelato ICE, Singapore, October, 2006 Fuzzy Penguin Award
		Geoffrey Lee and Charles Gray L4/Darwin: Evolving UNIX Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Vic, Australia, October, 2006 Slides
		Myrto Zehnder and Peter Chubb Virtualising PCI Gelato ICE, Singapore, October, 2006
		Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty Running the manual: An approach to high-assurance microkernel development Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006
		Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Verified Software: Theories, Tools and Experiments, pp. 1-7, Seattle, USA, August, 2006
		Stefan Schaefer, Bernhard Scholz, Stefan M. Petters and Gernot Heiser Static analysis support for measurement-based WCET analysis 12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Work-in-Progress Session, Sydney, Australia, August, 2006
		Sergio Ruocco Real-Time Programming and L4 Microkernels Proceedings of the 2nd Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Dresden, DE, July, 2006
		Daniel Potts and Ihor Kuz Adapting distributed shared memory applications in diverse environments Proceedings of the 6th International Symposium on Cluster Computing and the Grid, Singapore, May, 2006
		Shehjar Tikoo and Peter Chubb Improving NFS performance Gelato ICE conference, San Jose, CA, April, 2006
		Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel data – first class citizens of the system Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , pp. 39–43, Victor Harbor, South Australia, Australia, January, 2006
		Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur Are virtual-machine monitors microkernels done right? ACM Operating Systems Review, Volume 40, Number 1, pp. 95–99, January, 2006

2005

		Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 2005
		Harvey Tuch and Gerwin Klein A unified memory model for pointers Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005
		Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars 3rd Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005
		Peter Chubb Bugs: getting them stomped! Gelato ICE, Brazil, October, 2005
		Peter Chubb Which filesystem? Gelato ICE, Brazil, October, 2005
		Joshua LeVasseur, Volkmar Uhlig, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser Pre-virtualization: Slashing the cost of virtualization Technical Report PA005520, NICTA, October, 2005
		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, Volume 20, Number 5, pp. 654–664, September, 2005
		David C. Snowdon, Sergio Ruocco and Gernot Heiser Power management and dynamic voltage scaling: Myths and facts Proceedings of the 2005 Workshop on Power Aware Real-time Computing, New Jersey, USA, September, 2005 Preliminary workshop version
		Stefan M. Petters Deadline spanning: A graph based approach IEEE Conference on Embedded and Real-Time Computing and Applications, Hong Kong, China, August, 2005
		David Andrews, Iain Bate, Thomas Nolte, Clara Otero-Perez and Stefan M. Petters Impact of embedded systems evolution on RTOS use and design Proceedings of the 1st Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Palma, Mallorca, Spain, July, 2005
		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 Technical Report PA005043, NICTA, July, 2005
		David C. Snowdon, Stefan M. Petters and Gernot Heiser Power measurement as the basis for power management Proceedings of the 1st Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Palma, Mallorca, Spain, July, 2005
		Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems (HotOS), pp. 7–12, Santa Fe, NM, USA, June, 2005
		Matthew Chapman and Gernot Heiser Implementing transparent shared memory on clusters using virtual machines Proceedings of the 2005 USENIX Annual Technical Conference, pp. 383–386, Anaheim, CA, USA, April, 2005
		Peter Chubb and Darren Williams Linux scalability — from the micro to the HUGE 6th Linux.conf.au, Canberra, ACT, April, 2005
		Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang and Gernot Heiser Itanium — a system implementor's tale Proceedings of the 2005 USENIX Annual Technical Conference, pp. 264–278, Anaheim, CA, USA, April, 2005 Best Student Paper Award
		Ben Leslie, Carl van Schaik and Gernot Heiser Wombat: A portable user-mode Linux for embedded systems 6th Linux.conf.au, Canberra, April, 2005
		Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, NICTA, 2005

2004

		Kevin Elphinstone Future directions in the evolution of the L4 microkernel Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004
		Harvey Tuch and Gerwin Klein Verifying the L4 virtual memory subsystem Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, pp. 73–97, Sydney, Australia, October, 2004
		Kevin Elphinstone and Stefan Götz Initial evaluation of a user-level device driver framework Proceedings of the 9th Asia-Pacific Computer Systems Architecture Conference, Beijing, China, September, 2004
		Gerwin Klein and Harvey Tuch Towards verified virtual memory in L4 TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004
		Ian Wienand and Luke Macpherson Ipbench: A framework for distributed network benchmarking Conference for Unix, Linux and Open Source Professionals (AUUG), pp. 163–170, Melbourne, Australia, September, 2004
		Peter Chubb Get more device drivers out of the kernel! Ottawa Linux Symposium, Ottawa, Canada, July, 2004
		Ihor Kuz L4 user manual — API version X.2 June, 2004
		Peter Chubb Linux kernel infrastructure for user-level device drivers 5th Linux.conf.au, Adelaide, Australia, January, 2004
		Ben Leslie, Nicholas FitzRoy-Dale and Gernot Heiser Encapsulated user-level device drivers in the Mungi operating system Proceedings of the Workshop on Object Systems and Software Architectures 2004, Victor Harbor, South Australia, Australia, January, 2004
		Daniel Potts, Charles Gray, Ben Leslie and Gernot Heiser A secure, language independent, high performance component interface Proceedings of the Workshop on Object Systems and Software Architectures 2004, Victor Harbor, South Australia, January, 2004

2003

		Peter Chubb Where's all the time going? Microstate accounting in Linux 2.5 Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Australia, September, 2003
		Andreas Haeberlen and Kevin Elphinstone User-level management of kernel memory Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
		Chris Szmajda and Gernot Heiser Generalised radix page table: A page table for modern architectures Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, pp. 290-304, Aizu-Wakamatsu City, Japan, September, 2003
		Adam Wiggins, Harvey Tuch, Volkmar Uhlig and Gernot Heiser Implementation of fast address-space switching and TLB sharing on the StrongARM processor Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
		Matthew Chapman, Ian Wienand and Gernot Heiser Itanium page tables and TLB Technical Report UNSW-CSE-TR-0307, School of Computer Science and Engineering, May, 2003
		Ben Leslie and Gernot Heiser Towards untrusted device drivers Technical Report UNSW-CSE-TR-0303, School of Computer Science and Engineering, March, 2003

2002

		Peter Chubb Terabytes on a diet Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Australia, September, 2002
		Shane Stephens and Gernot Heiser Fault tolerance and avoidance in biomedical systems Proceedings of the 10th SIGOPS European Workshop, St Emilion, France, September, 2002
		Peter Chubb YOU ARE LOST in a maze of BitKeeper repositories — all almost the same Australian Open Source Symposium, Sydney, Australia, July, 2002
		Simon Winwood, Yefim Shuf and Hubertus Franke Multiple page size support in the Linux kernel Ottawa Linux Symposium, Ottawa, Canada, June, 2002
		Daniel Potts, Simon Winwood and Gernot Heiser Design and implementation of the L4 microkernel for Alpha multiprocessors Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002
		Kingsley Cheung and Gernot Heiser A resource management framework for priority-based physical-memory allocation Proceedings of the 7th Asia-Pacific Computer Systems Architecture Conference, Monash University, Melbourne, Australia, January, 2002
		Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser Performance of address-space multiplexing on the Pentium Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002

2001

		Gernot Heiser Dealing with TLB tags International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
		Chris Szmajda Calypso: A portable translation layer International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
		Antony Edwards and Gernot Heiser Secure OS extensibility needn't cost an arm and a leg Proceedings of the 8th Workshop on Hot Topics in Operating Systems (HotOS), pp. 168, Schloss Elmau, DE, May, 2001
		Adam Wiggins PLEB: A platform for portable and embedded systems research Technical Report UNSW-CSE-TR-0105, School of Computer Science and Engineering, April, 2001
		Antony Edwards and Gernot Heiser A component architecture for system extensibility Technical Report UNSW-CSE-TR-0103, School of Computer Science and Engineering, March, 2001
		Daniel Potts, Simon Winwood and Gernot Heiser L4 reference manual: Alpha 21x64 Technical Report UNSW-CSE-TR-0104, School of Computer Science and Engineering, March, 2001
		Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller The SawMill framework for VM diversity Proceedings of the 6th Asia-Pacific Computer Systems Architecture Conference, pp. 3–10, Gold Coast, Australia, January, 2001
		Alan Au and Gernot Heiser Enhancing IA64 memory management 2nd Linux.conf.au, Sydney, Australia, January, 2001
		Antony Edwards and Gernot Heiser Components + Security = OS Extensibility Proceedings of the 6th Asia-Pacific Computer Systems Architecture Conference, pp. 27–34, Gold Coast, Australia, January, 2001

2000

Adam Wiggins and Gernot Heiser Fast address-space switching on the StrongARM SA-1100 processor Proceedings of the 5th Australasian Computer Architecture Conference, pp. 97–104, Canberra, Australia, January, 2000

1999

		Adam Wiggins and Gernot Heiser Fast address-space switching on the StrongARM SA-1100 processor Technical Report UNSW-CSE-TR-9906, School of Computer Science and Engineering, July, 1999
		Luke Deller and Gernot Heiser Linking programs in a single address space Proceedings of the 1999 USENIX Annual Technical Conference, pp. 283–294, Monterey, Ca, USA, June, 1999
		Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual: MIPS R4x00, version 1.11, kernel version 79 Sydney, Australia, May, 1999
		Kevin Elphinstone Virtual memory in a 64-bit microkernel PhD Thesis, UNSW, Sydney, Australia, March, 1999
		Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko and Yoonho Park Flexible access control using IPC redirection Proceedings of the 7th Workshop on Hot Topics in Operating Systems (HotOS), pp. 191–196, Rio Rico, AZ, USA, March, 1999
		Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Proceedings of the 4th Australasian Computer Architecture Conference, pp. 211-226, Auckland, New Zealand, January, 1999

1998

		Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Technical Report UNSW-CSE-TR-9804, School of Computer Science and Engineering, August, 1998
		Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke The Mungi single-address-space operating system Software: Practice and Experience, Volume 28, Number 9, pp. 901–928, July, 1998
		Jerry Vochteloo Design, implementation and performance of protection in the Mungi single-address-space operating system PhD Thesis, UNSW, Sydney, Australia, July, 1998
		Alan Au and Gernot Heiser L4 User Manual — version 1.0 Technical Report UNSW-CSE-TR-9801, School of Computer Science and Engineering, April, 1998
		Gernot Heiser, Fondy Lam and Stephen Russell Resource management in the Mungi single-address-space operating system Proceedings of the 21st Australasian Computer Science Conference (ACSC), pp. 417–428, Perth, Australia, February, 1998

1997

		Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual – MIPS R4x00 — Version 1.0 Technical Report UNSW-CSE-TR-9709, School of Computer Science and Engineering, December, 1997
		Gernot Heiser, Fondy Lam and Stephen Russell Resource management in the Mungi single-address-space operating system Technical Report UNSW-CSE-TR-9705, UNSW, August, 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, UNSW, June, 1997
		Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam and Trent Jaeger Achieved IPC performance (still the foundation for extensibility) Proceedings of the 6th Workshop on Hot Topics in Operating Systems (HotOS), pp. 28–31, Cape Cod, MA, USA, May, 1997
		Gernot Heiser, Jerry Vochteloo, Kevin Elphinstone and Stephen Russell The Mungi kernel API/Release 1.0 Technical Report UNSW-CSE-TR-9701, School of Computer Science and Engineering, March, 1997

1996

		Jerry Vochteloo, Kevin Elphinstone, Stephen Russell and Gernot Heiser Protection domain extensions in Mungi Proceedings of the 5th IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 161–165, Seattle, WA, USA, October, 1996
		Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke Supporting persistent object systems in a single address space Proceedings of the 7th International Workshop on Persistent Object Systems (POS), pp. 111–119, Cape May, NJ, USA, May, 1996
		Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization ACM Operating Systems Review, Volume 30, Number 1, pp. 4–15, January, 1996

1995

		Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, November, 1995
		Tim Wilkinson, Kevin Murray, Stephen Russell, Gernot Heiser and Jochen Liedtke Single address space operating systems Technical Report UNSW-CSE-TR-9504, UNSW, November, 1995

1994

Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo Mungi: A distributed single-address-space operating system Proceedings of the 17th Australasian Computer Science Conference (ACSC), pp. 271–80, Christchurch, New Zealand, January, 1994

1993

		Jerry Vochteloo, Stephen Russell and Gernot Heiser Capability-based protection in the Mungi operating system Proceedings of the 3rd IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 108–15, Asheville, NC, USA, December, 1993
		Kevin Elphinstone Address space management issues in the Mungi operating system Technical Report UNSW-CSE-TR-9312, School of Computer Science and Engineering, November, 1993
		Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo Mungi: A distributed single address-space operating system Technical Report UNSW-CSE-TR-9314, School of Computer Science and Engineering, November, 1993
		Gernot Heiser, Kevin Elphinstone, Stephen Russell and Graham R. Hellestrand A distributed single address space system supporting persistence Technical Report UNSW-CSE-TR-9302, UNSW, March, 1993

1992

Stephen Russell, Alan Skea, Kevin Elphinstone, Gernot Heiser, Keith Burston, Ian Gorton and Graham Hellestrand Distribution + persistence = global virtual memory Proceedings of the 2nd IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 96–99, Dourdan, France, September, 1992