Skip to main content
Paper/Talk Abstract plain text Paper in PDF format PDF
Presentation slides Slides Video of the presentation Presentation
A reference to a location Link Paper yet to be published to be published

Publications related to Operating Systems @ SSRG

2018

Abstract PDF 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
Abstract
Slides
PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract Slides
Video
Gernot Heiser
Flying autonomous aircraft: Mixed-criticality support in seL4
at linux.conf.au, Sydney, January, 2018
Abstract PDF Anna Lyons
Mixed-criticality scheduling and resource sharing for high-assurance operating systems
PhD Thesis, UNSW, 2018

2017

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Aaron Carroll
Understanding and reducing smartphone energy consumption
PhD Thesis, UNSW, Sydney, Australia, May, 2017
Abstract PDF Thomas Sewell
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, 2017

2016

Abstract PDF 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
Abstract PDF 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

Abstract
Slides
PDF 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
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
SAT-based strategy extraction in reachability games
AAAI, Austin, TX, USA, January, 2015

2014

Abstract
Slides
PDF 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
Abstract PDF 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
Abstract
Slides
PDF 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
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Technical Report NRL-8281, NICTA, August, 2014
Abstract PDF 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
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Interpolants in two-player games
Abstract, iPRA workshop, July, 2014.
Abstract PDF Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Practical CNF interpolants via BDDs
Abstract, iPRA workshop, July, 2014.
Abstract PDF 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
Abstract PDF 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
Abstract
Slides
PDF 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
Abstract
Slides
PDF 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
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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
Abstract
Slides
PDF 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.
Abstract
Slides
PDF
Presentation Video
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
Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF 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
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract PDF 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
Abstract
Slides
PDF 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!
Abstract PDF Franck Cassez and Jean-Luc Bechennec
Timing analysis of binary programs with UPPAAL
13th International Conference on Application of Concurrency to System Design (ACSD), pp. 41–50, Barcelona, Spain, July, 2013
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Efficient synthesis for concurrency by semantics-preserving transformations
25th International Conference on Computer Aided Verification, pp. 1–16, Saint Petersburg, Russia, July, 2013
Abstract
Slides
PDF 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!
Abstract
Slides
PDF 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

Abstract PDF Matthew Fernandez, Ihor Kuz and Gerwin Klein
Formalisation of a component platform
Poster presented at Operating Systems Design and Implementation 2012, October, 2012
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Correct, fast, maintainable — choose any three!
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract
Slides
PDF 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
Abstract PDF Franck Cassez, René Rydhof Hansen and Mads Olesen
What is a timing anomaly?
Workshop on Worst-Case Execution-Time Analysis, pp. 1–12, Pisa, Italy, July, 2012
Abstract
Slides
PDF 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
Abstract PDF 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
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
It's time for trustworthy systems
IEEE Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012
Abstract Video 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

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Prashant Varanasi and Gernot Heiser
Hardware-supported virtualization on ARM
Asia-Pacific Workshop on Systems (APSys), pp. 5 pages, Shanghai, China, July, 2011
Abstract PDF Etienne Le Sueur
An analysis of the effectiveness of energy management on modern computer processors
MSc Thesis, UNSW, Sydney, Australia, June, 2011
Abstract PDF Etienne Le Sueur and Gernot Heiser
Slow down or sleep, that is the question
USENIX Technical Conference, pp. 6, Portland, Oregon, USA, June, 2011
Abstract
Slides
PDF 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, pp. 1–5, Napa, CA, USA, May, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems, pp. 5, Napa, USA, May, 2011
Abstract PDF Ihor Kuz, Zachary Anderson, Pravin Shinde and Timothy Roscoe
Multicore OS benchmarks: we can do better
Workshop on Hot Topics in Operating Systems, pp. 1–5, Napa, CA, USA, May, 2011
Abstract PDF Nicholas FitzRoy-Dale
Architecture optimisation
PhD Thesis, UNSW, Sydney, Australia, March, 2011
Abstract Video Etienne Le Sueur and Bernard Blackham
e4meter: Power management for the people
12th Linux.conf.au, Brisbane, Australia, January, 2011

