A Portable Operating System Interface and Utility Library. - Edoardo S. Biagioni; Klaus H. Hinrichs; Gernot Heiser; Carlo Muller (IEEE Softw., 1986)

Three-dimensional numerical semiconductor device simulation: algorithms, architectures, results. - Gernot Heiser; Claude Pommerell; Jürgen Weis; Wolfgang Fichtner (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1991)

Design and implementation of a three-dimensional, general purpose semiconductor device simulatior. - Gernot Heiser (Hartung-Gorre, 1991)

Libra: A Library for Reliable Distributed Applications. - Jinsong Ouzang; Gernot Heiser (PDPTA, 1996)

Supporting Persistent Object Systems in a Single Address Space. - Kevin Elphinstone; Stephen Russell 004; Gernot Heiser; Jochen Liedtke (POS, 1996)

Achieved IPC Performance. - Jochen Liedtke; Kevin Elphinstone; Sebastian Schönberg; Hermann Härtig; Gernot Heiser; Nayeem Islam; Trent Jaeger (Workshop on Hot Topics in Operating Systems, 1997)

The Mungi Single-Address-Space Operating System. - Gernot Heiser; Kevin Elphinstone; Jerry Vochteloo; Stephen Russell 004; Jochen Liedtke (Softw. Pract. Exp., 1998)

Linking Programs in a Single Address Space. - Luke Deller; Gernot Heiser (USENIX ATC, General Track, 1999)

Fast Address-Space Switching on the StrongARM SA-1100 Processor. - Adam Wiggins; Gernot Heiser (ACAC, 2000)

Components + Security = OS Extensibility. - Antony Edwards; Gernot Heiser (ACSAC, 2001)

Secure OS Extensibility Needn't Cost an Arm and a Leg. - Antony Edwards; Gernot Heiser (HotOS, 2001)

Fault tolerance and avoidance in biomedical systems. - Shane G. Stephens; Gernot Heiser (ACM SIGOPS European Workshop, 2002)

Variable Radix Page Table: A Page Table for Modern Architectures. - Cristan Szmajda; Gernot Heiser (Asia-Pacific Computer Systems Architecture Conference, 2003)

Implementation of Fast Address-Space Switching and TLB Sharing on the StrongARM Processor. - Adam Wiggins; Harvey Tuch; Volkmar Uhlig; Gernot Heiser (Asia-Pacific Computer Systems Architecture Conference, 2003)

Legba: Fast Hardware Support for Fine-Grained Protection. - Adam Wiggins; Simon Winwood; Harvey Tuch; Gernot Heiser (Asia-Pacific Computer Systems Architecture Conference, 2003)

OS Verification - Now! - Harvey Tuch; Gerwin Klein; Gernot Heiser (HotOS, 2005)

Pre-virtualization: uniting two worlds. - Joshua LeVasseur; Volkmar Uhlig; Ben Leslie; Matthew Chapman; Gernot Heiser (SOSP, 2005)

Providing Dynamic Update in an Operating System. - Andrew Baumann; Gernot Heiser; Jonathan Appavoo; Dilma Da Silva; Orran Krieger; Robert W. Wisniewski; Jeremy Kerr (USENIX ATC, General Track, 2005)

Implementing Transparent Shared Memory on Clusters Using Virtual Machines. - Matthew Chapman; Gernot Heiser (USENIX ATC, General Track, 2005)

Itanium - A System Implementor's Tale(Awarded General Track Best Student Paper Award!). - Charles Gray; Matthew Chapman; Peter Chubb; David Mosberger; Gernot Heiser (USENIX ATC, General Track, 2005)

User-Level Device Drivers: Achieved Performance. - Ben Leslie; Peter Chubb; Nicholas Fitzroy-Dale; Stefan Götz 004; Charles Gray; Luke Macpherson; Daniel Potts; Yue-Ting Shen; Kevin Elphinstone; Gernot Heiser (J. Comput. Sci. Technol., 2005)

Secure Embedded Systems Need Microkernels. - Gernot Heiser (login Usenix Mag., 2005)

Panel: Is University Systems Teaching and Research Relevant to Industry?. - Gernot Heiser (USENIX ATC, General Track, 2006)

Are virtual-machine monitors microkernels done right? - Gernot Heiser; Volkmar Uhlig; Joshua LeVasseur (ACM SIGOPS Oper. Syst. Rev., 2006)

Accurate on-line prediction of processor and memoryenergy usage under voltage scaling. - David C. Snowdon; Stefan M. Petters; Gernot Heiser (EMSOFT, 2007)

