ERTOS Publications, Theses and Technical Reports
- Best papers from NICTA's ERTOS Group
- All publications from NICTA's ERTOS Group ( 2008, 2007, 2006, 2005, 2004, 2003 )
- Non-NICTA publications by the UNSW OS group ( 2008, 2006, 2005, 2004, 2003, 2002 )
- Selected undergraduate student theses
 | is the abstract of the paper |
 | is the paper in compressed PostScript (.ps.gz or .ps.Z) format |
 | is the paper in PDF format |
 | is a reference to locations, where we can not directly refer to the downloadable document. |
 | means that the paper is yet to be published |
ERTOS Best Papers
All ERTOS Publications
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 Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 To appear |
|
|
|
Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic device driver synthesis with Termite Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 To appear |
|
|
|
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, Glasgow, UK, August, 2009 To appear. |
|
|
|
Rafal Kolanski and Gerwin Klein Types, maps and separation logic Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009 To appear |
|
|
|
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish Mind the gap: A verification framework for low-level C Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009 To appear |
|
|
|
Andrew Boyton A verified shared capability model Proceedings of the 4th Workshop on Systems Software Verification SSV'09, Aachen, Germany, June, 2009 To appear |
|
|
|
Matthew Chapman and Gernot Heiser vNUMA: A virtual shared-memory multiprocessor Proceedings of the 2009 USENIX Annual Technical Conference, San Diego, CA, USA, June, 2009 |
|
|
|
Nicholas FitzRoy-Dale and Ihor Kuz Towards automatic performance optimisation of componentised systems 2nd Workshop on Isolation and Integration in Embedded Systems, Nuremberg, Germany, April, 2009 |
|
|
|
Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser Dingo: Taming device drivers Proceedings of the 4th EuroSys Conference, Nuremberg, Germany, April, 2009 |
|
|
|
Asia Slowinska and Herbert Bos Pointless tainting? Evaluating the practicality of pointer tainting Proceedings of the 4th EuroSys Conference, Nuremberg, Germany, April, 2009 |
|
|
|
David C. Snowdon, Etienne Le Sueur, Stefan M. Petters and Gernot Heiser Koala: A platform for OS-level power management Proceedings of the 4th EuroSys Conference, Nuremberg, Germany, April, 2009 |
|
|
|
Matthew Chapman vNUMA: Virtual shared-memory multiprocessors, PhD Thesis, University of NSW, Sydney 2052, Australia, 2009 |
|
|
|
Gernot Heiser Many-core chips — a case for virtual shared memory Proceedings of the 2nd Workshop on Managed Many-Core Systems, Washington, DC, USA, March, 2009 |
|
|
|
Gerwin Klein Operating system verification — an overview Sādhanā, 34(1), 27–69, (February, 2009) Invited paper. Journal homepage. |
|
|
|
Gernot Heiser Hypervisors for consumer electronics Proceedings of the 6th IEEE Consumer Communications and Networking Conference, Las Vegas, NV, USA, January, 2009 |
|
|
|
Harvey Tuch Formal verification of C systems code: Structured types, separation logic and theorem proving Journal of Automated Reasoning: Special Issue on Operating System Verification, ?, 59, (2009) To appear |
2008
2007
|
|
|
Gernot Heiser Your system is secure? Prove it! USENIX ;login:, 32(6), 35–38, (December, 2007) |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007 |
|
|
|
Leonid Ryzhyk, Ihor Kuz and Gernot Heiser Formalising device driver interfaces Proceedings of the 4th Workshop on Programming Languages and Operating Systems, Stevenson, Washington, USA, October, 2007 |
|
|
|
David C. Snowdon, Stefan M. Petters and Gernot Heiser Accurate on-line prediction of processor and memory energy usage under voltage scaling Proceedings of the 7th International Conference on Embedded Software, Salzburg, Austria, October, 2007 |
|
|
|
Luke Macpherson Performing under overload, PhD Thesis, University of NSW, Sydney 2052, Australia, 2007 |
|
|
|
Andrew Baumann Dynamic update for operating systems, PhD Thesis, University of NSW, Sydney 2052, Australia, 2007 |
|
|
|
Scott Brandt and Kevin Elphinstone Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications Pisa, Italy (July, 2007). NICTA. |
|
|
|
Kevin Elphinstone, David Greenaway and Sergio Ruocco Lazy scheduling and direct process switch — merit or myths? Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications, Pisa, Italy, July, 2007 Preliminary version |
|
|
|
Ansgar Fehnker, Ralf Huuck, Felix Rauch and Sean Seefried Analysing Embedded System Software Proceedings of C/C++ Verification Workshop, Oxford, UK, July, 2007 Extended abstract |
|
|
|
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, 41(4), 3–11, (July, 2007) |
|
|
|
Ihor Kuz and Yan Liu Extending the capabilities of component models for embedded systems Proceedings of the Third International Conference on the Quality of Software-Architectures (QoSA), Boston, MA, USA, July, 2007 |
|
|
|
Jia Meng, Lawrence C. Paulson and Gerwin Klein A termination checker for Isabelle Hoare logic 4th International Verification Workshop - VERIFY'07, Bremen, Germany, July, 2007 |
|
|
|
Stefan M. Petters, Patryk Zadarnowski and Gernot Heiser Measurements or static analysis or both? Proceedings of the 7th Workshop on Worst-Case Execution-Time Analysis, Pisa, Italy, July, 2007 |
|
|
|
David C. Snowdon, Godfrey van der Linden, Stefan M. Petters and Gernot Heiser Accurate run-time prediction of performance degradation under frequency scaling Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications, Pisa, Italy, July, 2007 |
|
|
|
Andrew Baumann, Jonathan Appavoo, Robert W. Wisniewski, Dilma Da Silva, Orran Krieger and Gernot Heiser Reboots are for hardware: Challenges and solutions to updating an operating system on the fly Proceedings of the 2007 USENIX Annual Technical Conference, Santa Clara, CA, USA, June, 2007 |
|
|
|
Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch Model Checking Software at Compile Time Proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, Shanghai, China, June, 2007 |
|
|
|
Leonid Ryzhyk, Timothy Bourke and Ihor Kuz Reliable device drivers require well-defined protocols Proceedings of the 3rd Workshop on Hot Topics in System Dependability, Edinburgh, UK, June, 2007 |
|
|
|
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Proceedings of the 11th Workshop on Hot Topics in Operating Systems, 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, 80(5), 687–699, (May, 2007) Preprint |
|
|
|
Timothy Roscoe, Kevin Elphinstone and Gernot Heiser Hype and virtue Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007 |
|
|
|
Ihor Kuz and Stefan M. Petters Proceedings of the 1st International Workshop on Microkernels for Embedded Systems Sydney, Australia (March, 2007). NICTA. |
|
|
|
Peter Chubb, Matthew Chapman and Myrto Zehnder [para]virtualisation without pain Proceedings of the 8th Linux.Conf.Au, Sydney, NSW, January, 2007 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone A memory allocation model for an embedded microkernel Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007 |
|
|
|
Nicholas FitzRoy-Dale A declarative approach to extensible interface compilation Proceedings of the 1st 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 Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007 |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007 |
|
|
|
Carl van Schaik and Gernot Heiser High-performance microkernels and virtualisation on ARM and segmented architectures Proceedings of the 1st 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 |
|
|
|
Timothy Bourke and Stefan M. Petters Work in Progress Proceedings of the 13th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA) 2007 Sydney, Australia (October, 2006). None. |
|
|
|
Geoffrey Lee and Charles Gray L4/Darwin: Evolving UNIX Conference for Unix, Linux and Open Source Professionals, Melbourne, Vic, Australia, October, 2006 Slides |
|
|
|
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 Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 2006 |
|
|
|
Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch Goanna — A Static Model Checker Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems, Bonn, Germany, August, 2006 Published in Lecture Notes in Computer Science, Springer-Verlag (Vol. 4346). |
|
|
|
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, Dresden, Germany, 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 |
|
|
|
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 , 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, 40(1), 95–99, (January, 2006) |
|
|
|
Rafal Kolanski and Gerwin Klein Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006 |
|
|
|
Ben Leslie GrailOS: A micro-kernel based, multi-server, multi-personality operating system Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006 |
|
|
|
Leonid Ryzhyk and Ihor Kuz Towards operating system support for application-specific fault-tolerance protocols Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006 |
|
|
|
Simon Winwood, Gerwin Klein and Manuel Chakravarty On the synthesis of proof-carrying temporal reference monitors Proceedings of the 16th International Symposium on Logic-Based Program Synthesis and Transformation, Venice, Italy, 2006 |
2005
|
|
|
Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, 30(6), 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, 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, Germany, November, 2005 |
|
|
|
Andrew Baumann and Jonathan Appavoo Improving dynamic update for operating systems Proceedings of the 20th ACM Symposium on Operating Systems Principles, Work-in-Progress Session, Brighton, UK, 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 |
|
|
|
Felix Rauch Comprehensive Throughput Evaluation of LANs in Clusters of PCs with Switchbench — or How to Bring Your Switch to its Knees Proceedings of the IEEE International Symposium on Workload Characterization 2005, Austin, TX, USA, 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, 20(5), 654–664, (September, 2005) See TR PA005043 for a preprint |
|
|
|
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 Embedded Real-Time Computing Systems and Applications (RTCSA 2005), 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, 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, Palma, Mallorca, Spain, July, 2005 |
|
|
|
Simon Winwood and Manuel Chakravarty Secure untrusted binaries — provably! 3rd International Workshop on Formal Aspect of Security and Trust, Newcastle upon Tyne, UK, July, 2005 |
|
|
|
Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June, 2005 |
|
|
|
Andrew Baumann, Gernot Heiser, Jonathan Appavoo, Dilma Da Silva, Orran Krieger, Robert W. Wisniewski and Jeremy Kerr Providing dynamic update in an operating system Proceedings of the 2005 USENIX Annual Technical Conference, Anaheim, CA, USA, April, 2005 |
|
|
|
Andrew Baumann, Jeremy Kerr, Jonathan Appavoo, Dilma Da Silva, Orran Krieger and Robert W. Wisniewski Module hot-swapping for dynamic update and reconfiguration in K42 Proceedings of the 6th Linux.Conf.Au, Canberra, Australia, April, 2005 |
|
|
|
Matthew Chapman and Gernot Heiser Implementing transparent shared memory on clusters using virtual machines Proceedings of the 2005 USENIX Annual Technical Conference, Anaheim, CA, USA, 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, 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 Proceedings of the 6th Linux.Conf.Au, Canberra, April, 2005 |
|
|
|
Felix Rauch and Thomas M. Stricker OS Support for a Commodity Database on PC Clusters — Distributed Devices vs. Distributed File Systems Proceedings of the 16th Australasian Database Conference, Newcastle, Australia, January, 2005 |
|
|
|
Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, National ICT Australia, 2005 |
2004
2003
Other technical reports of the School of Computer Science & Engineering.
Non-NICTA Publications
These publications are from NICTA-independent work of the UNSW OS group (DiSy) which is co-located with ERTOS. They include outcomes of ARC-funded projects and pre-NICTA work of the group.2008
2006
|
|
|
Myrto Zehnder and Peter Chubb Virtualising PCI Gelato ICE, Singapore, October, 2006 |
|
|
|
Shehjar Tikoo and Peter Chubb Improving NFS performance Gelato ICE conference, San Jose, CA, April, 2006 |
2005
|
|
|
Peter Chubb and Darren Williams Linux scalability — from the micro to the HUGE Proceedings of the 6th Linux.Conf.Au, Canberra, ACT, April, 2005 |
2004
2003
2002
2001
2000
1999
1998
1997
1996
1995
1994
1993
1992
Selected Undergraduate Student Theses
Below are a selection of honours theses done with the group. UNSW students can access the complete list.2008
|
|
|
Aaron Carroll I/O scheduling on RAID, BE Thesis, University of NSW, Sydney 2052, Australia, 2008 |
2007
2006
2005
2003
|
|
|
Ka-shu Wong MacOS X on L4, BE Thesis, University of NSW, Sydney 2052, Australia, 2003 |