2010

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Michael von Tessin
Towards high-assurance multiprocessor virtualisation
6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010
Abstract PDF Aaron Carroll and Gernot Heiser
An analysis of power consumption in a smartphone
Proceedings of the 2010 USENIX Annual Technical Conference, Boston, MA, USA, June, 2010
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
An analysis of power consumption in a smartphone
USENIX Annual Technical Conference, pp. 271–284, Boston, MA, USA, June, 2010
Abstract PDF 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
Abstract PDF Dhammika Elkaduwe
A principled approach to kernel memory management
PhD Thesis, UNSW, Sydney, Australia, May, 2010
Abstract PDF Dave Snowdon
OS-level power management
PhD Thesis, UNSW CSE, Sydney, Australia, March, 2010
Abstract PDF Leonid Ryzhyk
On the construction of reliable device drivers
PhD Thesis, UNSW, Sydney, Australia, January, 2010

2009

Abstract
Slides
PDF
Presentation Video
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
Abstract PDF 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
Abstract PDF
Presentation Video
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
Abstract PDF 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
Abstract PDF Matthew Chapman and Gernot Heiser
vNUMA: A virtual shared-memory multiprocessor
USENIX Annual Technical Conference, pp. 349–362, San Diego, USA, June, 2009
Abstract PDF Gernot Heiser
Trusted <= trustworthy <= proof — position paper
Future of Trust in Computing, pp. 55–59, Berlin, May, 2009
Abstract PDF Joshua LeVasseur
Device-driver reuse via virtual machines
PhD Thesis, UNSW, Sydney, Australia, May, 2009
Abstract PDF Dave Snowdon, Etienne Le Sueur, Stefan Petters and Gernot Heiser
Koala: A platform for OS-level power management
EuroSys Conference, pp. 289–302, Nuremburg, DE, April, 2009
Abstract PDF Matthew Chapman
vNUMA: Virtual shared-memory multiprocessors
PhD Thesis, UNSW, Sydney, Australia, March, 2009
Abstract PDF 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
Abstract PDF Gernot Heiser
Hypervisors for consumer electronics
IEEE Consumer Communications and Networking Conference, pp. 1–5, Las Vegas, NV, USA, January, 2009

2008

Abstract PDF 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!
Abstract PDF Ian Wienand
Transparent large-page support for Itanium Linux
ME Thesis, UNSW, Sydney, Australia, July, 2008
Abstract PDF
Presentation Video
Gernot Heiser
Do microkernels suck?
9th Linux.conf.au, January, 2008

2007

Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
Abstract PDF Stefan 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
Abstract PDF Dave Snowdon, Godfrey van der Linden, Stefan 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
Abstract PDF Dave Snowdon, Stefan 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
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems, pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF 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
Abstract link 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
Abstract PDF Timothy Roscoe, Kevin Elphinstone and Gernot Heiser
Hype and virtue
Workshop on Hot Topics in Operating Systems, pp. 19–24, San Diego, USA, May, 2007
Abstract PDF Peter Chubb, Matthew Chapman and Myrto Zehnder
[para]virtualisation without pain
8th Linux.conf.au, Sydney, NSW, January, 2007
Abstract PDF 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
Abstract PDF Nicholas FitzRoy-Dale
A declarative approach to extensible interface compilation
International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007
Abstract PDF Stefan M. Petters
Execution-time profiles
Technical Report, NICTA, January, 2007
Abstract PDF Mohit Singal and Stefan M. Petters
Issues in analysing L4 for its WCET
International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007
Abstract PDF 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

Abstract PDF 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
Abstract PDF Ian Wienand, Adam Wiggins Paul Davies and Peter Chubb
The GPT and superpages
Gelato ICE, Singapore, October, 2006
Fuzzy Penguin Award!
Abstract PDF Geoffrey Lee and Charles Gray
L4/Darwin: Evolving UNIX
Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Vic, Australia, October, 2006
Slides
Abstract PDF Myrto Zehnder and Peter Chubb
Virtualising PCI
Gelato ICE, Singapore, October, 2006
Abstract PDF 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
Abstract PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), pp. 1-7, Seattle, USA, August, 2006
Abstract PDF 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
Abstract PDF Sergio Ruocco
Real-Time Programming and L4 Microkernels
Proceedings of the 2nd Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Dresden, Germany, July, 2006
Abstract PDF 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
Abstract PDF Shehjar Tikoo and Peter Chubb
Improving NFS performance
Gelato ICE conference, San Jose, CA, April, 2006
Abstract PDF 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
Abstract PDF 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