Towards a Practical, Verified Kernel. - Kevin Elphinstone; Gerwin Klein; Philip Derrin; Timothy Roscoe; Gernot Heiser (HotOS, 2007)

Hype and Virtue. - Timothy Roscoe; Kevin Elphinstone; Gernot Heiser (HotOS, 2007)

Formalising device driver interfaces. - Leonid Ryzhyk; Ihor Kuz; Gernot Heiser (PLOS@SOSP, 2007)

Reboots Are for Hardware: Challenges and Solutions to Updating an Operating System on the Fly. - Andrew Baumann; Jonathan Appavoo; Robert W. Wisniewski; Dilma Da Silva; Orran Krieger; Gernot Heiser (USENIX ATC, 2007)

Measurements or Static Analysis or Both?. - Stefan M. Petters; Patryk Zadarnowski; Gernot Heiser (WCET, 2007)

CAmkES: A component model for secure microkernel-based embedded systems. - Ihor Kuz; Yan Liu 001; Ian Gorton; Gernot Heiser (J. Syst. Softw., 2007)

Towards trustworthy computing systems: taking microkernels to the next level. - Gernot Heiser; Kevin Elphinstone; Ihor Kuz; Gerwin Klein; Stefan M. Petters (ACM SIGOPS Oper. Syst. Rev., 2007)

Your System Is Secure? Prove It! - Gernot Heiser (login Usenix Mag., 2007)

Pre-virtualization: Soft layering for virtual machines. - Joshua LeVasseur; Volkmar Uhlig; Yaowei Yang; Matthew Chapman; Peter Chubb; Ben Leslie; Gernot Heiser (ACSAC, 2008)

Operating System Verification for Real Use. - Gernot Heiser (VERIFY, 2008)

The role of virtualization in embedded systems. - Gernot Heiser (IIES@EuroSys, 2008)

Hypervisors for Consumer Electronics. - Gernot Heiser (CCNC, 2009)

Dingo: taming device drivers. - Leonid Ryzhyk; Peter Chubb; Ihor Kuz; Gernot Heiser (EuroSys, 2009)

Koala: a platform for OS-level power management. - David C. Snowdon; Etienne Le Sueur; Stefan M. Petters; Gernot Heiser (EuroSys, 2009)

seL4: formal verification of an OS kernel. - Gerwin Klein; Kevin Elphinstone; Gernot Heiser; June Andronick; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (SOSP, 2009)

Automatic device driver synthesis with termite. - Leonid Ryzhyk; Peter Chubb; Ihor Kuz; Etienne Le Sueur; Gernot Heiser (SOSP, 2009)

vNUMA: A Virtual Shared-Memory Multiprocessor. - Matthew Chapman; Gernot Heiser (USENIX ATC, 2009)

The road to trustworthy systems. - Gernot Heiser; June Andronick; Kevin Elphinstone; Gerwin Klein; Ihor Kuz; Leonid Ryzhyk (STC@CCS, 2010)

Improved Device Driver Reliability Through Verification Reuse. - Leonid Ryzhyk; John Keys; Balachandra Mirla; Arun Raghunath; Mona Vij; Gernot Heiser (HotDep, 2010)

The OKL4 microvisor: convergence point of microkernels and hypervisors. - Gernot Heiser; Ben Leslie (ApSys, 2010)

The case for active device drivers. - Leonid Ryzhyk; Yanjin Zhu; Gernot Heiser (ApSys, 2010)

An Analysis of Power Consumption in a Smartphone. - Aaron Carroll; Gernot Heiser (USENIX ATC, 2010)

seL4: formal verification of an operating-system kernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (Commun. ACM, 2010)

Static analysis of device drivers: we can do better! - Sidney Amani; Leonid Ryzhyk; Alastair F. Donaldson; Gernot Heiser; Alexander Legg; Yanjin Zhu (APSys, 2011)

Protected hard real-time: the next frontier. - Bernard Blackham; Yao Shi; Gernot Heiser (APSys, 2011)

Hardware-supported virtualization on ARM. - Prashant Varanasi; Gernot Heiser (APSys, 2011)

Improved device driver reliability through hardware verification reuse. - Leonid Ryzhyk; John Keys; Balachandra Mirla; Arun Raghunath; Mona Vij; Gernot Heiser (ASPLOS, 2011)

Low-overhead virtualization of mobile platforms. - Gernot Heiser (CASES, 2011)

Virtualizing embedded systems: why bother? - Gernot Heiser (DAC, 2011)

