Publications, Theses and Technical Reports
| Paper/Talk Abstract |
|
Paper in PDF format |
|
| Presentation slides |
 |
Video of the presentation |  |
| A reference to a location |  | Paper yet to be published |  |
- Best papers from the Trustworthy Systems Group
- All publications from Trustworthy Systems ( 2026, 2025, 2024, 2023, 2022, 2021, 2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005, 2004, 2003, 2002, 2001, 2000, 1999, 1998, 1997, 1996, 1995, 1994, 1993, 1992 )
- Invited talks given by TS People ( 2025, 2024, 2023, 2022, 2021, 2020, 2019, 2018, 2017, 2016, 2015, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005 )
- Research theses
- Selected coursework student theses
Our Best Papers
|
|
|
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award |
|
|
|
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 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, Felix 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 |
|
|
|
Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith Additive and multiplicative notions of leakage, and their capacities Computer Security Foundations, pp. 308–322, Vienna, Austria, July, 2014 Winner of the 2015 NSA Best Scientific Cybersecurity Paper Award |
|
|
|
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 |
|
|
|
Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 471–481, Seattle, Washington, USA, June, 2013 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
|
|
|
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, 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 |
|
|
|
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 |
All TS Publications
2026
|
|
|
Kevin Tran, Johannes Åman Pohjola, Rob Sison and Gerwin Klein A rely-guarantee-based simulation for cooperative semantics International Colloquium on Theoretical Aspects of Computing, pp. 87–105, 2026 |
2025
|
|
|
Liam Murphy, Albert Rizaldi, Lesley Rossouw, Chen George, James Treloar, Hammond Pearce, Miki Tanaka and Gernot Heiser High-fidelity specification of real-world devices Workshop on Programming Languages and Operating Systems (PLOS), October, 2025 |
|
|
|
Gernot Heiser Trustworthy Systems R&D update Talk at the 7th seL4 Summit, September, 2025 |
|
|
|
Peter Chubb My home network Everything Open, Adelaide, SA, AU, January, 2025 |
|
|
|
Gernot Heiser, Ivan Velickovic, Peter Chubb, Alwin Joshy, Anuraag Ganesh, Bill Nguyen, Cheng Li, Courtney Darville, Guangtao Zhu, James Archer, Jingyao Zhou, Krishnan Winter, Lucy Parker, Szymon Duchniewicz and Tianyi Bai Fast, secure, adaptable: LionsOS design, implementation and performance arXiv preprint, January, 2025 |
|
|
|
Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser Verifying device drivers with Pancake arXiv preprint, January, 2025 |
2024
|
|
|
Rob Sison Verification status of time protection and Microkit-based OS services Talk at the 6th seL4 Summit, October, 2024 |
|
|
|
Nils Wistoff, Gernot Heiser and Luca Benini fence.t.s: Closing timing channels in high-performance out-of-order cores through ISA-supported temporal partitioning International Conference on Applications in Electronics Pervading Industry, Environment and Society (ApplePies), Turin, IT, September, 2024 |
|
|
|
Trudy Weibel, Zoltan A. Kocsis, Mathieu Paturel, Robert Sison, Isitha Subasinghe and Gernot Heiser Verifying the seL4 Microkit https://trustworthy.systems/publications/papers/Weibel_KPSSH_24.pdf, June, 2024 |
|
|
|
Nils Wistoff, Robert Balas, Alessandro Ottaviano, Gernot Heiser and Luca Benini ISA support for hardware resource partitioning in RISC-V RISC-V Summit Europe, Munich, DE, June, 2024 |
|
|
|
Peter Chubb Running your own mailserver Everything Open, Gladstone, QLD, AU, April, 2024 |
|
|
|
Gernot Heiser Lions OS: secure – fast – adaptable 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 2024 |
2023
|
|
|
Marcelo Orenes-Vera, Hyunsung Yun, Nils Wistoff, Gernot Heiser, Luca Benini, David Wentzlaff and Margaret Martonosi AutoCC: Automatic discovery of covert channels in time-shared hardware International Symposium on Microarchitecture (MICRO), Toronto, ON, CA, October, 2023 |
|
|
|
Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Tsun Wang Sau, Benjamin Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus O. Myreen, Michael Norrish and Gernot Heiser Pancake: verified systems programming made sweeter Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 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 |
|
|
|
Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser Formalising the prevention of microarchitectural timing channels by operating systems International Symposium on Formal Methods (FM), Lübeck, DE, March, 2023 |
|
|
|
Zilin Chen, Ambroise Lafont, Liam O’Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson and Christine Rizkallah Dargent: A silver bullet for verified data layout refinement Proc. ACM Program. Lang., Volume 7, Number POPL, January, 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 |
|
|
|
Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein and Gernot Heiser Proving the absence of microarchitectural timing channels arXiv preprint arXiv:2310.17046, 2023 |
|
|
|
Gernot Heiser R&D update from Trustworthy Systems Talk at the 5th seL4 Summit, 2023 |
|
|
|
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola and Riccardo Zanetti PureCake: A verified compiler for a lazy functional language Proceedings of the ACM on Programming Languages, Volume 7, Number PLDI, pp. 952–976, 2023 |
|
|
|
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Gernot Heiser and Luca Benini Systematic prevention of on-core timing channels by full temporal partitioning IEEE Transactions on Computers, Volume 72, Number 5, pp. 1420–1430, 2023 |
2022
|
|
|
Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser and Gabriele Keller Property-based testing: Climbing the stairway to verification ACM SIGPLAN International Conference on Software Language Engineering, Auckland, New Zealand, December, 2022 Distinguished Artifact Award |
|
|
|
Gernot Heiser, Lucy Parker, Peter Chubb, Ivan Velickovic and Ben Leslie Can we put the "S" into IoT? IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022 |
|
|
|
Lucy Parker The seL4 device driver framework Talk at the 4th seL4 Summit, October, 2022 |
|
|
|
Arve Gengelbach and Johannes Åman Pohjola A verified cyclicity checker: For theories with overloaded constants International Conference on Interactive Theorem Proving, pp. 15:1–15:18, Haifa, Israel, August, 2022 |
|
|
|
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker and Michael Norrish Kalas: A verified, end-to-end compiler for a choreographic language International Conference on Interactive Theorem Proving, pp. 27:1–27:18, Haifa, Israel, August, 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 Foundation – growing through upheaval On-line, January, 2022 |
|
|
|
Mário Alvim, Natasha Fernandes, Annabelle McIver, Carroll Morgan and Gabriel Nunes Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata Proc. Priv. Enhancing Technol. 2022(4), pp. 378–99, 2022 |
2021
|
|
|
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser Microarchitectural timing channels and their prevention on an open-source 64-bit RISC-V core Design, Automation and Test in Europe (DATE), virtual, February, 2021 Best Paper Award |
|
|
|
Richard S. Bird, Jeremy Gibbons, Ralf Hinze, Peter Höfner, Johan Jeuring, Lambert G. L. T. Meertens, Bernhard Möller, Carroll Morgan, Tom Schrijvers, Wouter Swierstra and Nicolas Wu Algorithmics Volume 600 in IFIP Advances in Information and Communication Technology. Springer, 2021 |
|
|
|
Natasha Fernandes, Annabelle McIver and Carroll Morgan The Laplace mechanism has optimal utility for differential privacy over continuous queries 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021 |
|
|
|
Liam O’Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell and Gabriele Keller Cogent: Uniqueness types and certifying compilation Journal of Functional Programming, Volume 31, 2021 |
|
|
|
Robert Sison and Toby Murray Verified secure compilation for mixed-sensitivity concurrent programs Journal of Functional Programming, Volume 31, pp. e18, 2021 |
2020
|
|
|
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Logical Methods in Computer Science, Volume 16, Issue 4, pp. 16:1-16:28, December, 2020 |
|
|
|
Jeremy Gibbons, Annabelle McIver, Carroll Morgan and Tom Schrijvers Quantitative information flow with monads in Haskell Foundations of Probabilistic Programming, pp. 391–448, Cambridge University Press, 2020 |
|
|
|
Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus Myreen and Yong Kiam Tan Do you have space for dessert? A verified space cost semantics for CakeML programs OOPSLA, pp. 204:1-29, Chicago, IL, November, 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 |
|
|
|
Michael Norrish and Yiming Xu Mechanised modal model theory International Joint Conference on Automated Reasoning, pp. 518-533, Paris, July, 2020 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Formal reasoning under cached address translation Journal of Automated Reasoning, Volume 64, Issue 6, pp. 911-945, June, 2020 |
|
|
|
Johannes Åman Pohjola and Arve Gengelbach A mechanised semantics for HOL with ad-hoc overloading LPAR23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 498-515, Alicante, Spain, May, 2020 |
|
|
|
Gernot Heiser The seL4 microkernel – an introduction seL4 Foundation Whitepaper, May, 2020 |
|
|
|
Erik van der Kouwe, Gernot Heiser, Dennis Andriesse, Herbert Bos and Cristiano Giuffrida Benchmarking flaws undermine security research IEEE Security and Privacy Magazine, Volume 18, Issue 3, May, 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 |
|
|
|
Konrad Slind, David Hardin, Johannes Åman Pohjola and Michael Sproul Synthesis of verified architectural components for autonomy hosted on a verified microkernel Hawaii International Conference on System Sciences, pp. 6365-6374, Grand Wilea, Hawaii, January, 2020 |
|
|
|
Annabelle McIver and Carroll Morgan Correctness by construction for probabilistic programs Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles—9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I, pp. 216–239, 2020 |
2019
|
|
|
Johannes Åman Pohjola, Henrik Rostedt and Magnus Myreen Characteristic formulae for liveness properties of non-terminating CakeML programs International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019 |
|
|
|
Ihor Kuz Building trustworthy systems on seL4 seL4 Summit, Herndon, VA, USA, September, 2019 |
|
|
|
Robert Sison and Toby Murray Verifying that a compiler preserves concurrent value-dependent information-flow security International Conference on Interactive Theorem Proving, pp. 27:1–27:19, Portland, USA, September, 2019 |
|
|
|
Adam Sandberg Ericsson, Magnus Myreen and Johannes Åman Pohjola A verified generational garbage collector for CakeML Journal of Automated Reasoning, Volume 63, Issue 2, pp. 463–488, August, 2019 |
|
|
|
Gidon Ernst and Toby Murray SecCSL: security concurrent separation logic International Conference on Computer Aided Verification, pp. 208–230, July, 2019 |
|
|
|
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality FORTE 2019: International Conference on Formal Techniques for Distributed Systems, pp. 3-20, Lyngby, Denmark, June, 2019 Best paper award |
|
|
|
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus Myreen, Michael Norrish, Oskar Abrahamsson and Anthony Fox Verified compilation on a verified processor ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 1041-1053, Phoenix, AZ, US, June, 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 |
|
|
|
Erik van der Kouwe, Gernot Heiser, Dennis Andriesse, Herbert Bos and Cristiano Giuffrida SoK: benchmarking flaws in systems security European Conference on Security and Privacy (EuroS&P), Stockholm, Sweden, 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 |
|
|
|
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Technical Report, Data61, CSIRO, April, 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 |
|
|
|
Carroll Morgan, Annabelle McIver and Tahiry Rabehaja Abstract hidden Markov models: A monadic account of quantitative information flow Mathematical Structures in Computer Science, Volume 15, Issue 1, pp. 36:1-36:50, March, 2019 |
|
|
|
Hing-Lun Chan and Michael Norrish Proof pearl: Bounding least common multiples with triangles Journal of Automated Reasoning, Volume 62, Issue 2, pp. 171-192, February, 2019 |
|
|
|
Gernot Heiser What's new in the world of seL4? Talk at FOSDEM'19, Brussels, February, 2019 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish The verified CakeML compiler backend Journal of Functional Programming, Volume 29, February, 2019 |
|
|
|
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith and Keith Wanbrough Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API Journal of the ACM, Volume 66, Issue 1, January, 2019 |
|
|
|
Zilin Chen, Matt Di Meglio, Liam O'Connor, Partha Susarla Ajay, Christine Rizkallah and Gabriele Keller A data layout description language for Cogent at PriSC, Lisbon, Portugal, January, 2019 |
|
|
|
Mário S. Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith An axiomatization of information flow measures Theoretical Computer Science, Volume 777, pp. 32-54, 2019 |
|
|
|
Annabelle McIver and Carroll Morgan Proving that programs are differentially private Programming Languages and Systems, pp. 3–18, 2019 |
|
|
|
Tahiry Rabehaja, Annabelle McIver, Carroll Morgan and Georg Struth Categorical information flow The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 329–343, Springer International Publishing, 2019 |
2018
|
|
|
Milad Ghale, Dirk Pattinson, Ramana Kumar and Michael Norrish Verified certificate checking for counting votes Verified Software: Theories, Tools and Experiments, pp. 69–87, Oxford, December, 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 |
|
|
|
Hugo Feree, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus Myreen and Son Ho Program verification in the presence of I/O: semantics, verified library routines, and verified applications Verified Software: Theories, Tools and Experiments, pp. 88-111, Oxford, UK, November, 2018 |
|
|
|
X. Sharon Hu, Rolf Ernst, Petru Eles, Gernot Heiser, Kurt Keutzer, Daehyun Kim and Tetsuya Tohdo Roundtable: Machine learning for embedded systems IEEE Design and Test, Volume 35, Issue 6, pp. 86-93, November, 2018 |
|
|
|
Liam O'Connor, Zilin Chen, Partha Susarla Ajay, Christine Rizkallah, Gerwin Klein and Gabriele Keller Bringing effortless refinement of data layouts to Cogent International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 134-149, Limassol, Cyprus, November, 2018 |
|
|
|
Callum Bannister and Peter Höfner False failure: Creating failure models for separation logic 17th International Conference on Relational and Algebraic Methods in Computer Science, pp. 263-279, Groningen, October, 2018 |
|
|
|
Alejandro Gómez-Londoño and Johannes Åman Pohjola Connecting choreography languages with verified stacks at Nordic Workshop on Programming Theory, Oslo, Norway, October, 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 |
|
|
|
Qian Ge, Yuval Yarom and Gernot Heiser No security without time protection: we need a new hardware-software contract Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018 Best Paper Award Complete timing-channel data for evaluated x86 and Arm platforms. |
|
|
|
Callum Bannister, Peter Höfner and Gerwin Klein Backwards and forwards with separation logic International Conference on Interactive Theorem Proving, pp. 68–87, Oxford, July, 2018 |
|
|
|
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus Myreen, Yong Kiam Tan and Michael Norrish Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions International Joint Conference on Automated Reasoning, pp. 646-662, Oxford, July, 2018 |
|
|
|
Simon Jantsch and Michael Norrish Verifying the LTL to Büchi automata translation via very weak alternating automata International Conference on Interactive Theorem Proving, pp. 306-323, Oxford, July, 2018 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Program verification in the presence of cached address translation International Conference on Interactive Theorem Proving, pp. 542-559, Oxford, UK, July, 2018 |
|
|
|
Qian Ge, Yuval Yarom, David Cock and Gernot Heiser A survey of microarchitectural timing attacks and countermeasures on contemporary hardware Journal of Cryptographic Engineering, Volume 8, Issue 1, pp. 1-27, 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 |
|
|
|
Toby Murray, Robert Sison and Kai Engelhardt COVERN: A logic for compositional verification of information flow control European Conference on Security and Privacy (EuroS&P), London, UK, 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 |
|
|
|
Kunshan Wang, Stephen Blackburn, Tony Hosking and Michael Norrish Hop, skip, & jump: Practical on-stack replacement for a cross-platform language-neutral VM International Conference on Virtual Execution Environments, pp. 1-16, Williamsburg, VA, March, 2018 |
|
|
|
Gernot Heiser Flying autonomous aircraft: Mixed-criticality support in seL4 at linux.conf.au, Sydney, January, 2018 |
|
|
|
Annabelle McIver, Carroll Morgan, Benjamin Kaminski and Joost-Pieter Katoen A new proof rule for almost-sure termination ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, January, 2018 |
|
|
|
Robert Sison Per-thread compositional compilation for confidentiality-preserving concurrent programs 2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018 |
|
|
|
Solrun Halla Einarsdottir, Moa Johansson and Johannes Åman Pohjola Into the infinite - theory exploration for coinduction Artificial Intelligence and Symbolic Computation, pp. 70-86, Suzhou, China, 2018 |
2017
|
|
|
June Andronick From Hoare logic to Owicki-Gries and rely-guarantee for interruptible eChronos and multicore seL4 International Colloquium on Theoretical Aspects of Computing (ICTAC), pp. XIII-XV, Hanoi, Vietnam, October, 2017 |
|
|
|
Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein and Gernot Heiser The Cogent case for property-based testing Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Shanghai, China, October, 2017 |
|
|
|
Annabelle McIver, Tahiry Rabehaja, Roland Wen and Carroll Morgan Privacy in elections: How small is "small"? Journal of Information Security and Applications, Volume 36, Issue 1, pp. 112-126, October, 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 Zarraby, 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 |
|
|
|
Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor Provably trustworthy systems Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017 |
|
|
|
Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen Verifying efficient function calls in CakeML International Conference on Functional Programming, Oxford, 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 |
|
|
|
Nicolas Bordenabe, Annabelle McIver, Carroll Morgan and Tahiry Rabehaja Reasoning about distributed secrets FORTE, pp. 156-170, Shanghai, June, 2017 |
|
|
|
Annabelle McIver, Carroll Morgan and Tahiry Rabehaja Algebra for quantitative information flow International Conference on Relational and Algebraic Methods in Computer Science, pp. 3–23, Lyon, France, May, 2017 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Reasoning about translation lookaside buffers International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 490–508, Maun, Botswana, May, 2017 |
|
|
|
Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish Verified characteristic formulae for CakeML European Symposium on Programming, pp. 584-610, Uppsala, April, 2017 |
|
|
|
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joey Tuong COMPLX: A verification framework for concurrent imperative programs International Conference on Certified Programs and Proofs, pp. 138–150, Paris, France, January, 2017 |
|
|
|
Anthony Fox, Magnus Myreen, Yong Kiam Tan and Ramana Kumar Verified compilation of CakeML to multiple machine-code targets International Conference on Certified Programs and Proofs, pp. 125–137, Paris, France, January, 2017 |
|
|
|
Carroll Morgan A demonic lattice of information Concurrency, Security, and Puzzles — Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 203–222, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017 |
|
|
|
Qian Ge, Yuval Yarom, Frank Li and Gernot Heiser Your processor leaks information — and there's nothing you can do about it arXiv preprint, 2017 |
2016
|
|
|
Mark Beaumont, Jim McCarthy and Toby Murray The Cross Domain Desktop Compositor: Using hardware-based video compositing for a multi-level secure user interface Annual Computer Security Applications Conference (ACSAC), December, 2016 |
|
|
|
Yutaka Nagashima and Liam O'Connor Close encounters of the higher kind — emulating constructor classes in standard ML Abstract, ACM SIGPLAN Workshop on ML, September, 2016. |
|
|
|
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein Refinement through restraint: Bringing down the cost of verification International Conference on Functional Programming, Nara, Japan, September, 2016 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish A new verified compiler backend for CakeML International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016 |
|
|
|
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah Proof of OS scheduling behavior in the presence of interrupt-induced concurrency International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016 |
|
|
|
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein A framework for the automatic formal verification of refinement from Cogent to C International Conference on Interactive Theorem Proving, Nancy, France, August, 2016 |
|
|
|
Yong Kiam Tan, Scott Owens and Ramana Kumar A verified type system for CakeML Implementation and application of functional and programming languages, pp. 12, Koblenz, Germany, July, 2016 Winner: 2016 Peter Landin Prize for best paper |
|
|
|
Mario Alvim, Kostantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith Axioms for information leakage Computer Security Foundations, pp. 77-92, Lisbon, June, 2016 |
|
|
|
Yi Lin, Steve Blackburn, Tony (Antony) Hosking and Michael Norrish Rust as a language for high performance GC implementation International Symposium on Memory Management, pp. 89–98, Santa Barbara, California, USA, June, 2016 |
|
|
|
Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah Compositional verification and refinement of concurrent value-dependent noninterference IEEE Computer Security Foundations Symposium, pp. 417–431, Lisbon, Portugal, June, 2016 |
|
|
|
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, Toby Murray, Gerwin Klein and Gernot Heiser Cogent: verifying high-assurance file system implementations International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175–188, Atlanta, GA, USA, April, 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, Felix 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 |
|
|
|
Fangfei Liu, Qian Ge, Yuval Yarom, Frank Mckeen, Carlos Rozas, Gernot Heiser and Ruby B Lee CATalyst: defeating last-level cache side channel attacks in cloud computing IEEE Symposium on High-Performance Computer Architecture, pp. 406–418, Barcelona, Spain, March, 2016 |
|
|
|
Daniel Matichuk, Toby Murray and Makarius Wenzel Eisbach: A proof method language for isabelle Journal of Automated Reasoning, Volume 56, Number 3, pp. 261–282, March, 2016 |
2015
|
|
|
Sidney Amani and Toby Murray Specifying a realistic file system Workshop on Models for Formal Analysis of Real Systems, pp. 1–9, Suva, Fiji, November, 2015 |
|
|
|
June Andronick, Corey Lewis and Carroll Morgan Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015 |
|
|
|
Paul Rimba, Liming Zhu, Len Bass, Ihor Kuz and Steve Reeves Composing patterns to construct secure systems European Dependable Computing Conference, pp. 213–224, Paris, France, September, 2015 |
|
|
|
Yuval Yarom, Qian Ge, Fangfei Liu, Ruby B. Lee and Gernot Heiser Mapping the Intel last-level cache The Cryptology ePrint Archive, September, 2015 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Verified over-approximation of the diameter of propositionally factored transition systems International Conference on Interactive Theorem Proving, pp. 1–16, Nanjing, China, August, 2015 |
|
|
|
Joseph Chan and Michael Norrish Mechanisation of AKS algorithm: Part 1 — the main theorem International Conference on Interactive Theorem Proving, pp. 117–136, Nanjing, China, August, 2015 |
|
|
|
Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of a component platform Technical Report, NICTA and UNSW, August, 2015 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Exploiting symmetries by planning for a descriptive quotient International Joint Conference on Artificial Intelligence, pp. 1479–1486, Buenos Aires, July, 2015 |
|
|
|
Jasmin Blanchette, Maximilian Haslbeck, Daniel Matichuk and Tobias Nipkow Mining the archive of formal proofs Conference on Intelligent Computer Mathematics, pp. 3–17, Washington DC, USA, July, 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 |
|
|
|
Carroll Morgan, Annabelle McIver and Tahiry Rabehaja Abstract hidden Markov models: A monadic account of quantitative information flow Annual IEEE Symposium on Logic in Computer Science, pp. 597–608, Tokyo, Japan, July, 2015 |
|
|
|
Toby Murray On high-assurance information-flow-secure programming languages ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 43–48, Prague, Czech Republic, 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 |
|
|
|
Peter Gammie, Tony (Antony) Hosking and Kai Engelhardt Relaxing safely: verified on-the-fly garbage collection for x86-TSO ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 11, Portland, OR, US, June, 2015 |
|
|
|
Yi Lin, Stephen M. Blackburn, Kunshan Wang, Tony (Antony) Hosking and Michael Norrish Stop and go: Understanding yieldpoint behavior International Symposium on Memory Management, pp. 70–80, Portland, OR, USA, June, 2015 |
|
|
|
Carroll Morgan a nondeterministic lattice of information One-hour invited talk at Mathematics of Program Construction, Königswinter, Germany, June, 2015 |
|
|
|
Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser and Ruby B Lee Last-level cache side-channel attacks are practical IEEE Symposium on Security and Privacy, pp. 605–622, San Jose, CA, US, May, 2015 |
|
|
|
Michael Norrish and Michelle Mills Strout An approach for proving the correctness of inspector/executor transformations Languages and Compilers for Parallel Computing, pp. 131–145, Hillsboro, Oregon, USA, May, 2015 |
|
|
|
Franck Cassez, Takashi Matsuoka, Edward Pierzchalski and Nathan Smyth Perentie: Modular trace refinement and selective value tracking SV-COMP-2015, pp. 439–442, London, UK, April, 2015 |
|
|
|
Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples Empirical study towards a leading indicator for cost of formal software verification International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015 |
|
|
|
Peter Chubb SD cards and filesystems for embedded systems linux.conf.au, Auckland, NZ, January, 2015 |
|
|
|
Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk SAT-based strategy extraction in reachability games AAAI, Austin, TX, USA, January, 2015 |
|
|
|
Gernot Heiser seL4 is free — what does this mean for you? Abstract, LCA. |
|
|
|
Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray An empirical research agenda for understanding formal methods productivity Information and Software Technology, Volume 60, pp. 102–112, January, 2015 |
|
|
|
Annabelle McIver, Larissa Meinicke and Carroll Morgan Hidden-markov program algebra with iteration Mathematical Structures in Computer Science, Volume 25, Number 2, pp. 320–360, 2015 |
2014
|
|
|
Hyungsoo Jung, Hyuck Han, Alan Fekete, Gernot Heiser and Heon Yeom A scalable lock manager for multicores ACM Transactions on Database Systems, Volume 39, Number 4, pp. 29:1–29:29, December, 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 |
|
|
|
David Cock, Qian Ge, Toby Murray and Gernot Heiser The last mile: An empirical study of some timing channels on seL4 ACM Conference on Computer and Communications Security, pp. 570–581, Scottsdale, AZ, USA, November, 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 |
|
|
|
Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah CDSL version 1: Simplifying verification with linear types Technical Report, NICTA, 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 |
|
|
|
Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski Productivity for proof engineering Empirical Software Engineering and Measurement, pp. 15, Turin, Italy, September, 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 |
|
|
|
Yuxin Deng, Robert van Glabbeek, Matthew Hennessy and Carroll Morgan Real reward testing for probabilistic processes Theoretical Computer Science, Volume 538, pp. 16–36, July, 2014 |
|
|
|
Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk Interpolants in two-player games Abstract, iPRA workshop, July, 2014. |
|
|
|
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish Beagle as a HOL4 external ATP method Practical Aspects of Automated Reasoning, pp. 50–59, Vienna, July, 2014 |
|
|
|
Alexander Legg, Nina Narodytska and Leonid Ryzhyk Practical CNF interpolants via BDDs Abstract, iPRA workshop, July, 2014. |
|
|
|
Daniel Matichuk, Makarius Wenzel and Toby Murray An Isabelle proof method language International Conference on Interactive Theorem Proving, pp. 390–405, Vienna, Austria, July, 2014 |
|
|
|
Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith Additive and multiplicative notions of leakage, and their capacities Computer Security Foundations, pp. 308–322, Vienna, Austria, July, 2014 Winner of the 2015 NSA Best Scientific Cybersecurity Paper Award |
|
|
|
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 |
|
|
|
Daniel Potts, Rene Bourquin, Leslie Andresen, June Andronick, Gerwin Klein and Gernot Heiser Mathematically verified software kernels: Raising the bar for high assurance implementations Technical Report, NICTA, July, 2014 |
|
|
|
Thomas Sewell Formal replay of translation validation for highly optimised c: Work in progress Verification and Program Transformation, Vienna, Austria, July, 2014 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Mechanising theoretical upper bounds in planning Workshop on Knowledge Engineering for Planning and Scheduling, Portsmouth, USA, June, 2014 |
|
|
|
David Greenaway, Japheth Lim, June Andronick and Gerwin Klein Don't sweat the small stuff: Formal verification of C code without the pain ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 429–439, Edinburgh, UK, June, 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 |
|
|
|
Gerwin Klein Proof engineering challenges for large-scale verification Abstract, AI4FM/2014 Workshop. |
|
|
|
Gerwin Klein and Tobias Nipkow Applications of interactive proof to data flow analysis and security Software Systems Safety, pp. 77–134, Volume 36 in NATO Science for Peace and Security Series , IOS Press BV, 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 Proof engineering considered essential International Symposium on Formal Methods (FM), pp. 16–21, Singapore, April, 2014 |
|
|
|
Carroll Morgan, Annabelle McIver, Geoffrey Smith, Barbara Espinoza and Larisa Meinicke Abstract channels and their robust information-leakage ordering Principles of Security and Trust (ETAPS), pp. 83–102, Grenoble, France, April, 2014 |
|
|
|
Aditi Barthwal and Michael Norrish A mechanisation of some context-free language theory in HOL4 Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 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 |
|
|
|
Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens CakeML: A verified implementation of ML ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014 |
2013
|
|
|
Joseph Chan and Michael Norrish A string of pearls: Proofs of fermat's little theorem Journal of Formal Reasoning, Volume 6, Number 1, pp. 63–87, December, 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 |
|
|
|
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 |
|
|
|
Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser File systems deserve verification too! Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, Pennsylvania, USA, November, 2013 A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64. |
|
|
|
Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell Formally verified system initialisation International Conference on Formal Engineering Methods, pp. 70–85, Queenstown, New Zealand, October, 2013 |
|
|
|
Yao Shi, Bernard Blackham and Gernot Heiser Code optimizations using formally verified properties Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 427–442, Indianapolis, USA, October, 2013 |
|
|
|
Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish Tableaux for verification of data-centric processes Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28–43, Nancy, France, September, 2013 |
|
|
|
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 |
|
|
|
Michael Norrish and Brian Huffman Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω1 International Conference on Interactive Theorem Proving, pp. 133–146, Rennes, France, July, 2013 |
|
|
|
Hyungsoo Jung, Hyuck Han, Alan Fekete, Gernot Heiser and Heon Y. Yeom A scalable lock manager for multicores ACM SIGMOD Conference, pp. 73–84, New York, USA, June, 2013 Honorable Mention Award |
|
|
|
Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 471–481, Seattle, Washington, USA, June, 2013 |
|
|
|
Aleksander Budzynowski and Gernot Heiser The von Neumann architecture is due for retirement Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, Santa Ana Pueblo, NM, USA, May, 2013 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
|
|
|
Toby Murray and Thomas Sewell Above and beyond: seL4 noninterference and binary verification Abstract, 2013 High Confidence Software and Systems Conference, Annapolis, MD, May, 2013. |
|
|
|
Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass Formal specifications better than function points for code sizing International Conference on Software Engineering, pp. 1257–1260, San Francisco, USA, May, 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 |
|
|
|
Tudor-Ioan Salomie, Gustavo Alonso, Timothy Roscoe and Kevin Elphinstone Application level ballooning for efficient server consolidation EuroSys Conference, pp. 337–350, Prague, Czech Republic, April, 2013 |
|
|
|
Toby Murray On the limits of refinement-testing for model-checking CSP Formal Aspects of Computing, Volume 25, Number 2, pp. 219–256, February, 2013 |
2012
|
|
|
Daniel Matichuk and Toby Murray Extensible specifications for automatic re-use of specifications and proofs 10th International Conference on Software Engineering and Formal Methods, pp. 8, Thessaloniki, Greece, December, 2012 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein Noninterference for operating system kernels International Conference on Certified Programs and Proofs, pp. 126–142, Kyoto, Japan, December, 2012 |
|
|
|
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Automatic verification of message-based device drivers Systems Software Verification, pp. 1–14, Sydney, Australia, November, 2012 |
|
|
|
Daniel Matichuk Automatic function annotations for hoare logic Systems Software Verification, pp. 10, Sydney, Australia, November, 2012 |
|
|
|
June Andronick, Andrew Boyton and Gerwin Klein Final report for AOARD grant #FA2386-11-1-4070, formal system verification — extension Technical Report, NICTA, October, 2012 |
|
|
|
June Andronick, Gerwin Klein and Toby Murray Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105 Technical Report, NICTA, October, 2012 |
|
|
|
Hing-Lun Chan and Michael Norrish A string of pearls: Proofs of fermat’s little theorem International Conference on Certified Programs and Proofs, pp. 188–207, Kyoto, Japan, October, 2012 |
|
|
|
Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012 |
|
|
|
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Active device drivers Technical Report, NICTA, September, 2012 |
|
|
|
Nick Barnes, Peter Baumgartner, Tiberio Caetano, Hugh Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter Stuckey, Sylvie Thiebaux, Pascal Van Hentenryck and Toby Walsh AI @ NICTA AI Magazine, Volume 33, Number 3, pp. 115–127, September, 2012 |
|
|
|
June Andronick and Gerwin Klein Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022 Technical Report, NICTA, August, 2012 |
|
|
|
James Cheney, Michael Norrish and René Vestergaard Formalizing adequacy: A case study for higher-order abstract syntax Journal of Automated Reasoning, Volume 49, Number 2, pp. 209–239, August, 2012 |
|
|
|
David Greenaway, June Andronick and Gerwin Klein Bridging the gap: Automatic verified abstraction of C International Conference on Interactive Theorem Proving, pp. 99–115, Princeton, New Jersey, USA, August, 2012 |
|
|
|
Gerwin Klein, Rafal Kolanski and Andrew Boyton Mechanised separation algebra International Conference on Interactive Theorem Proving, pp. 332–337, Princeton, USA, August, 2012 |
|
|
|
Ihor Kuz, Liming Zhu, Len Bass, Mark Staples and Xiwei (Sherry) Xu An architectural approach for cost effective trustworthy systems IEEE/IFIP Working Conference on Software Architecture (WICSA), pp. 325–328, Helsinki, Finland, August, 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 |
|
|
|
Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski Challenges and experiences in managing large-scale proofs Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, pp. 32–48, Bremen, Germany, July, 2012 |
|
|
|
June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He (Jason) Zhang and Liming Zhu Large-scale formal verification in practice: A process perspective International Conference on Software Engineering, pp. 1002–1011, Zurich, Switzerland, June, 2012 |
|
|
|
He (Jason) Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski Simulation modeling of a large scale formal verification process International Conference on Software and Systems Process, pp. 3–12, Zurich, Switzerland, June, 2012 |
|
|
|
June Andronick, Gerwin Klein and Andrew Boyton Formal system verification — extension, AOARD 114070 Technical Report, NICTA, May, 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 |
|
|
|
Matthew Fernandez, Gerwin Klein and Ihor Kuz Microkernel verification down to assembly Poster presented at EuroSys 2012, April, 2012 |
|
|
|
Gerwin Klein Interactive proof: Applications to semantics Software Safety and Security: Tools for Analysis and Verification, pp. 85–125, IOS Press, 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 |
|
|
|
Peter Chubb Bourne shell tutorial Tutorial at Linux.conf.au, Ballarat, January, 2012 |
|
|
|
Peter Chubb Linux as a boot loader Talk at linux.conf.au, Ballarat, January, 2012 |
|
|
|
Stefan M. Petters, Kevin Elphinstone and Gernot Heiser Trustworthy real-time systems Advances in Real-Time Systems, pp. 191–206, Springer, 2012 |
2011
|
|
|
June Andronick, Gerwin Klein and Toby Murray Formal system verification for trustworthy embedded systems, final report option 1 — AOARD 104105 Technical Report, NICTA, November, 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 |
|
|
|
Michael Norrish Mechanised computability theory International Conference on Interactive Theorem Proving, pp. 297—311, Nijmegen, The Netherlands, August, 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 |
|
|
|
Sidney Amani, Leonid Ryzhyk, Alastair Donaldson, Gernot Heiser, Alexander Legg and Yanjin Zhu Static analysis of device drivers: we can do better! Asia-Pacific Workshop on Systems (APSys), pp. 1–5, Shanghai, China, July, 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 |
|
|
|
Yuxin Deng, Robert van Glabbeek, Matthew Hennessy and Carroll Morgan Real reward testing for probabilistic processes (extended abstract) Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), pp. 61–73, Saarbrücken, Germany, 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 |
|
|
|
Han-Hing Dang, Bernhard Möller and Peter Höfner Algebraic separation logic The Journal of Logic and Algebraic Programming, Volume 80, Number 6, pp. 221–247, June, 2011 |
|
|
|
Gernot Heiser Virtualizing embedded systems — why bother? Design Automation Conference (DAC), pp. 901–905, Dan Diego, CA, USA, 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 |
|
|
|
June Andronick and Gerwin Klein Formal system verification for trustworthy embedded systems, final report AOARD 094160 Technical Report, NICTA, April, 2011 |
|
|
|
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved device driver reliability through hardware verification reuse International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 1–12, Newport Beach, CA, USA, March, 2011 |
2010
|
|
|
June Andronick From a proven correct microkernel to trustworthy large systems International Conference on Formal Verification of Object-Oriented Software, pp. 1–9, Paris, December, 2010 |
|
|
|
Gerwin Klein From a verified kernel towards verified systems Asian Symposium on Programming Languages and Systems (APLAS), pp. 21–33, Shanghai, China, November, 2010 Invited extended abstract. |
|
|
|
June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Systems Software Verification, pp. 9, Vancouver, CA, October, 2010 |
|
|
|
Yuxin Deng and Robert van Glabbeek Characterising probabilistic processes logically (extended abstract) International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 278–293, Yogyakarta, Indonesia, October, 2010 |
|
|
|
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The road to trustworthy systems ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3–10, Chicago, IL, USA, October, 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 |
|
|
|
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved device driver reliability through verification reuse Workshop on Hot Topics in System Dependability, pp. 1–6, Vancouver, Canada, October, 2010 |
|
|
|
Aditi Barthwal and Michael Norrish A formalisation of the normal forms of context-free grammars in HOL4 19th EACSL Annual Conferences on Computer Science Logic, pp. 95–109, Brno, Czech Republic, August, 2010 |
|
|
|
Nicholas Fitzroy-Dale, Ihor Kuz and Gernot Heiser Architecture optimisation with Currawong Asia-Pacific Workshop on Systems (APSys), pp. 7–12, New Delhi, India, August, 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 |
|
|
|
Gerwin Klein The l4.verified project – next steps Verified Software: Theories, Tools and Experiments, pp. 86–96, Edinburgh, UK, 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 |
|
|
|
Aditi Barthwal and Michael Norrish Mechanisation of PDA and grammar equivalence for context-free languages 17th Workshop on Logic, Language, Information and Computation , pp. 125–135, Brasília, Brazil, July, 2010 |
|
|
|
Gerwin Klein A formally verified OS kernel. now what? International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010 |
|
|
|
Ramana Kumar and Michael Norrish (nominal) unification by recursive descent with triangular substitutions International Conference on Interactive Theorem Proving, pp. 51–66, 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 |
|
|
|
Gerwin Klein, Thomas Sewell and Simon Winwood Refinement in the formal verification of seL4 Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323–339, Springer, 2010 |
|
|
|
Peter Chubb Decent MIDI from LilyPond Linux.conf.au, January, 2010 |
|
|
|
Peter Chubb and John Judge When the arduino meets year 9 Other Conference Presentation, linux.conf.au, Wellington, New Zealand, January, 2010. |
|
|
|
Peter Chubb and Yang Song Interrupts considered harmful Other Conference Presentation, Linux.conf.au, Wellington, NZ, January, 2010. |
2009
|
|
|
Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009 |
|
|
|
Andrew Boyton A verified shared capability model Systems Software Verification, pp. 25–44, Aachen, Germany, October, 2009 |
|
|
|
Ralf Huuck, Gerwin Klein and Schlich Bastian Proc. 4th international workshop on system software verification (SSV09) Electronic Notes in Theoretical Computer Science, Volume 254, pp. 1–3, October, 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 |
|
|
|
Michael Norrish Rewriting conversions implemented with continuations Journal of Automated Reasoning, Volume 43, Number 3, pp. 305–336, October, 2009 |
|
|
|
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 |
|
|
|
Yuxin Deng, Robert van Glabbeek, Matthew Hennessy and Carroll Morgan Testing finitary probabilistic processes (extended abstract) International Conference on Concurrency Theory (CONCUR), pp. 274–288, Bologna, Italy, August, 2009 |
|
|
|
Rafal Kolanski and Gerwin Klein Types, maps and separation logic International Conference on Theorem Proving in Higher Order Logics, pp. 276–292, Munich, Germany, 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 |
|
|
|
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish Mind the gap: A verification framework for low-level C International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, 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 |
|
|
|
Gerwin Klein, Ralf Huuck and Bastian Schlich Operating system verification Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009 |
|
|
|
Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser Dingo: Taming device drivers EuroSys Conference, pp. 275–288, Nuremberg, DE, April, 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 |
|
|
|
Aditi Barthwal and Michael Norrish Verified, executable parsing European Symposium on Programming, pp. 160–174, York, March, 2009 |
|
|
|
James Cheney, René Vestergaard and Michael Norrish Formalizing adequacy 2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming, York, March, 2009 |
|
|
|
Nicholas Fitzroy-Dale and Ihor Kuz Towards automatic optimisation of componentised systems Workshop on Isolation and Integration in Embedded Systems, pp. 6, Nuremberg, Germany, 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 |
|
|
|
Gerwin Klein Operating system verification — an overview Sadhana, Volume 34, Number 1, pp. 26–69, February, 2009 Invited paper. Journal homepage. |
|
|
|
Gernot Heiser Hypervisors for consumer electronics IEEE Consumer Communications and Networking Conference, pp. 1–5, Las Vegas, NV, USA, January, 2009 |
2008
|
|
|
André Hergenhan and Gernot Heiser Operating systems technology for converged ECUs Embedded Security in Cars Conference (escar), pp. 3 pages, Hamburg, Germany, November, 2008 |
|
|
|
Stefan M. Petters, Martin Lawitzky, Kevin Elphinstone and Ryan Heffernan Fitting an EDF based scheduling approach to componentised real(-time) systems IEEE Real-Time Systems Symposium, Barcelona, Spain, November, 2008 |
|
|
|
Yuxin Deng, Robert van Glabbeek, Matthew Hennessy and Carroll Morgan Characterising testing preorders for finite probabilistic processes Logical Methods in Computer Science, Volume 4, Number 4, pp. 1–33, October, 2008 |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Verified Software: Theories, Tools and Experiments, pp. 99–115, Toronto, Canada , October, 2008 |
|
|
|
Rafal Kolanski and Gerwin Klein Mapped separation logic Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008 |
|
|
|
5th international verification workshop — VERIFY'08 CEUR Workshop Proceedings, 2008 |
|
|
|
David Cock Bitfields and tagged unions in C — verification through automatic generation International Verification Workshop, pp. 44–55, Sydney, August, 2008 |
|
|
|
David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement International Conference on Theorem Proving in Higher Order Logics, pp. 167–182, Montreal, Canada, August, 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 |
|
|
|
Konrad Slind and Michael Norrish A brief overview of HOL4 International Conference on Theorem Proving in Higher Order Logics, pp. 28–32, Montréal, Canada, August, 2008 |
|
|
|
Proceedings of the 3rd international workshop on systems software verification (SSV 2008) Volume 217 in ENTCS, Elsevier, 2008 |
|
|
|
Rafal Kolanski A logic for virtual memory Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008 |
|
|
|
Gernot Heiser Trusted ⇐ trustworthy ⇐ proof – Position paper Conference on Future of Trust in Computing, pp. 55–59, Berlin, DE, May, 2008 |
|
|
|
Tom Ridge, Michael Norrish and Peter Sewell A rigorous approach to networking: TCP, from implementation to protocol to service International Symposium on Formal Methods (FM), pp. 294—309, Turku, Finland, May, 2008 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel design for isolation and assurance of physical memory Workshop on Isolation and Integration in Embedded Systems, pp. 35–40, Glasgow, UK, April, 2008 |
|
|
|
Gernot Heiser The role of virtualization in embedded systems Workshop on Isolation and Integration in Embedded Systems, pp. 11–16, Glasgow, UK, April, 2008 |
|
|
|
Gernot Heiser Do microkernels suck? Other Conference Presentation, Linux.conf.au, Melbourne, Australia, January, 2008. |
|
|
|
Ihor Kuz and Jenny Liu Extending the capabilities of component models for embedded systems Third International Conference on the Quality of Software-Architectures (QoSA), pp. 182–196, Boston, MA, USA, January, 2008 |
2007
|
|
|
Kevin Elphinstone, David Greenaway and Sergio Ruocco Lazy queueing and direct process switch — merit or myths? Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 69–77, Pisa, Italy, December, 2007 |
|
|
|
Gernot Heiser Your system is secure? Prove it! USENIX ;login:, Volume 32(6), pp. 35—38, December, 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 |
|
|
|
Michael Norrish A formal semantics for c++ Technical Report, NICTA, November, 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 Workshop on Programming Languages and Operating Systems (PLOS), pp. 5, Stevenson, WA, USA, October, 2007 |
|
|
|
Michael Norrish and René Vestergaard Proof pearl: de bruijn terms really do work International Conference on Theorem Proving in Higher Order Logics, pp. 207–222, Kaiserslautern, September, 2007 |
|
|
|
Yuxin Deng, Robert van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang Characterising testing preorders for finite probabilistic processes Annual IEEE Symposium on Logic in Computer Science, pp. 313–322, Wroclaw, Poland, July, 2007 |
|
|
|
Jia Meng, Lawrence C. Paulson and Gerwin Klein A termination checker for isabelle hoare logic International Verification Workshop, pp. 104–118, Bremen, Germany, July, 2007 |
|
|
|
Leonid Ryzhyk, Timothy Bourke and Ihor Kuz Reliable device drivers require well-defined protocols Workshop on Hot Topics in System Dependability, pp. Article 3, Edinburgh, UK, June, 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 |
|
|
|
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 |
|
|
|
Yuxin Deng, Robert van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang Remarks on testing probabilistic processes Electronic Notes in Theoretical Computer Science, Volume 172, Number , pp. 359–397, April, 2007 |
|
|
|
Yuxin Deng, Robert van Glabbeek, Carroll Morgan and Chenyi Zhang Scalar outcomes suffice for finitary probabilistic testing European Symposium on Programming, pp. 363–378, Braga, Portugal, March, 2007 |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97–108, Nice, France, January, 2007 |
2006
|
|
|
Myrto Zehnder and Peter Chubb Virtualising PCI Gelato ICE, Singapore, October, 2006 |
|
|
|
Kevin Elphinstone and Scott Brandt Proceedings of the 2007 workshop on operating system platforms for embedded real-time applications Technical Report, NICTA, July, 2006 |
|
|
|
Shehjar Tikoo and Peter Chubb Improving NFS performance Gelato ICE conference, San Jose, CA, April, 2006 |
|
|
|
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55—66, Charleston, South Carolina, USA, January, 2006 |
2005
|
|
|
Peter Chubb Bugs: getting them stomped! Gelato ICE, Brazil, October, 2005 |
|
|
|
Peter Chubb Which filesystem? Gelato ICE, Brazil, October, 2005 |
|
|
|
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets ACM Conference on Communications, pp. 265–276, Philadelphia, August, 2005 |
|
|
|
Peter Chubb and Darren Williams Linux scalability — from the micro to the HUGE Linux.conf.au, Canberra, ACT, April, 2005 |
2004
|
|
|
Michael Norrish Recursive function definition for types with binders International Conference on Theorem Proving in Higher Order Logics, pp. 241—256, Park City, UT, US, September, 2004 |
|
|
|
Peter Chubb Get more device drivers out of the kernel! Ottawa Linux Symposium, Ottawa, Canada, July, 2004 |
|
|
|
Peter Chubb Linux kernel infrastructure for user-level device drivers Linux.conf.au, Adelaide, Australia, January, 2004 |
2003
|
|
|
Peter Chubb Where's all the time going? Microstate accounting in Linux 2.5 AUUG Winter Conference, 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 |
|
|
|
Michael Norrish Complete integer decision procedures as derived rules in HOL International Conference on Theorem Proving in Higher Order Logics, pp. 71–86, Rome, September, 2003 |
|
|
|
Adam Wiggins A survey on the interaction between caching, translation and protection Technical Report UNSW-CSE-TR-0321, School of Computer Science and Engineering, August, 2003 |
2002
|
|
|
Peter Chubb Terabytes on a diet AUUG Winter Conference, 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 2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001 |
|
|
|
Cristan Szmajda Calypso: A portable translation layer 2nd Workshop on Microkernels and Microkernel-based 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 |
|
|
|
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 |
|
|
|
Gernot Heiser Inside L4/MIPS: Anatomy of a high-performance microkernel Sydney, 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 J. 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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Jinsong Ouyang and Gernot Heiser Libra: A library for reliable distributed applications International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 801–810, Sunnyvale, CA, USA, August, 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 |
|
|
|
Jinsong Ouyang and Gernot Heiser Checkpointing and recovery for distributed shared memory applications IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 191–9, Lund, SE, August, 1995 |
1994
|
|
|
Kevin Elphinstone, Stephen Russell and Gernot Heiser Issues in implementing virtual memory Technical Report UNSW-CSE-TR-9411, School of Computer Science and Engineering, September, 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 |
Other technical reports of the School of Computer Science & Engineering.
Trustworthy Systems Invited Talks
TS people are frequently invited to give talks at international events. Here is an (almost complete) list:
2025
|
|
|
Gernot Heiser Why change the kernel when you have seL4? Keynote at KISV workshop, October, 2025 |
|
|
|
Gernot Heiser Don’t forget the OS – and the principles! Invited talk at SIGOPS Strategy Workshop, October, 2025 |
|
|
|
Gernot Heiser It's time for truly secure operating systems CASA Distinguished Lecture, May, 2025 |
|
|
|
Gernot Heiser Will we ever have truly secure operating systems? Joint Keynote at ASPLOS and EuroSys, April, 2025 |
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 |
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 |
|
|
|
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 |
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 |
|
|
|
Gernot Heiser Can we make trustworthy systems a reality? Keynote at the ACM International Systems and Storage Conference (SYSTOR), June, 2022 |
|
|
|
Gernot Heiser Security is no excuse for poor performance: welcome to the world's most highly assured operating system Invited Talk at the CyberUK Conference, May, 2022 |
|
|
Gernot Heiser Securing the kernel Invited Talk at the Swiss Cyber Security Days, April, 2022 | |
|
|
|
Gernot Heiser The seL4 report: State of the seL4 ecosystem Keynote at the Trusted Computing Center of Excellence 2022 Summit, February, 2022 |
|
|
|
Natasha Fernandes, Annabelle McIver and Carroll Morgan How to develop an intuition for risk... and other invisible phenomena (invited talk) Proc. Computer Science Logic 2022, pp. 2:1–2:14, 2022 |
2021
|
|
Gernot Heiser The seL4 microkernel – mathematical proof of security Invited Talk at the SSRC Summit, October, 2021 |
2020
|
|
|
Gernot Heiser The seL4 microkernel – security through mathematical proof Invited Talk at the Western Digital Security Workshop, December, 2020 |
|
|
Gernot Heiser seL4: verified operating system for the real world Invited Talk at the Annual Conference of the Research Institute for Cyber Defence (CODE), November, 2020 | |
|
|
|
Gernot Heiser The seL4 report Keynote at the 3rd seL4 Summit, November, 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 The formally verified seL4 microkernel: Present and future Invited Talk at Multicore World, February, 2020 |
2019
|
|
Gernot Heiser Making the (software) TCB trustworthy Invited Talk at the NSA Formal Methods at Scale Workshop, October, 2019 | |
|
|
|
Gernot Heiser We need a new hardware-software contract Invited Talk at the Lorentz Center SHARD Workshop, September, 2019 |
|
|
|
Gernot Heiser Security needs a better hardware-software contract Invited talk at Design Automation Conference (DAC), Las Vegas, NV, USA, June, 2019 |
|
|
|
Gernot Heiser Time Protection: Principled prevention of timing channels Invited Talk at the Enabling Trust through OS Proofs (ENTROPY) Workshop, June, 2019 |
|
|
|
Gernot Heiser How to not only do great systems research, but also convince others Keynote at EuroSys Doctoral Workshop, Dresden, DE, March, 2019 |
|
|
Gernot Heiser Security needs a new hardware-software contract Invited Talk at the ISAT/DARPA PHI Workshop, February, 2019 | |
|
|
|
Gernot Heiser Security needs a new hardware-software contract Keynote at HiPEAC Workshop Secure Hardware, Architectures, and Operating Systems (SeHAS), January, 2019 |
2018
|
|
|
Gernot Heiser No safety without security, no security without trustworthy operating systems Invited talk at Qingdao International Academicians Forum, August, 2018 |
|
|
|
Gernot Heiser Stop the leaks: Towards provable information security with seL4 Keynote at the International Summer School on Information Security and Protection (ISSISP), July, 2018 |
|
|
|
Gernot Heiser No safety without security Presentation to Korean National Academy of Engineering as part of a delegation of the Australian Academy of Technology and Engineering, June, 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 |
2017
|
|
Gernot Heiser Why safety requires security, and how to achieve it Invited talk at Symposium on Cyber Security of Medical and Healthcare Systems, Hong Kong Productivity Council, December, 2017 | |
|
|
Gernot Heiser Trustworthy operating systems for critical embedded / cyber-physical systems Keynote at Embedded Systems Week (ESWEEK), October, 2017 | |
|
|
|
Gernot Heiser Software-enforced isolation – the key to cyber-secure cars Invited talk at Cyber-Secure Car Japan, September, 2017 |
|
|
Gernot Heiser The open-source seL4 kernel: Military-grade security through mathematics Invited talk at Linaro Connect conference, September, 2017 | |
|
|
|
June Andronick Reasoning about concurrency in high-assurance, high-performance software systems International Conference on Automated Deduction, pp. 1–7, Gothenburg, August, 2017 |
|
|
|
Gernot Heiser Operating systems for secure and safe embedded systems Invited lecture series at ACACES Summer School, Italy, July, 2017 |
|
|
Gernot Heiser seL4: A formally-verified OS kernel for the real world Invited talk at JASON Summer Study on Formal Methods, June, 2017 |
2016
|
|
|
Gernot Heiser Challenges of temporal isolation Invited Dagstuhl Seminar, October, 2016 |
|
|
Gernot Heiser Making systems trustworthy: The seL4 microkernel Invited Talk at Huawei, October, 2016 | |
|
|
Gernot Heiser Provable security and safety: The seL4 microkernel and its use in critical systems Invited lecture at GI Winter School on Operating Systems, February, 2016 | |
|
|
Gernot Heiser Provable security and safety: The seL4 microkernel and its use in critical systems Invited Talk at the GFI Workshop on Operating Systems, February, 2016 |
2015
|
|
Gernot Heiser seL4 overview Invited lecture at NATO Cybersecurity School, Jordan, February, 2015 | |
|
|
|
Gernot Heiser seL4: Present and future invited talk at FOSDEM'15, Brussels, BE, February, 2015 |
2013
|
|
|
Gernot Heiser Making trusted systems trustworthy Invited lecture at the Artist Summer School on Embedded Systems, Aix-les-Bains, France, September, 2013 |
|
|
|
Gernot Heiser Can truly dependable systems be affordable? Keynote at APSys'13, Singapore, July, 2013 |
|
|
Gernot Heiser Provable isolation Invited talk at 3rd ADM Cyber Security Conference, June, 2013 | |
|
|
Gernot Heiser Building effective operating systems in cyber defence – now and into the future Invited talk at 3rd ADM Cyber Security Conference, June, 2013 | |
|
|
|
Gernot Heiser Towards verified real-world systems Invited talk at LCCC Workshop on Formal Verification of Embedded Control Systems, April, 2013 |
|
|
|
Gernot Heiser Protecting e-government against attacks Invited talk at European Parliament Workshop on Security of e-Government Systems, February, 2013 |
2012
|
|
Gernot Heiser How to write a good (systems) paper Invited talk at Workshop on Supporting Diversity in Systems Research (Diversity'12), October, 2012 | |
|
|
|
Gernot Heiser Can we make trusted systems trustworthy? Invited lecture at the Artist Summer School on Embedded Systems, Aix-les-Bains, France, September, 2012 |
|
|
Gernot Heiser A platform for trustworthy systems Invited talk at the 9th International Colloquium on Theoretical Aspects of Computing (ICTAC), Bangalore, India, September, 2012 | |
|
|
Gernot Heiser Towards trustworthy embedded systems Keynote at Conference on Language, Compiler and Tool Support for Embedded Systems (LCTES), Beijing, China, June, 2012 | |
|
|
|
Gernot Heiser How to build truly dependable systems Invited lecture at UPMARC Summer School on Programming Multicore Computer Systems, Uppsala, Sweden, June, 2012 |
|
|
|
Gernot Heiser Towards a platform for secure systems Keynote at SICS Workshop on Virtualization and Verification for Security, Stockholm, Sweden, March, 2012 |
|
|
|
Gernot Heiser Towards a platform for trustworthy systems Invited talk at 2nd Tsinghua Software Day, Beijing, China, March, 2012 |
2011
|
|
Gernot Heiser Towards trustworthy systems or the continuing relevance of OS research Keynote at the Brazilian Symposium of Computational Systems (SBESC), Florianopolis, BR, November, 2011 | |
|
|
|
Gernot Heiser Low-overhead virtualization of mobile systems Invited talk at International Conference on Compilers, Architecture and Synthesis for Embedded Systems (CASES), Taipei, Taiwan, October, 2011 |
|
|
|
Gernot Heiser The role of language technology in trustworthy operating systems Keynote at Workshop on Programming Languages and Operating Systems (PLOS), Cascais, Portugal, October, 2011 |
|
|
|
Gernot Heiser Towards trustworthy systems Distinguished Lecturer Series, Institute of Information Science, Academia Sinica, Taipei, Taiwan, October, 2011 |
|
|
|
Gernot Heiser Towards an OS platform for truly dependable real-time systems Keynote at Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Porto, Portugal, July, 2011 |
|
|
Gernot Heiser Virtualizing embedded systems – why bother? Invited talk at Design Automation Conference (DAC), San Diego, CA, USA, June, 2011 |
2010
|
|
|
Gernot Heiser The road to trustworthy systems Distinguished Systems Speakers Series, Purdue University, USA, October, 2010 |
|
|
|
Gernot Heiser The L4 microkernel — from research to mass deployment and back Invited Talk at Workshop on Isolation and Integration for Dependable Systems, Paris, France, April, 2010 |
|
|
Gernot Heiser Formally-verified OS kernel: A basis for reliable systems? Invited Talk at IFIP WG10.4 Winter Meeting, Ishigaki Island, Japan, January, 2010 |
2009
|
|
Gernot Heiser 8,000 lines, one kernel, zero bugs Invited talk at Microsoft Research Asia Workshop on Verified Software, Beijing, China, October, 2009 |
2008
|
|
Gernot Heiser Formal OS kernel verification—making trusted trustworthy Invited talk at 1st BSI Workshop on Operating System Security, Munich, DE, December, 2008 | |
|
|
Gernot Heiser Virtualization in embedded systems Invited talk at Intel Virtualization Summit, Hillsboro, OR, USA, September, 2008 | |
|
|
Gernot Heiser Secure operating systems Invited Lecture at 2nd Asia Pacific Trusted Infrastructure Summer School 2008 (APTISS'08), Malaysia, August, 2008 | |
|
|
Gernot Heiser Operating system verification for real use Invited talk at the 5th International Verification Workshop, Sydney, August, 2008 |
2007
|
|
Gernot Heiser Secure operating systems Invited lecture at 2nd European Trusted Infrastructure Summer School (ETISS), Bochum, DE, October, 2007 | |
|
|
Gernot Heiser Embedded systems safety, reliability and security: The challenge of complexity Invited talk at the IITA International Symposium on IT R&D, Seoul, Korea, October, 2007 | |
|
|
Gernot Heiser Next-generation embedded operating systems Invited talk at the China Australia ICT Workshop, Beijing, China, August, 2007 | |
|
|
Gernot Heiser Safe and reliable embedded systems Invited presentation at ISO/IEC JTC 1 Technology Watch Workshop, Gold Coast, Australia, August, 2007 | |
|
|
Gernot Heiser Next-generation embedded operating systems Invited talk at the 3rd International Conference on Embedded Software and Systems (ICESS 2007), Daegu, Korea, May, 2007 |
2006
|
|
Gernot Heiser Trustworthy embedded systems—how Australian research can have an impact Invited talk at 3rd Australian ICT Outlook Forum, September, 2006 | |
|
|
Gernot Heiser Software freedom—essential for business and innovation Invited talk for Software Freedom Day, Sydney, September, 2006 | |
|
|
Gernot Heiser Towards trustworthy embedded systems Invited talk at the 12th IEEE Conference on Embedded and Real-Time Computing and Applications, Sydney, August, 2006 |
2005
|
|
Gernot Heiser Secure embedded systems need microkernels Invited talk at Indo-Australia Conference on IT Security, Chennai, IN, February, 2005 |
Research Theses
Below are theses done by students done as part of higher degree by research (HDR) studies (PhD, MPhil and, in the past, ME).
2023
|
|
|
Zilin Chen Towards a practical high-assurance systems programming language PhD Thesis, UNSW, Sydney, Australia, March, 2023 |
2020
|
|
|
Robert Sison Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs PhD Thesis, UNSW, Sydney, Australia, October, 2020 |
2019
|
|
|
Qian Ge Principled elimination of microarchitectural timing channels through operating-system enforced time protection PhD Thesis, UNSW, Sydney, Australia, October, 2019 |
|
|
|
Liam O'Connor Type systems for systems types PhD Thesis, UNSW, Sydney, Australia, August, 2019 |
|
|
|
Hira Taqdees Syeda Low-level program verification under cached address translation PhD Thesis, UNSW, Sydney, Australia, August, 2019 |
|
|
|
Yanyan Shen Microkernel mechanisms for improving the trustworthiness of commodity hardware PhD Thesis, UNSW, Sydney, Australia, March, 2019 |
2018
|
|
|
Anna Lyons Mixed-criticality scheduling and resource sharing for high-assurance operating systems PhD Thesis, UNSW, August, 2018 |
|
|
|
Daniel Matichuk Automation for proof engineering: Machine-checked proofs at scale PhD Thesis, UNSW, Sydney, Australia, July, 2018 |
|
|
|
Mohammad Abdulaziz Formally verified compositional algorithms for factored transition systems PhD Thesis, Australian National University, June, 2018 |
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
|
|
|
Alexander Legg A counterexample guided method for reactive synthesis PhD Thesis, UNSW, Sydney,Australia, September, 2016 |
|
|
|
Sidney Amani A methodology for trustworthy file systems PhD Thesis, CSE, UNSW, Sydney, Australia, August, 2016 |
|
|
|
Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016 |
2015
|
|
|
David Greenaway Automated proof-producing abstraction of c code PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015 |
2014
|
|
|
Andrew Boyton Secure architectures on a verified microkernel PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014 |
|
|
|
David Cock Leakage in trustworthy systems PhD Thesis, UNSW, Sydney, Australia, August, 2014 |
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 |
|
|
|
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 |
2011
|
|
|
Rafal Kolanski Verification of programs in virtual memory using separation logic PhD Thesis, UNSW, Sydney, Australia, July, 2011 |
|
|
|
Etienne Le Sueur An analysis of the effectiveness of energy management on modern computer processors MSc Thesis, UNSW, Sydney, Australia, June, 2011 |
|
|
|
Nicholas FitzRoy-Dale Architecture optimisation PhD Thesis, UNSW, Sydney, Australia, March, 2011 |
2010
|
|
|
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
|
|
|
Joshua LeVasseur Device-driver reuse via virtual machines PhD Thesis, UNSW, Sydney, Australia, May, 2009 |
|
|
|
Matthew Chapman vNUMA: Virtual shared-memory multiprocessors PhD Thesis, UNSW, Sydney, Australia, March, 2009 |
2008
|
|
|
Harvey Tuch Formal memory models for verifying C systems code PhD Thesis, UNSW, Sydney, Australia, August, 2008 |
|
|
|
Ian Wienand Transparent large-page support for Itanium Linux ME Thesis, UNSW, Sydney, Australia, July, 2008 |
|
|
|
Daniel Potts Eidolon: Adapting distributed applications to their environment PhD Thesis, UNSW, Sydney, Australia, January, 2008 |
2007
|
|
|
Luke Macpherson Performing under overload PhD Thesis, UNSW, Sydney, Australia, September, 2007 |
|
|
|
Andrew Baumann Dynamic update for operating systems PhD Thesis, UNSW, Sydney, Australia, August, 2007 |
2005
|
|
|
Volkmar Uhlig Scalability of microkernel-based systems PhD Thesis, University of Karlsruhe, Karlsruhe, DE, June, 2005 |
1999
|
|
|
Kevin Elphinstone Virtual memory in a 64-bit microkernel PhD Thesis, UNSW, Sydney, Australia, March, 1999 |
1998
|
|
|
Jerry Vochteloo Design, implementation and performance of protection in the Mungi single-address-space operating system PhD Thesis, UNSW, Sydney, Australia, July, 1998 |
Selected Coursework Student Theses
Below are a selection of theses produced by pre-research students with the group: BSc Hons, BE, MIT (coursework masters)
2025
|
|
|
Michael Mospan Core management in LionsOS BSc(Hons) Thesis, School of Computer Science and Engineering, December, 2025 |
|
|
|
Sai Nair Updating L4v invariants to aid time protection proofs BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2025 |
|
|
|
Halogen Truong Improving the safety of the Pancake language BE Thesis, School of Computer Science and Engineering, November, 2025 |
|
|
|
Lesley Rossouw sDDF queueing performance BE Thesis, School of Computer Science and Engineering, Sydney, Australia, September, 2025 |
2023
|
|
|
Lucy Parker High-performance networking on seL4 BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2023 |
2022
|
|
|
Mitchell Johnston Strengthening scheduling guarantees of seL4 MCS with IPC budget limits BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2022 |
2018
|
|
|
Sebastian Holzapfel User-level mixed criticality systems scheduling on multicore processors BE Thesis, School of Electrical Engineering and Telecommunication, Sydney, Australia, November, 2018 |
|
|
|
Jack Suann Zircon on seL4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, May, 2018 |
2017
|
|
|
A. Felizzi Trianqles: Porting Qubes to seL4 BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2017 |
2016
|
|
|
Kent McLeod Usermode OS components on seL4 with rump kernels BE Thesis, School of Electrical Engineering and Telecommunication, Sydney, Australia, October, 2016 |
2011
|
|
|
Alexandra Boulgakov Sunswift IV strategy for the 2011 World Solar Challenge BE Thesis, School of Electrical Engineering, Sydney, Australia, November, 2011 |
|
|
|
Aleksander Budzynowski Operating system for a flow-graph machine BE Thesis, School of Mechanical and Manufacturing Engineering, Sydney, Australia, October, 2011 |
|
|
|
Anna Lyons Efficient concurrency control for high-performance microkernels BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, July, 2011 |
2010
|
|
|
Prashant Varanasi Implementing hardware-supported virtualization in OKL4 on ARM BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2010 |
|
|
|
Josh Matthews Native OKL4 web browser BE Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2010 |
2009
|
|
|
Michael Hills Native OKL4 Android stack BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2009 |
|
|
|
Andrew Wrigley Steering-Integrated driver controls for sunswift IV BE Thesis, School of Electrical Engineering, Sydney, Australia, November, 2009 |
2008
|
|
|
Aaron Carroll I/O scheduling on RAID BE Thesis, School of Electrical Engineering, Sydney, Australia, July, 2008 |
2007
|
|
|
David Greenaway Quantifying the effects of scheduling on IPC performance BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2007 |
|
|
|
Joshua Root Virtualising Darwin on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, February, 2007 |
2006
|
|
|
Clarence Dang Optimising L4 on Blackfin 533/537: An investigation into a high performance L4 microkernel without virtual memory BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006 |
|
|
|
Tom Birch Performance limits of Darwin on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006 |
2005
|
|
|
Geoffrey Lee I/O kit drivers for L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2005 |
|
|
|
Matthew Warton Single kernel stack L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2005 |
|
|
|
Philip Geoffrey Derrin A secure microkernel BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2005 |
|
|
|
Abi Nourai A physically-addressed L4 kernel BE Thesis, School of Computer Science and Engineering, Sydney, Australia, March, 2005 |
2003
|
|
 |
Ka-shu Wong MacOS X on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, December, 2003 |
2002
|
|
|
Andrew Baumann A thread model for Mungi BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
|
|
|
Ben Leslie Mungi device drivers BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
|
|
|
David C. Snowdon Hard- and software framework for the optimisation of Sunswift-II BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
|
|
|
Harvey Tuch A comparison of address translation mechanisms for virtually-addressed caches in embedded systems BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
2000
|
|
|
Antony Edwards A component architecture for system extensibility BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000 |
|
|
|
Simon Winwood Flexible scheduling mechanisms in L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000 |
|
|
|
Patryk Zadarnowski The design and implementation of an extendible instruction set simulator BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000 |
1999
|
|
|
Luke Deller Loading and debugging tasks in SawMill BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Vincent Jayawardene An intensional engine on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Daniel Potts L4 on uni- and multiprocessor Alpha BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Cristan Szmajda A new virtual memory implementation for L4/MIPS BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Adam Wiggins The design and implementation of the L4 microkernel on the StrongARM SA-1100 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |