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
Gernot Heiser LionsOS: A highly dependable operating system for cyberphysical systems Keynote at International Symposium on Parallel Computing and Distributed Systems, September, 2024 | ||
Gernot Heiser LionsOS: Towards a truly dependable operating system Keynote at International Conference on Dependable Systems and Networks (DSN), June, 2024 | ||
Peter Chubb Running your own mailserver Everything Open, Gladstone, QLD, AU, April, 2024 | ||
Gernot Heiser, Peter Chubb, Alex Brown, Courtney Darville and Lucy Parker sDDF design: design, implementation and evaluation of the seL4 device driver framework https://trustworthy.systems/publications/papers/Heiser_CBDP_24.pdf, 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 | |
Anna Lyons Mixed-criticality scheduling and resource sharing for high-assurance operating systems PhD Thesis, UNSW, 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 |
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 | ||
Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, July, 2017 | ||
Aaron Carroll Understanding and reducing smartphone energy consumption PhD Thesis, UNSW, Sydney, Australia, May, 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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! 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 USENIX, pp. 383–386, Anaheim, CA, USA, April, 2005 | ||
Peter Chubb and Darren Williams Linux scalability — from the micro to the HUGE 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 USENIX, 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 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 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 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 Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2004 | ||
Daniel Potts, Charles Gray, Ben Leslie and Gernot Heiser A secure, language independent, high performance component interface Workshop on Object Systems and Software Architectures , 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 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 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 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 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 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 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 Asia-Pacific Computer Systems Architecture Conference, pp. 3–10, Gold Coast, Australia, January, 2001 | ||
Alan Au and Gernot Heiser Enhancing IA64 memory management Linux.conf.au, Sydney, Australia, January, 2001 | ||
Antony Edwards and Gernot Heiser Components + Security = OS Extensibility 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 Australasian Computer Architecture Conference, pp. 97–104, Canberra, Australia, January, 2000 | ||
Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther The Sawmill multiserver approach SIGOPS European Workshop, pp. 109–114, Kolding, Denmark, 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 USENIX, 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 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 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 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) 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 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 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 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 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 IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 96–99, Dourdan, France, September, 1992 |