What If You Could Actually Trust Your Kernel? - Gernot Heiser; Leonid Ryzhyk; Michael von Tessin; Aleksander Budzynowski (HotOS, 2011)

Timing Analysis of a Protected Operating System Kernel. - Bernard Blackham; Yao Shi; Sudipta Chattopadhyay 001; Abhik Roychoudhury; Gernot Heiser (RTSS, 2011)

Slow Down or Sleep, That Is the Question. - Etienne Le Sueur; Gernot Heiser (USENIX ATC, 2011)

Architecture optimisation with currawong. - Nicholas Fitzroy-Dale; Ihor Kuz; Gernot Heiser (Comput. Commun. Rev., 2011)

Correct, fast, maintainable: choose any three! - Bernard Blackham; Gernot Heiser (APSys, 2012)

To preempt or not to preempt, that is the question. - Bernard Blackham; Vernon Tang; Gernot Heiser (APSys, 2012)

Trustworthy Real-Time Systems. - Stefan M. Petters; Kevin Elphinstone; Gernot Heiser (Advances in Real-Time Systems, 2012)

Improving interrupt response time in a verifiable protected microkernel. - Bernard Blackham; Yao Shi; Gernot Heiser (EuroSys, 2012)

It's Time for Trustworthy Systems. - Gernot Heiser; Toby C. Murray; Gerwin Klein (IEEE Secur. Priv., 2012)

The systems hacker's guide to the galaxy energy usage in a modern smartphone. - Aaron Carroll; Gernot Heiser (APSys, 2013)

RapiLog: reducing system complexity through verification. - Gernot Heiser; Etienne Le Sueur; Adrian Danis; Aleksander Budzynowski; Tudor-Ioan Salomie; Gustavo Alonso (EuroSys, 2013)

The von Neumann Architecture Is Due for Retirement. - Aleksander Budzynowski; Gernot Heiser (HotOS, 2013)

Code optimizations using formally verified properties. - Yao Shi; Bernard Blackham; Gernot Heiser (OOPSLA, 2013)

Sequoll: A framework for model checking binaries. - Bernard Blackham; Gernot Heiser (IEEE Real-Time and Embedded Technology and Applications Symposium, 2013)

From L3 to seL4 what have we learnt in 20 years of L4 microkernels? - Kevin Elphinstone; Gernot Heiser (SOSP, 2013)

The Last Mile: An Empirical Study of Timing Channels on seL4. - David A. Cock; Qian Ge 001; Toby C. Murray; Gernot Heiser (CCS, 2014)

Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets. - Bernard Blackham; Mark H. Liffiton; Gernot Heiser (RTAS, 2014)

Unifying DVFS and offlining in mobile multicores. - Aaron Carroll; Gernot Heiser (RTAS, 2014)

Mobile multicores: use them or waste them. - Aaron Carroll; Gernot Heiser (ACM SIGOPS Oper. Syst. Rev., 2014)

File systems deserve verification too! - Gabriele Keller; Toby C. Murray; Sidney Amani; Liam O'Connor; Zilin Chen; Leonid Ryzhyk; Gerwin Klein; Gernot Heiser (ACM SIGOPS Oper. Syst. Rev., 2014)

Comprehensive formal verification of an OS microkernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Toby C. Murray; Thomas Sewell; Rafal Kolanski; Gernot Heiser (ACM Trans. Comput. Syst., 2014)

A Scalable Lock Manager for Multicores. - Hyungsoo Jung 001; Hyuck Han; Alan D. Fekete; Gernot Heiser; Heon Young Yeom (ACM Trans. Database Syst., 2014)

For a Microkernel, a Big Lock Is Fine. - Sean Peters; Adrian Danis; Kevin Elphinstone; Gernot Heiser (APSys, 2015)

Last-Level Cache Side-Channel Attacks are Practical. - Fangfei Liu; Yuval Yarom; Qian Ge 001; Gernot Heiser; Ruby B. Lee (IEEE Symposium on Security and Privacy, 2015)

Mapping the Intel Last-Level Cache. - Yuval Yarom; Qian Ge 001; Fangfei Liu; Ruby B. Lee; Gernot Heiser (IACR Cryptol. ePrint Arch., 2015)

CoGENT: Verifying High-Assurance File System Implementations. - Sidney Amani; Alex Hixon; Zilin Chen; Christine Rizkallah; Peter Chubb; Liam O'Connor; Joel Beeren; Yutaka Nagashima; Japheth Lim; Thomas Sewell; Joseph Tuong; Gabriele Keller; et al. (ASPLOS, 2016)