Abstract PDF Gernot Heiser
Secure embedded systems need microkernels
USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 2005
Abstract PDF 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
Abstract PDF Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco
L4cars
3rd Embedded Security in Cars Conference (escar), Cologne, Germany, November, 2005
Abstract PDF Peter Chubb
Bugs: getting them stomped!
Gelato ICE, Brazil, October, 2005
Abstract PDF Peter Chubb
Which filesystem?
Gelato ICE, Brazil, October, 2005
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Stefan M. Petters
Deadline spanning: A graph based approach
IEEE Conference on Embedded and Real-Time Computing and Applications, Hong Kong, China, August, 2005
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Proceedings of the 10th Workshop on Hot Topics in Operating Systems, pp. 7–12, Santa Fe, NM, USA, June, 2005
Abstract PDF 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
Abstract PDF Peter Chubb and Darren Williams
Linux scalability — from the micro to the HUGE
6th Linux.conf.au, Canberra, ACT, April, 2005
Abstract PDF 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!
Abstract PDF Ben Leslie, Carl van Schaik and Gernot Heiser
Wombat: A portable user-mode Linux for embedded systems
6th Linux.conf.au, Canberra, April, 2005
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004
Abstract PDF Ian Wienand and Luke Macpherson
Ipbench: A framework for distributed network benchmarking
AUUG Winter Conference, pp. 163–170, Melbourne, Australia, September, 2004
Abstract PDF Peter Chubb
Get more device drivers out of the kernel!
Ottawa Linux Symposium, Ottawa, Canada, July, 2004
Abstract PDF Ihor Kuz
L4 user manual — API version X.2
June, 2004
Abstract PDF Peter Chubb
Linux kernel infrastructure for user-level device drivers
5th Linux.conf.au, Adelaide, Australia, January, 2004
Abstract PS 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
Abstract PS 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

Abstract PDF Peter Chubb
Where's all the time going? Microstate accounting in Linux 2.5
AUUG Winter Conference, Melbourne, Australia, September, 2003
Abstract PDF 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
Abstract PDF 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
Abstract PS 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
Abstract PDF 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
Abstract PDF Ben Leslie and Gernot Heiser
Towards untrusted device drivers
Technical Report UNSW-CSE-TR-0303, School of Computer Science and Engineering, March, 2003

2002

Abstract PS Peter Chubb
Terabytes on a diet
AUUG Winter Conference, Melbourne, Australia, September, 2002
Abstract PDF Shane Stephens and Gernot Heiser
Fault tolerance and avoidance in biomedical systems
Proceedings of the 10th SIGOPS European Workshop, St Emilion, France, September, 2002
Abstract PDF Peter Chubb
YOU ARE LOST in a maze of BitKeeper repositories — all almost the same
Australian Open Source Symposium, Sydney, Australia, July, 2002
Abstract PS Simon Winwood, Yefim Shuf and Hubertus Franke
Multiple page size support in the Linux kernel
Ottawa Linux Symposium, Ottawa, Canada, June, 2002
Abstract PDF 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
Abstract PS 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
Abstract PDF 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

Abstract PDF Gernot Heiser
Dealing with TLB tags
International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PS Chris Szmajda
Calypso: A portable translation layer
International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PDF 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, pp. 168, Schloss Elmau, Germany, May, 2001
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PS 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
Abstract PS Alan Au and Gernot Heiser
Enhancing IA64 memory management
2nd Linux.conf.au, Sydney, Australia, January, 2001
Abstract PDF 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

Abstract PS 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
Abstract PDF Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther
The Sawmill multiserver approach
Proceedings of the 9th SIGOPS European Workshop, pp. 109–114, Kolding, Denmark, 2000

1999

Abstract PDF 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
Abstract PS 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
Abstract PS Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual: MIPS R4x00, version 1.11, kernel version 79
Sydney, Australia, May, 1999
Abstract PS Kevin Elphinstone
Virtual memory in a 64-bit microkernel
PhD Thesis, UNSW, Sydney, Australia, March, 1999
Abstract PDF 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, Rio Rico, AZ, USA, March, 1999
Abstract PS 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

Abstract PDF 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
Abstract PS 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
Abstract PS Jerry Vochteloo
Design, implementation and performance of protection in the Mungi single-address-space operating system
PhD Thesis, UNSW, Sydney, Australia, July, 1998
Abstract PDF 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
Abstract PS 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

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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, pp. 28–31, Cape Cod, MA, USA, May, 1997
Abstract PDF 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

Abstract PS 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
Abstract PS 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
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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

Abstract PS 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

Abstract PS 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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

Abstract PS 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
Served by Apache on Linux on seL4.