CATalyst: Defeating last-level cache side channel attacks in cloud computing. - Fangfei Liu; Qian Ge 001; Yuval Yarom; Frank McKeen; Carlos V. Rozas; Gernot Heiser; Ruby B. Lee (HPCA, 2016)

Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis. - Thomas Sewell; Felix Kam; Gernot Heiser (RTAS, 2016)

An Evaluation of Coarse-Grained Locking for Multicore Microkernels. - Kevin Elphinstone; Amirreza Zarrabi; Adrian Danis; Yanyan Shen; Gernot Heiser (CoRR, 2016)

Do Hardware Cache Flushing Operations Actually Meet Our Expectations? - Qian Ge 001; Yuval Yarom; Gernot Heiser (CoRR, 2016)

It's Time: OS Mechanisms for Enforcing Asymmetric Temporal Integrity. - Anna Lyons; Gernot Heiser (CoRR, 2016)

Report on the Asia-Pacific Systems Workshop 2015 (APSys'15). - Gernot Heiser; Kenji Kono; KyoungSoo Park; Robbert van Renesse (ACM SIGOPS Oper. Syst. Rev., 2016)

State of the Journal. - Paolo Montuschi; Edward J. McCluskey; Samarjit Chakraborty; Jason Cong; Ramón M. Rodríguez-Dagnino; Fred Douglis; Lieven Eeckhout; Gernot Heiser; Sushil Jajodia; Ruby B. Lee; Dinesh Manocha; Tomás F. Pena; et al. (IEEE Trans. Computers, 2016)

L4 Microkernels: The Lessons from 20 Years of Research and Deployment. - Gernot Heiser; Kevin Elphinstone (ACM Trans. Comput. Syst., 2016)

A Performance Evaluation of Rump Kernels as a Multi-server OS Building Block on seL4. - Kevin Elphinstone; Amirreza Zarrabi; Kent McLeod; Gernot Heiser (APSys, 2017)

The Cogent Case for Property-Based Testing. - Zilin Chen; Liam O'Connor; Gabriele Keller; Gerwin Klein; Gernot Heiser (PLOS@SOSP, 2017)

Technical Perspective: Proving file systems meet expectations. - Gernot Heiser (Commun. ACM, 2017)

High-assurance timing analysis for a high-assurance real-time operating system. - Thomas Sewell; Felix Kam; Gernot Heiser (Real Time Syst., 2017)

The Jury Is In: Monolithic OS Design Is Flawed: Microkernel-based Designs Improve Security. - Simon Biggs; Damon Lee; Gernot Heiser (APSys, 2018)

No Security Without Time Protection: We Need a New Hardware-Software Contract. - Qian Ge 001; Yuval Yarom; Gernot Heiser (APSys, 2018)

Scheduling-context capabilities: a principled, light-weight operating-system mechanism for managing time. - Anna Lyons; Kent McLeod; Hesham Almatary; Gernot Heiser (EuroSys, 2018)

Formally verified software in the real world. - Gerwin Klein; June Andronick; Matthew Fernandez; Ihor Kuz; Toby C. Murray; Gernot Heiser (Commun. ACM, 2018)

A Formal Approach to Constructing Secure Air Vehicle Software. - Darren D. Cofer; Andrew Gacek; John Backes; Michael W. Whalen; Lee Pike; Adam Foltzer; Michal Podhradsky; Gerwin Klein; Ihor Kuz; June Andronick; Gernot Heiser; Douglas Stuart (Computer, 2018)

Benchmarking Crimes: An Emerging Threat in Systems Security. - Erik van der Kouwe; Dennis Andriesse; Herbert Bos; Cristiano Giuffrida; Gernot Heiser (CoRR, 2018)

For Safety's Sake: We Need a New Hardware-Software Contract! - Gernot Heiser (IEEE Des. Test, 2018)

Roundtable: Machine Learning for Embedded Systems: Hype or Lasting Impact? - Xiaobo Sharon Hu; Rolf Ernst; Petru Eles; Gernot Heiser; Kurt Keutzer; Daehyun Kim; Tetsuya Tohdo (IEEE Des. Test, 2018)

A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. - Qian Ge 001; Yuval Yarom; David A. Cock; Gernot Heiser (J. Cryptogr. Eng., 2018)

Fault Tolerance Through Redundant Execution on COTS Multicores: Exploring Trade-Offs. - Yanyan Shen; Gernot Heiser; Kevin Elphinstone (DSN, 2019)

SoK: Benchmarking Flaws in Systems Security. - Erik van der Kouwe; Gernot Heiser; Dennis Andriesse; Herbert Bos; Cristiano Giuffrida (EuroS&P, 2019)

Time Protection: The Missing OS Abstraction. - Qian Ge 001; Yuval Yarom; Tom Chothia; Gernot Heiser (EuroSys, 2019)

Can We Prove Time Protection? - Gernot Heiser; Gerwin Klein; Toby C. Murray (HotOS, 2019)

seL4 in Australia: from research to real-world trustworthy systems. - Gernot Heiser; Gerwin Klein; June Andronick (Commun. ACM, 2020)

Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core. - Nils Wistoff; Moritz Schneider 001; Frank K. Gürkaynak; Luca Benini; Gernot Heiser (CoRR, 2020)

Benchmarking Flaws Undermine Security Research. - Erik van der Kouwe; Gernot Heiser; Dennis Andriesse; Herbert Bos; Cristiano Giuffrida (IEEE Secur. Priv., 2020)

Towards Provable Timing-Channel Prevention. - Gernot Heiser; Toby Murray; Gerwin Klein (ACM SIGOPS Oper. Syst. Rev., 2020)

Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core. - Nils Wistoff; Moritz Schneider 001; Frank K. Gürkaynak; Luca Benini; Gernot Heiser (DATE, 2021)

Property-Based Testing: Climbing the Stairway to Verification. - Zilin Chen; Christine Rizkallah; Liam O'Connor; Partha Susarla; Gerwin Klein; Gernot Heiser; Gabriele Keller (SLE, 2022)

Can We Put the "S" Into IoT? - Gernot Heiser; Lucy Parker; Peter Chubb; Ivan Velickovic; Ben Leslie (WF-IoT, 2022)

First steps in verifying the seL4 Core Platform. - Mathieu Paturel; Isitha Subasinghe; Gernot Heiser (APSys, 2023)

Verified Value Chains, Innovation and Competition. - Arnd Weber; Sylvain Guilley; René Rathfelder; Marc Stöttinger; Christoph Lüth; Maja Malenko; Torsten Grawunder; Steffen Reith; Armand Puccetti; Jean-Pierre Seifert; Norbert Herfurth; Hagen Sankowski; et al. (CSR, 2023)

Tutorial: Using the seL4 Microkernel. - Gernot Heiser; Ivan Velickovic (DSN-S, 2023)

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. - Robert Sison; Scott Buckley; Toby Murray; Gerwin Klein; Gernot Heiser (FM, 2023)

AutoCC: Automatic Discovery of Covert Channels in Time-Shared Hardware. - Marcelo Orenes-Vera; Hyunsung Yun; Nils Wistoff; Gernot Heiser; Luca Benini; David Wentzlaff; Margaret Martonosi (MICRO, 2023)

Pancake: Verified Systems Programming Made Sweeter. - Johannes Åman Pohjola; Hira Taqdees Syeda; Miki Tanaka; Krishnan Winter; Tsun Wang Sau; Benjamin Nott; Tiana J. Tsang Ung; Craig McLaughlin; Remy Seassau; Magnus O. Myreen; Michael Norrish; Gernot Heiser (PLOS@SOSP, 2023)

Proving the Absence of Microarchitectural Timing Channels. - Scott Buckley; Robert Sison; Nils Wistoff; Curtis Millar; Toby Murray; Gerwin Klein; Gernot Heiser (CoRR, 2023)

Systematic Prevention of On-Core Timing Channels by Full Temporal Partitioning. - Nils Wistoff; Moritz Schneider 001; Frank K. Gürkaynak; Gernot Heiser; Luca Benini (IEEE Trans. Computers, 2023)

fence.t.s: Closing Timing Channels in High-Performance Out-of-Order Cores Through ISA-Supported Temporal Partitioning. - Nils Wistoff; Gernot Heiser; Luca Benini (ApplePies, 2024)

Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance. - Gernot Heiser; Ivan Velickovic; Peter Chubb; Alwin Joshy; Anuraag Ganesh; Bill Nguyen; Cheng Li; Courtney Darville; Guangtao Zhu; James Archer; Jingyao Zhou; Krishnan Winter; et al. (CoRR, 2025)

Verifying Device Drivers with Pancake. - Junming Zhao; Alessandro Legnani; Tiana J. Tsang Ung; H. Truong; Tsun Wang Sau; Miki Tanaka; Johannes Åman Pohjola; Thomas Sewell; Robert Sison; Syeda Hira; Magnus Myreen; Michael Norrish; et al. (CoRR, 2025)