Trustworthy Systems

Publications, Theses and Technical Reports

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

Our Best Papers

Abstract
Slides
PDF
Presentation Video
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser
Time protection: The missing OS abstraction
EuroSys Conference, Dresden, Germany, March, 2019
Best Paper Award
Abstract PDF Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser
Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time
EuroSys Conference, Porto, Portugal, April, 2018
Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract PDF 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
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013
Abstract
Slides
PDF 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
Abstract PDF 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
Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Best Paper Award
Hall of Fame Award
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009
Abstract PDF 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

2024

Abstract Slides Gernot Heiser
LionsOS: A highly dependable operating system for cyberphysical systems
Keynote at International Symposium on Parallel Computing and Distributed Systems, September, 2024
Abstract PDF 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
Abstract Slides Gernot Heiser
LionsOS: Towards a truly dependable operating system
Keynote at International Conference on Dependable Systems and Networks (DSN), June, 2024
Abstract PDF Trudy Weibel, Zoltan Kocsis, Mathieu Paturel, Rob Sison, Isitha Subasinghe and Gernot Heiser
Verifying the seL4 Microkit
https://trustworthy.systems/publications/papers/Weibel_KPSSH_24.pdf, June, 2024
Abstract PDF Nils Wistoff1, 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
Abstract Slides Peter Chubb
Running your own mailserver
Everything Open, Gladstone, QLD, AU, April, 2024
Abstract Slides
Video
Gernot Heiser
Lions OS: secure – fast – adaptable
Everything Open, Gladstone, QLD, AU, April, 2024
Abstract PDF Gernot Heiser, Peter Chubb, Alex Brown, Courtney Darville and Lucy Parker
sDDF design: design, implementation and evaluation of the seL4 device driver framework
https://trustworthy.systems/publications/papers/Heiser_CBDP_24.pdf, 2024

2023

Abstract PDF 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
Abstract PDF Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus Myreen, Michael Norrish and Gernot Heiser
Pancake: verified systems programming made sweeter
Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023
Abstract Slides Gernot Heiser
The seL4 microkernel: Provable security for the real world
Keynote at the International Workshop on Advanced Industrial Science and Technology, September, 2023
Abstract Slides
Video
Lucy Parker
The seL4 device driver framework
Talk at the 5th seL4 Summit, September, 2023
Abstract Slides
Video
Ivan Velickovic
The seL4 Microkit
Talk at the 5th seL4 Summit, September, 2023
Abstract PDF 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
Abstract Slides Gernot Heiser
Intelligent vehicle security needs a verified operating system
Keynote at the International Workshop on Safety and Security of Intelligent Vehicles, June, 2023
Abstract Slides
Video
Gernot Heiser
seL4 update: Foundation and TS R&D news
Invited talk at the Trusted Computing Center of Excellence 2023 Summit, May, 2023
Abstract
Slides
PDF Rob 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Scott Buckley, Rob 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
Abstract Slides
Video
Gernot Heiser
R&D update from Trustworthy Systems
Talk at the 5th seL4 Summit, 2023
plain text to be published Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus Myreen, Michael Norrish, Johannes Åman Pohjola and Riccardo Zanetti
Purecake: A verified compiler for a lazy functional language
Proc. ACM Program. Lang., Volume 7, Number PLDI, pp. 952–976, 2023
Abstract PDF 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

Abstract PDF 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
Abstract
Slides
PDF
Presentation Video
Gernot Heiser, Lucy Parker, Ivan Velickovic, Peter Chubb and Ben Leslie
Can we put the "S" into IoT?
IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022
Abstract Slides
Video
Gernot Heiser
State of seL4-related research
Keynote at the seL4 Summit, October, 2022
Abstract Slides
Video
Gernot Heiser
seL4 overview: Principles, abstractions, use
Invited talk at the seL4 Summit, October, 2022
Abstract Slides
Video
Lucy Parker
The seL4 device driver framework
Talk at the 4th seL4 Summit, October, 2022
plain text to be published 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
plain text to be published 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
Abstract PDF 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
Abstract Slides
Video
Gernot Heiser
The seL4 report: State of the seL4 ecosystem
Keynote at the Trusted Computing Center of Excellence 2022 Summit, February, 2022
Abstract Slides
Video
Gernot Heiser
The seL4 Foundation – growing through upheaval
On-line, January, 2022
Abstract PDF 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
Abstract PDF 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

Abstract PDF 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
Abstract PDF Richard S. Bird, Jeremy Gibbons, Ralf Hinze, Peter Hoefner, 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Rob Sison and Toby Murray
Verified secure compilation for mixed-sensitivity concurrent programs
Journal of Functional Programming, Volume 31, pp. e18, 2021

2020

Abstract PDF 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
Abstract PDF 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
Abstract PDF
Presentation Video
Alejandro Gomez-Londono, 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
Abstract Slides
Video
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
Abstract PDF 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
Abstract PDF Rob van Glabbeek
Reactive bisimulation semantics for a process algebra with time-outs
31st International Conference on Concurrency Theory (CONCUR 20), pp. 6:1-6:23, Online, August, 2020
Abstract PDF Rob van Glabbeek
Reactive temporal logic
Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics (EXPRESS/SOS 2020), pp. 51-68, Online, August, 2020
Abstract PDF Rob van Glabbeek, Bas Luttik and Linda Spaninks
Rooted divergence-preserving branching bisimilarity is a congruence
Logical Methods in Computer Science, Volume 16, Issue 3, pp. 14:0-14;16, August, 2020
Abstract to be published Michael Norrish and Yiming Xu
Mechanised modal model theory
International Joint Conference on Automated Reasoning, pp. 518-533, Paris, July, 2020
Abstract PDF Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat
Feasibility of cross-chain payment with success guarantees
32nd ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2020, pp. 579-581, Virtual event, July, 2020
Abstract to be published 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
Abstract PDF 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
Abstract PDF Gernot Heiser
The seL4 microkernel – an introduction
seL4 Foundation Whitepaper, May, 2020
Abstract PDF Erik van der Kouwe, Gernot Heiser, Dennis Andriesse, Herbert Bos and Cristiano Giuffrida
Benchmarking flaws undermine security research
IEEE Security and Privacy, Volume 18, Issue 3, May, 2020
Abstract PDF Rob van Glabbeek and Kees Middelburg
On infinite guarded recursive specifications in process algebra
Technical Report, Data61, CSIRO, May, 2020
Abstract PDF
Presentation Video
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
Abstract PDF Ryan Barry, Rob van Glabbeek and Peter Hoefner
Formalising the optimised link state routing protocol
4th Workshop on Models for Formal Analysis of Real Systems (MARS 2020), pp. 40-71, Dublin, Ireland, April, 2020
Abstract PDF Jack Drury, Peter Hoefner and Weiyou Wang
Formal models of the OSPF routing protocol
MARS2020, pp. 72–120, Dublin, Ireland, April, 2020
Abstract PDF 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
Abstract Slides
Video
Gernot Heiser
Verified seL4 on secure RISC-V processors
at linux.conf.au, Gold Coast, January, 2020
Abstract PDF 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
Abstract PDF 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

Abstract PDF Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat
Cross-chain payment protocols with success guarantees
Technical Report, Data61, CSIRO, December, 2019
Abstract PDF Rob van Glabbeek, Ursula Goltz, Christopher Lippert and Mennicke Stephan
Stronger validity criteria for encoding synchrony
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. 182-205, Paris, November, 2019
Abstract to be published June Andronick
Successes in deployed verified software (and insights on key social factors)
FM 2019: Formal Methods – The Next 30 Years, pp. 11-17, Porto, Portugal, October, 2019
Abstract PDF Wan Fokkink, Rob van Glabbeek and Bas Luttik
Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence
Information and Computation, Volume 268, October, 2019
Abstract PDF 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
Abstract Slides Ihor Kuz
Building trustworthy systems on seL4
seL4 Summit, Herndon, VA, USA, September, 2019
Abstract
Slides
PDF Rob 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
Abstract PDF Wan Fokkink and Rob van Glabbeek
Proceedings 30th international conference on concurrency theory (CONCUR 2019)
Volume 140 in Leibniz International Proceedings in Informatics (LIPIcs) 140. Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Amsterdam, August, 2019
Abstract PDF 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
Abstract PDF Rob van Glabbeek
Ensuring liveness properties of distributed systems: Open problems
Journal of Logical and Algebraic Methods in Programming, Volume 109, pp. 1-19, August, 2019
Abstract PDF Rob van Glabbeek
On the meaning of transition system specifications
Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics, pp. 69–85, Amsterdam, The Netherlands, August, 2019
Abstract PDF Rob van Glabbeek and Peter Hoefner
Progress, justness and fairness
ACM Computing Surveys, Volume 52, Issue 4, pp. 69:1–69:38, August, 2019
Abstract PDF Rob van Glabbeek
Reward testing equivalences for processes
Models, Languages, and Tools for Concurrent and Distributed Programming, Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, pp. 45-70, Volume 11665 in Lecture Notes in Computer Science, Springer, 2019
Abstract PDF 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
Abstract Slides Gernot Heiser
Security needs a better hardware-software contract
Invited talk at Design Automation Conference (DAC), Las Vegas, NV, USA, June, 2019
Abstract PDF 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, pp. 1041-1053, Phoenix, Arizona, United States of America, June, 2019
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Johannes Åman Pohjola
Psi-calculi revisited: Connectivity and compositionality
Technical Report, Data61, CSIRO, April, 2019
Abstract PDF Peter Hoefner, Rob van Glabbeek and Michael Markl
A process algebra for link layer protocols
European Symposium on Programming, Prague, Czech Republic, April, 2019
Abstract PDF Rob van Glabbeek
Justness: A completeness criterion for capturing liveness properties
International Conference on Foundations of Software Science and Computational Structures, pp. 505-522, Prague, Czech Republic, April, 2019
Abstract
Slides
PDF
Presentation Video
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser
Time protection: The missing OS abstraction
EuroSys Conference, Dresden, Germany, March, 2019
Best Paper Award
Abstract Slides Gernot Heiser
How to not only do great systems research, but also convince others
Keynote at EuroSys Doctoral Workshop, Dresden, DE, March, 2019
Abstract PDF 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
Abstract PDF 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
Abstract Slides Gernot Heiser
What's new in the world of seL4?
Talk at FOSDEM'19, Brussels, February, 2019
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Nick Fischer and Rob van Glabbeek
Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours
Journal of Logical and Algebraic Methods in Programming, Volume 102, pp. 64-102, January, 2019
Abstract PDF 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
Abstract PDF Annabelle McIver and Carroll Morgan
Proving that programs are differentially private
Programming Languages and Systems, pp. 3–18, 2019
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Callum Bannister and Peter Hoefner
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
Abstract PDF Alejandro Gomez-Londono and Johannes Åman Pohjola
Connecting choreography languages with verified stacks
at Nordic Workshop on Programming Theory, Oslo, Norway, October, 2018
Abstract PDF Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
Abstract PDF Rob van Glabbeek and Peter Hoefner
Progress, justness and fairness
Technical Report, Data61, CSIRO, October, 2018
Abstract PDF Rob van Glabbeek
On the validity of encodings of the synchronous in the asynchronous π-calculus
Information Processing Letters, Volume 137, pp. 17-25, September, 2018
Abstract PDF Rob van Glabbeek
Is speed-independent mutual exclusion implementable?
International Conference on Concurrency Theory (CONCUR), Beijing, China, September, 2018
Abstract PDF Rob van Glabbeek, Peter Hoefner and Djurre van der Wal
Analysing AWN-specifications using mCRL2 (extended abstract)
14th International Conference on integrated Formal Methods, pp. 398-418, Maynooth, September, 2018
Abstract
Slides
PDF Simon Biggs, Damon Lee and Gernot Heiser
The jury is in: Monolithic OS design is flawed
Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018
Abstract
Slides
PDF 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.
Abstract PDF Callum Bannister, Peter Hoefner and Gerwin Klein
Backwards and forwards with separation logic
International Conference on Interactive Theorem Proving, pp. 68–87, Oxford, July, 2018
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract Slides Gernot Heiser
The quest for the perfect API
Invited "Fireside Talk" at VMware on occasion of the virtualisation pioneer's 20th anniversary, April, 2018
Abstract PDF Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser
Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time
EuroSys Conference, Porto, Portugal, April, 2018
Abstract PDF Toby Murray, Rob Sison and Kai Engelhardt
COVERN: A logic for compositional verification of information flow control
European Conference on Security and Privacy (EuroS&P), London, United Kingdom, April, 2018
Abstract PDF Rob van Glabbeek
A theory of encodings and expressiveness
International Conference on Foundations of Software Science and Computational Structures, pp. 183-202, Thessaloniki, Greece, April, 2018
Abstract PDF John Gallager, Rob van Glabbeek and Wendelin Serwe
Proceedings third workshop on models for formal analysis of real systems and sixth international workshop on verification and program transformation
Volume 268 in EPTCS 268. Open Publishing Association, Thessaloniki, Greece, March, 2018
Abstract PDF Gernot Heiser
For safety's sake: we need a new hardware-software contract!
IEEE Design and Test, Volume 35, Issue 2, pp. 27-30, March, 2018
Abstract PDF 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
Abstract PDF Sidney Amani, Myriam Begel, Maksym Bortin and Mark Staples
Towards verifying Ethereum smart contract bytecode in Isabelle/HOL
International Conference on Certified Programs and Proofs, pp. 66-77, Los Angeles, January, 2018
Abstract PDF Rudolf Brghammer, Hitoshi Furusawa, Walter Guttmann and Peter Hoefner
Relational characterisations of paths
Technical Report, Data61, CSIRO, January, 2018
Abstract Slides
Video
Gernot Heiser
Flying autonomous aircraft: Mixed-criticality support in seL4
at linux.conf.au, Sydney, January, 2018
Abstract PDF 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
Abstract
Slides
PDF Rob Sison
Per-thread compositional compilation for confidentiality-preserving concurrent programs
2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018
Abstract PDF 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

Abstract PDF Rob van Glabbeek and Wan Fokkink
Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
Information and Computation, Volume 257, pp. 79-113, December, 2017
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson
Secure mathematically-assured composition of control models
Technical Report, Data61, CSIRO, September, 2017
Abstract PDF Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser
A performance evaluation of rump kernels as a multi-server OS building block on seL4
Asia-Pacific Workshop on Systems (APSys), India, September, 2017
Abstract PDF Wan Fokkink, Rob van Glabbeek and Bas Luttik
Divide and congruence III: Stability & divergence
International Conference on Concurrency Theory (CONCUR), pp. 15:1-15:16, Berlin, Germany, September, 2017
Abstract PDF 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
Abstract PDF 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
Abstract PDF Thomas Sewell, Felix Kam and Gernot Heiser
High-assurance timing analysis for a high-assurance real-time OS
Real-Time Systems, Volume 53, Issue 5, pp. 812-853, September, 2017
Abstract PDF June Andronick
Reasoning about concurrency in high-assurance, high-performance software systems
International Conference on Automated Deduction, pp. 1–7, Gothenburg, August, 2017
Abstract PDF Victor Dyseryn, Rob van Glabbeek and Peter Hoefner
Analysing mutual exclusion using process algebra with signals
Combined International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS), Berlin, August, 2017
Abstract PDF Wan Fokkink and Rob van Glabbeek
Precongruence formats with lookahead through modal decomposition
26th EACSL Annual Conference on Computer Science Logic (CSL'17), Stockholm, Sweden, August, 2017
Abstract PDF Rob van Glabbeek
Lean and full congruence formats for recursion
Annual IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, August, 2017
Abstract PDF Nicolas Bordenabe, Annabelle McIver, Carroll Morgan and Tahiry Rabehaja
Reasoning about distributed secrets
FORTE, pp. 156-170, Shanghai, June, 2017
Abstract PDF 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
Abstract PDF 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
Abstract PDF Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish
Verified characteristic formulae for CakeML
European Symposium on Programming, pp. 584–610, Uppsala, Sweden, April, 2017
Abstract to be published 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
Abstract PDF Holger Hermanns and Peter Hoefner
Preface: Proceedings of the 2nd workshop on models for formal analysis of real systems
Electronic Proceedings in Theoretical Computer Science, pp. -, 2017
Abstract PDF Peter Hoefner, Damien Pous and Georg Struth
Preface: Proceedings of the 16th conference on relational and algebraic methods in computer science
Lecture Notes in Computer Science, pp. 2, 2017
Abstract PDF Rob van Glabbeek and Peter Hoefner
Split, send, reassemble: A formal specification of a CAN bus protocol stack
2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), pp. 14-52, Uppsala, Sweden, April, 2017
Abstract PDF Peter Hoefner and Holger Hermanns
Proceedings of the 2nd workshop on models for formal analysis of real systems
2nd Workshop on Models for Formal Analysis of Real Systems, Uppsala, Sweden, March, 2017
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Rob van Glabbeek
A branching time model of CSP
Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 272-293, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017
Abstract PDF Qian Ge, Yuval Yarom, Frank Li and Gernot Heiser
Your processor leaks information — and there's nothing you can do about it
arXiv preprint arXiv:1612.04474, 2017

2016

Abstract PDF Rudolf Berghammer, Nikita Danilenko, Peter Hoefner and Insa Stucke
Cardinality of relations with applications
Discrete Mathematics, Volume 339, Number 12, pp. 3089–3115, December, 2016
Abstract PDF Rob van Glabbeek
An algebraic treatment of recursion
Liber Amicorum for Jan Bergstra, pp. 58-59, University of Amsterdam, 2016
Abstract PDF 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.
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Wan Fokkink and Rob van Glabbeek
Divide and congruence II: delay and weak bisimilarity
Annual IEEE Symposium on Logic in Computer Science, pp. 778–787, New York City, USA, July, 2016
Abstract PDF 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
Abstract PDF 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
Abstract PDF Peter Hoefner and Bernhard Möller
Extended feature algebra
Journal of Logical and Algebraic Methods in Programming, Volume 85, Number 5, pp. 952–971, June, 2016
Abstract PDF Yi Lin, Steve Blackburn, Tony 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
Abstract PDF Toby Murray, Rob Sison, Ed 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
Abstract PDF Rudolf Berghammer, Peter Hoefner and Insa Stucke
Cardinality of relations and relational approximation algorithms
Journal of Logical and Algebraic Methods in Programming, Volume 85, Number 2, pp. 269–286, May, 2016
Abstract PDF 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
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing (extended abstract)
European Symposium on Programming, pp. 95–122, Eindhoven, The Netherlands, April, 2016
Abstract PDF Wan Fokkink and Rob van Glabbeek
Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
Technical Report 9351, NICTA, April, 2016
Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Mechanizing a process algebra for network protocols
Journal of Automated Reasoning, Volume 56, Number 3, pp. 309–341, March, 2016
Abstract PDF 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
Abstract PDF 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
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing
Technical Report, NICTA, February, 2016

2015

Abstract PDF 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
Abstract
Slides
PDF 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
Abstract PDF Peter Hoefner
Using process algebra to design better protocols (abstract)
Forum “Math-for-Industry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015
Abstract PDF Rudolf Berghammer, Peter Hoefner and Insa Stucke
Tool-based verification of a relational vertex coloring program
International Conference on Relational and Algebraic Methods in Computer Science, pp. 18, Braga, September, 2015
Abstract PDF Mojgan Kamali, Peter Hoefner, Maryam Kamali and Luigia Petre
Formal analysis of proactive, distributed routing
Software Engineering and Formal Methods, pp. 15, York, UK, September, 2015
Abstract PDF 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
Abstract PDF Yuval Yarom, Qian Ge, Fangfei Liu, Ruby B. Lee and Gernot Heiser
Mapping the Intel last-level cache
The Cryptology ePrint Archive, September, 2015
Abstract PDF 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
Abstract PDF 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
Abstract PDF Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of a component platform
Technical Report, NICTA and UNSW, August, 2015
Abstract PDF Kirstin Peters and Rob van Glabbeek
Analysing and comparing encodability criteria
Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, pp. 46–60, Madrid, Spain, August, 2015
Abstract PDF 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
Abstract PDF 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
Abstract
Slides
PDF Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach
From non-preemptive to preemptive scheduling using synchronization synthesis
International Conference on Computer Aided Verification, San Francisco, USA, July, 2015
Abstract PDF 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
Abstract PDF 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
Abstract
Slides
PDF 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
Abstract PDF Peter Gammie, Tony Hosking and Kai Engelhardt
Relaxing safely: verified on-the-fly garbage collection for x86-TSO
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 11, Portland, Oregon, United States, June, 2015
Abstract PDF Yi Lin, Stephen M. Blackburn, Kunshan Wang, Tony Hosking and Michael Norrish
Stop and go: Understanding yieldpoint behavior
International Symposium on Memory Management, pp. 70–80, Portland, OR, USA, June, 2015
Abstract
Slides
PDF Carroll Morgan
a nondeterministic lattice of information
One-hour invited talk at Mathematics of Program Construction, Königswinter, Germany, June, 2015
Abstract PDF Wolfram Kahl, Timothy G. Griffin and Peter Hoefner
Preface: Special issue on relational and algebraic methods in computer science
Journal of Logical and Algebraic Methods in Programming, Volume 84, Number 3, pp. 283–284, May, 2015
Abstract PDF 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
Abstract PDF 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
Abstract PDF Kunshan Wang, Yi Lin, Stephen M Blackburn, Michael Norrish and Tony Hosking
Draining the swamp: Micro virtual machines as a solid foundation for language development
SNAPL, pp. 321–336, Asilomar, California, May, 2015
Abstract PDF Franck Cassez, Takashi Matsuoka, Ed Pierzchalski and Nathan Smyth
Perentie: Modular trace refinement and selective value tracking
SV-COMP-2015, pp. 439–442, London, UK, April, 2015
Abstract PDF Don Batory, Peter Hoefner, Dominik Köppl and Bernhard Möller
Structured document algebra in action
Lecture Notes in Computer Science, Volume 8950, pp. 291–311, March, 2015
Abstract Slides Gernot Heiser
seL4: Present and future
invited talk at FOSDEM'15, Brussels, BE, February, 2015
Abstract PDF 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
Abstract Slides
Video
Peter Chubb
SD cards and filesystems for embedded systems
linux.conf.au, Auckland, NZ, January, 2015
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
SAT-based strategy extraction in reachability games
AAAI, Austin, TX, USA, January, 2015
Abstract Slides
Video
Gernot Heiser
seL4 is free — what does this mean for you?
Abstract, LCA.
Abstract PDF 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
plain text to be published 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

Abstract PDF 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
Abstract
Slides
PDF Anna Lyons and Gernot Heiser
Mixed-criticality support in a high-assurance, general-purpose microkernel
Workshop on Mixed Criticality Systems, pp. 9–14, Rome, Italy, December, 2014
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
A mechanized proof of loop freedom of the (untimed) AODV routing protocol
International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 47–63, Sydney, Australia, November, 2014
Abstract PDF 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
Abstract PDF Matthias Daum, Nelson Billing and Gerwin Klein
Concerned with the unprivileged: User programs in kernel refinement
Formal Aspects of Computing, Volume 26, Number 6, pp. 1205–1229, October, 2014
Abstract PDF 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
Abstract
Slides
PDF Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm and Mona Vij
User-guided device driver synthesis
USENIX Symposium on Operating Systems Design and Implementation, pp. 661–676, Broomfield, CO, USA, October, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014
Abstract PDF 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
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Technical Report NRL-8281, NICTA, August, 2014
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Showing invariance compositionally for a process algebra for network protocols
International Conference on Interactive Theorem Proving, pp. 44–59, Vienna, Austria, July, 2014
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Regression-free synthesis for concurrency
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Real reward testing for probabilistic processes
Theoretical Computer Science, Volume 538, pp. 16–36, July, 2014
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Interpolants in two-player games
Abstract, iPRA workshop, July, 2014.
Abstract PDF 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
Abstract PDF Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Practical CNF interpolants via BDDs
Abstract, iPRA workshop, July, 2014.
Abstract PDF 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
Abstract PDF 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
Abstract PDF Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Christopher Walker
Solving games without controllable predecessor
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF 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
Abstract PDF Thomas Sewell
Formal replay of translation validation for highly optimised c: Work in progress
Verification and Program Transformation, Vienna, Austria, July, 2014
Abstract
Slides
PDF 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
Abstract PDF 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, pp. 429–439, Edinburgh, UK, June, 2014
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu
Automatic verification of active device drivers
ACM Operating Systems Review, Volume 48, Number 1, May, 2014
Abstract PDF Peter Hoefner, Peter Jipsen, Wolfram Kahl and Martin Eric Müller
Preface: Relational and algebraic methods in computer science
Lecture Notes in Computer Science, pp. 2, 2014
Abstract PDF Gerwin Klein
Proof engineering challenges for large-scale verification
Abstract, AI4FM/2014 Workshop.
Abstract PDF 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
Abstract PDF Rudolf Berghammer, Peter Hoefner and Insa Stucke
Automated verification of relational while-programs
International Conference on Relational and Algebraic Methods in Computer Science, pp. 16, Marienstatt im Westerwald, Germany, April, 2014
Abstract
Slides
PDF Bernard Blackham, Mark Liffiton and Gernot Heiser
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 169–178, Berlin, Germany, April, 2014
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
Unifying DVFS and offlining in mobile multicores
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 287–296, Berlin, Germany, April, 2014
Abstract PDF Peter Hoefner and Annabelle McIver
Hopscotch—reaching the target hop by hop
Journal of Logical and Algebraic Methods in Programming (JLAMP), Volume 83, Number 2, pp. 212–224, April, 2014
Abstract
Slides
PDF Gerwin Klein
Proof engineering considered essential
International Symposium on Formal Methods (FM), pp. 16–21, Singapore, April, 2014
Abstract PDF 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
Abstract PDF 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
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract PDF 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

Abstract PDF 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
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV
Technical Report 5513, NICTA, December, 2013
Abstract PDF Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Christopher Walker and Alexander Legg
Device driver synthesis
Intel Technology Journal, Volume 17, Number 2, pp. 136–157, December, 2013
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
Mobile multicores: Use them or waste them
Workshop on Power Aware Computing and Systems, pp. 5, Farmington, PA, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 44-48.
Abstract
Slides
PDF
Presentation Video
Kevin Elphinstone and Gernot Heiser
From L3 to seL4 – what have we learnt in 20 years of L4 microkernels?
ACM Symposium on Operating Systems Principles, pp. 133–150, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF 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.
Abstract PDF Don Batory, Peter Hoefner, Bernhard Möller and Andreas Zelend
Features, modularity, and variation points
Fifth International Workshop on Feature-Oriented Software Development (FOSD), pp. 8, Indianapolis, Indiana, USA, October, 2013
Abstract
Slides
PDF 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
Abstract
Slides
PDF 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
Abstract PDF 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
Abstract PDF Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta
Topology-based mobility models for wireless networks
International Conference on Quantitative Evaluation of SysTems, pp. 16, Buenos Aires, Argentina, August, 2013
Abstract PDF Peter Hoefner and Maryam Kamali
Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking
International Conference on Formal Modeling and Analysis of Timed Systems, pp. 15, Buenos Aires, Argentina, August, 2013
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
The systems hacker’s guide to the Galaxy: Energy usage in a modern smartphone
Asia-Pacific Workshop on Systems (APSys), pp. 7, Singapore, July, 2013
Best Student Paper Award
Abstract PDF 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
Abstract
Slides
PDF Gernot Heiser
Can truly dependable systems be affordable?
Keynote at APSys'13, Singapore, July, 2013
Abstract
Slides
PDF Michael Norrish and Brian Huffman
Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$
International Conference on Interactive Theorem Proving, pp. 133–146, Rennes, France, July, 2013
Abstract
Slides
PDF 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
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013
Abstract
Slides
PDF 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
Abstract PDF Peter Hoefner and Annabelle McIver
Statistical model checking of wireless mesh routing protocols
5th NASA Formal Methods Symposium (NFM 2013), pp. 15, Moffett Field, CA, USA, May, 2013
Abstract
Slides
PDF 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
Abstract PDF 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.
Abstract PDF 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
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Sequoll: A framework for model checking binaries
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 97–106, Philadelphia, USA, April, 2013
Best Paper Award
Abstract
Slides
PDF Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie and Gustavo Alonso
RapiLog: reducing system complexity through verification
EuroSys Conference, pp. 323–336, Prague, Czech Republic, April, 2013
Abstract PDF 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
Abstract
Slides
PDF Gernot Heiser
Protecting e-government against attacks
EP Workshop on Security of e-Government, pp. 5, Brussels, Belgium, February, 2013
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Daniel Matichuk
Automatic function annotations for hoare logic
Systems Software Verification, pp. 10, Sydney, Australia, November, 2012
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Matthew Fernandez, Ihor Kuz and Gerwin Klein
Formalisation of a component platform
Poster presented at Operating Systems Design and Implementation 2012, October, 2012
Abstract PDF Peter Hoefner and Sarah Edenhofer
Towards a rigorous analysis of AODVv2 (DYMO)
2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), pp. 1–6, Austin, Texas, October, 2012
Abstract PDF Peter Hoefner, Rob van Glabbeek, Wee Lum Tan, Marius Portmann, Annabelle McIver and Ansgar Fehnker
A rigorous analysis of AODV and its variants
15th ACM/IEEE International Conference on Modelling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM 2012), pp. 203–212, Paphos, Cyprus, October, 2012
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
Active device drivers
Technical Report, NICTA, September, 2012
Abstract PDF 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
Abstract PDF Peter Hoefner, Bernhard Möller and Andreas Zelend
Foundations of coloring algebra with consequences for feature-oriented programming
International Conference on Relational and Algebraic Methods in Computer Science, pp. 16, Cambridge, UK, September, 2012
Abstract PDF June Andronick and Gerwin Klein
Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022
Technical Report, NICTA, August, 2012
Abstract PDF 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
Abstract PDF 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
Abstract PDF Peter Hoefner
Towards a representation theorem for coloring algebra
Abstract, Workshop on Lattices and Relations, August, 2012.
Abstract PDF Peter Hoefner
Kleene modules for routing procedures
Abstract, Workshop on Lattices and Relations, August, 2012.
Abstract PDF Gerwin Klein, Rafal Kolanski and Andrew Boyton
Mechanised separation algebra
International Conference on Interactive Theorem Proving, pp. 332–337, Princeton, USA, August, 2012
Abstract PDF Ihor Kuz, Liming Zhu, Len Bass, Mark Staples and 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
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Correct, fast, maintainable — choose any three!
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract
Slides
PDF Bernard Blackham, Vernon Tang and Gernot Heiser
To preempt or not to preempt, that is the question
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract PDF 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
Abstract PDF Peter Hoefner, Rob van Glabbeek and Ian Hayes
Preface—Morgan: A suitable case for treatment
Formal Aspects of Computing, Volume 24, Number 4-6, pp. 417–422, July, 2012
Abstract PDF Peter Hoefner and Bernhard Möller
Dijkstra, Floyd and Warshall meet Kleene
Formal Aspects of Computing (FAOC), Volume 24, Number 4-6, pp. 459–476, July, 2012
Abstract PDF June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, 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
Abstract PDF 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
Abstract PDF June Andronick, Gerwin Klein and Andrew Boyton
Formal system verification — extension, AOARD 114070
Technical Report, NICTA, May, 2012
Abstract PDF Wan Fokkink, Rob van Glabbeek and Paulien de Wind
Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity
Information and Computation, Volume 214, Number , pp. 59–85, May, 2012
Abstract
Slides
PDF Bernard Blackham, Yao Shi and Gernot Heiser
Improving interrupt response time in a verifiable protected microkernel
EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012
Abstract PDF Matthew Fernandez, Gerwin Klein and Ihor Kuz
Microkernel verification down to assembly
Poster presented at EuroSys 2012, April, 2012
Abstract PDF Gerwin Klein
Interactive proof: Applications to semantics
Software Safety and Security: Tools for Analysis and Verification, pp. 85–125, IOS Press, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
A process algebra for wireless mesh networks
European Symposium on Programming, pp. 295–315, Tallinn, Estonia, March, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Automated analysis of AODV using UPPAAL
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 173–187, Tallinn, Estonia, March, 2012
Abstract PDF 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
Abstract Video Peter Chubb
Bourne shell tutorial
Tutorial at Linux.conf.au, Ballarat, January, 2012
Abstract Video Peter Chubb
Linux as a boot loader
Talk at linux.conf.au, Ballarat, January, 2012
Abstract PDF Stefan M. Petters, Kevin Elphinstone and Gernot Heiser
Trustworthy real-time systems
Advances in Real-Time Systems, pp. 191–206, Springer, 2012

2011

Abstract PDF 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
Abstract PDF Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser
Timing analysis of a protected operating system kernel
IEEE Real-Time Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Modelling and analysis of AODV in UPPAAL
1st International Workshop on Rigorous Protocol Engineering, pp. 1–6, Vancouver, October, 2011
Abstract PDF Peter Hoefner, Don Batory and Jongwook Kim
Feature interactions, products, and composition
Generative Programming and Component Engineering (GPCE'11), pp. 13–22, Portland, OR, United States, October, 2011
Abstract
Slides
PDF Michael Norrish
Mechanised computability theory
International Conference on Interactive Theorem Proving, pp. 297—311, Nijmegen, The Netherlands, August, 2011
Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
Abstract PDF 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
Abstract PDF Bernard Blackham, Yao Shi and Gernot Heiser
Protected hard real-time: The next frontier
Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011
Abstract PDF Yuxin Deng, Rob 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
Abstract PDF Peter Hoefner, Ridha Khedri and Bernhard Möller
Supplementing product families with behaviour
International Journal of Software and Informatics (IJSI), Volume 5, Number 1-2, Part II, pp. 245–266, July, 2011
Abstract PDF Prashant Varanasi and Gernot Heiser
Hardware-supported virtualization on ARM
Asia-Pacific Workshop on Systems (APSys), pp. 5 pages, Shanghai, China, July, 2011
Abstract PDF Han-Hing Dang, Bernhard Möller and Peter Hoefner
Algebraic separation logic
The Journal of Logic and Algebraic Programming, Volume 80, Number 6, pp. 221–247, June, 2011
Abstract PDF Gernot Heiser
Virtualizing embedded systems — why bother?
Design Automation Conference (DAC), pp. 901–905, Dan Diego, CA, USA, June, 2011
Abstract PDF Peter Hoefner and Bernhard Möller
Fixing zeno gaps
Theoretical Computer Science, Volume 412, Number 28, pp. 3303–3322, June, 2011
Abstract PDF Etienne Le Sueur and Gernot Heiser
Slow down or sleep, that is the question
USENIX Technical Conference, Portland, Oregon, USA, June, 2011
Abstract
Slides
PDF Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski
What if you could actually Trust your kernel?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011
Abstract PDF Peter Hoefner and Annabelle McIver
Towards an algebra of routing tables
12th International Conference on Relational and Algebraic Methods in Computer Science, pp. 212–229, Rotterdam, Netherlands, May, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 5, Napa, USA, May, 2011
Abstract PDF Ihor Kuz, Zachary Anderson, Pravin Shinde and Timothy Roscoe
Multicore OS benchmarks: we can do better
Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011
Abstract PDF June Andronick and Gerwin Klein
Formal system verification for trustworthy embedded systems, final report AOARD 094160
Technical Report, NICTA, April, 2011
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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.
Abstract PDF 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
Abstract PDF Yuxin Deng and Rob 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
Abstract PDF 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
Abstract PDF Etienne Le Sueur and Gernot Heiser
Dynamic voltage and frequency scaling: The laws of diminishing returns
Workshop on Power Aware Computing and Systems, pp. 1–5, Vancouver, Canada, October, 2010
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Gernot Heiser and Ben Leslie
The OKL4 microvisor: Convergence point of microkernels and hypervisors
Asia-Pacific Workshop on Systems (APSys), pp. 19–24, New Delhi, India, August, 2010
Abstract PDF Gerwin Klein
The l4.verified project – next steps
Verified Software: Theories, Tools and Experiments, pp. 86–96, Edinburgh, UK, August, 2010
Abstract PDF Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker
capDL: A language for describing capability-based systems
Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010
Abstract PDF Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser
The case for active device drivers
Asia-Pacific Workshop on Systems (APSys), pp. 25–30, New Delhi, India, August, 2010
Abstract PDF 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
Abstract PDF Gerwin Klein
A formally verified OS kernel. now what?
International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010
Abstract
Slides
PDF Ramana Kumar and Michael Norrish
(nominal) unification by recursive descent with triangular substitutions
International Conference on Interactive Theorem Proving, pp. 51–66, Edinburgh, United Kingdom, July, 2010
Abstract PDF 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
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010
Research Highlights paper
Abstract PDF 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
Abstract PDF
Presentation Video
Peter Chubb
Decent MIDI from LilyPond
Linux.conf.au, January, 2010
Abstract PDF Peter Chubb and John Judge
When the arduino meets year 9
Other Conference Presentation, linux.conf.au, Wellington, New Zealand, January, 2010.
Abstract PDF Peter Chubb and Yang Song
Interrupts considered harmful
Other Conference Presentation, Linux.conf.au, Wellington, NZ, January, 2010.

2009

Abstract PDF Gerwin Klein
Correct OS kernel? Proof? Done!
USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009
Abstract PDF Andrew Boyton
A verified shared capability model
Systems Software Verification, pp. 25–44, Aachen, Germany, October, 2009
Abstract PDF 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
Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Best Paper Award
Hall of Fame Award
Abstract PDF Michael Norrish
Rewriting conversions implemented with continuations
Journal of Automated Reasoning, Volume 43, Number 3, pp. 305–336, October, 2009
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009
Abstract PDF Yuxin Deng, Rob 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
Abstract PDF 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
Abstract PDF Stefan M. Petters, Martin Lawitzky, Ryan Heffernan and Kevin Elphinstone
Towards real multi-criticality scheduling
IEEE Conference on Embedded and Real-Time Computing and Applications, pp. 155–164, Beijing, China, August, 2009
Abstract PDF 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
Abstract PDF Matthew Chapman and Gernot Heiser
vNUMA: A virtual shared-memory multiprocessor
USENIX Annual Technical Conference, pp. 349–362, San Diego, USA, June, 2009
Abstract PDF Gerwin Klein, Ralf Huuck and Bastian Schlich
Operating system verification
Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser
Dingo: Taming device drivers
EuroSys Conference, pp. 275–288, Nuremberg, DE, April, 2009
Abstract PDF 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
Abstract PDF Aditi Barthwal and Michael Norrish
Verified, executable parsing
European Symposium on Programming, pp. 160–174, York, March, 2009
Abstract PDF James Cheney, René Vestergaard and Michael Norrish
Formalizing adequacy
2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming, York, March, 2009
Abstract PDF 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
Abstract PDF Gernot Heiser
Many-core chips — a case for virtual shared memory
Workshop on Managed Many-Core Systems, pp. 4 pages, Washington, DC, USA, March, 2009
Abstract PDF Gerwin Klein
Operating system verification — an overview
Sadhana, Volume 34, Number 1, pp. 26–69, February, 2009
Invited paper. Journal homepage.
Abstract PDF Taolue Chen, Wan Fokkink and Rob van Glabbeek
On finite bases for weak semantics: Failures versus impossible futures
35th Conference on Current Trends in Theory and Practice of Computer Science, pp. 167–180, Spindleruv Mlyn, Czech Republic , January, 2009
Abstract PDF Gernot Heiser
Hypervisors for consumer electronics
IEEE Consumer Communications and Networking Conference, pp. 1–5, Las Vegas, NV, USA, January, 2009

2008

Abstract PDF Taolue Chen, Wan Fokkink and Rob van Glabbeek
Ready to preorder: The case of weak process semantics
Information Processing Letters, Volume 109, Number 2, pp. 104–111, December, 2008
Abstract PDF André Hergenhan and Gernot Heiser
Operating systems technology for converged ECUs
Embedded Security in Cars Conference (escar), pp. 3 pages, Hamburg, Germany, November, 2008
Abstract PDF 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
Abstract PDF Yuxin Deng, Rob 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
Abstract PDF 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
Abstract PDF Rafal Kolanski and Gerwin Klein
Mapped separation logic
Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008
Abstract PDF
5th international verification workshop — VERIFY'08
CEUR Workshop Proceedings, 2008
Abstract PDF David Cock
Bitfields and tagged unions in C — verification through automatic generation
International Verification Workshop, pp. 44–55, Sydney, August, 2008
Abstract PDF 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
Abstract PDF Joshua LeVasseur, Volkmar Uhlig, Yaowei Yang, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser
Pre-virtualization: Soft layering for virtual machines
Asia-Pacific Computer Systems Architecture Conference, pp. 1–9, Hsinchu, Taiwan, August, 2008
Best Paper Award
Abstract PDF 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
Abstract PDF
Proceedings of the 3rd international workshop on systems software verification (SSV 2008)
Volume 217 in ENTCS, Elsevier, 2008
Abstract PDF Rafal Kolanski
A logic for virtual memory
Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008
Abstract PDF Gernot Heiser
Trusted ⇐ trustworthy ⇐ proof – Position paper
Conference on Future of Trust in Computing, pp. 55–59, Berlin, DE, May, 2008
Abstract PDF 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
Abstract PDF 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
Abstract PDF Gernot Heiser
The role of virtualization in embedded systems
Workshop on Isolation and Integration in Embedded Systems, pp. 11–16, Glasgow, UK, April, 2008
Abstract PDF
Presentation Video
Gernot Heiser
Do microkernels suck?
Other Conference Presentation, Linux.conf.au, Melbourne, Australia, January, 2008.
Abstract PDF Ihor Kuz and Yan 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

Abstract PDF 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
Abstract PDF Gernot Heiser
Your system is secure? Prove it!
USENIX ;login:, Volume 32(6), pp. 35—38, December, 2007
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Michael Norrish
A formal semantics for c++
Technical Report, NICTA, November, 2007
Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 2007
Abstract PDF 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
Abstract PDF 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
Abstract PDF Yuxin Deng, Rob 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF 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
Abstract PDF Yuxin Deng, Rob 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
Abstract PDF Yuxin Deng, Rob 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
Abstract PDF 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

Abstract PDF Kevin Elphinstone and Scott Brandt
Proceedings of the 2007 workshop on operating system platforms for embedded real-time applications
Technical Report, NICTA, July, 2006
Abstract PDF 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

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

2004

Abstract
Slides
PDF Michael Norrish
Recursive function definition for types with binders
International Conference on Theorem Proving in Higher Order Logics, pp. 241—256, Park City, Utah, United States, September, 2004

2003

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

Abstract PDF Shane Stephens and Gernot Heiser
Fault tolerance and avoidance in biomedical systems
SIGOPS European Workshop, St Emilion, France, September, 2002
Abstract PDF Daniel Potts, Simon Winwood and Gernot Heiser
Design and implementation of the L4 microkernel for Alpha multiprocessors
Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002
Abstract PDF 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
Abstract PDF Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser
Performance of address-space multiplexing on the Pentium
Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002

2001

Abstract PDF Gernot Heiser
Dealing with TLB tags
International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PDF 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
Abstract PDF Daniel Potts, Simon Winwood and Gernot Heiser
L4 reference manual: Alpha 21x64
Technical Report UNSW-CSE-TR-0104, School of Computer Science and Engineering, March, 2001
Abstract PDF Alan Au and Gernot Heiser
Enhancing IA64 memory management
Linux.conf.au, Sydney, Australia, January, 2001
Abstract PDF Antony Edwards and Gernot Heiser
Components + Security = OS Extensibility
Asia-Pacific Computer Systems Architecture Conference, pp. 27–34, Gold Coast, Australia, January, 2001
Abstract PDF Gernot Heiser
Inside L4/MIPS: Anatomy of a high-performance microkernel
Sydney, Australia, January, 2001

2000

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

1999

Abstract PDF Luke Deller and Gernot Heiser
Linking programs in a single address space
USENIX, pp. 283–294, Monterey, Ca, USA, June, 1999
Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual: MIPS R4x00, version 1.11, kernel version 79
Sydney, Australia, May, 1999
Abstract PDF 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

Abstract PDF Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke
The Mungi single-address-space operating system
Software: Practice and Experience, Volume 28, Number 9, pp. 901–928, July, 1998
Abstract PDF 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

Abstract PDF Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam and Trent Jaeger
Achieved IPC performance (still the foundation for extensibility)
Workshop on Hot Topics in Operating Systems (HotOS), pp. 28–31, Cape Cod, MA, USA, May, 1997

1996

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

1995

Abstract PDF Tim Wilkinson, Kevin Murray, Stephen Russell, Gernot Heiser and Jochen Liedtke
Single address space operating systems
Technical Report UNSW-CSE-TR-9504, UNSW, November, 1995
Abstract PDF 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

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

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

1992

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

Pre-TS Publications

These publications are from work of the UNSW OS group (DiSy) which used to be co-located with the Trustworthy Systems group. They include outcomes of ARC-funded projects and pre-NICTA work of the group.

2009

Abstract PDF Joshua LeVasseur
Device-driver reuse via virtual machines
PhD Thesis, UNSW, Sydney, Australia, May, 2009

2008

Abstract PDF Ian Wienand
Transparent large-page support for Itanium Linux
ME Thesis, UNSW, Sydney, Australia, July, 2008
Abstract PDF Daniel Potts
Eidolon: Adapting distributed applications to their environment
PhD Thesis, UNSW, Sydney, Australia, January, 2008

2006

Abstract PDF Myrto Zehnder and Peter Chubb
Virtualising PCI
Gelato ICE, Singapore, October, 2006
Abstract PDF Shehjar Tikoo and Peter Chubb
Improving NFS performance
Gelato ICE conference, San Jose, CA, April, 2006

2005

Abstract PDF Peter Chubb
Bugs: getting them stomped!
Gelato ICE, Brazil, October, 2005
Abstract PDF Peter Chubb
Which filesystem?
Gelato ICE, Brazil, October, 2005
Abstract PDF Peter Chubb and Darren Williams
Linux scalability — from the micro to the HUGE
Linux.conf.au, Canberra, ACT, April, 2005

2004

Abstract PDF Peter Chubb
Get more device drivers out of the kernel!
Ottawa Linux Symposium, Ottawa, Canada, July, 2004
Abstract PDF Peter Chubb
Linux kernel infrastructure for user-level device drivers
Linux.conf.au, Adelaide, Australia, January, 2004

2003

Abstract PDF Peter Chubb
Where's all the time going? Microstate accounting in Linux 2.5
Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Australia, September, 2003
Abstract PDF Andreas Haeberlen and Kevin Elphinstone
User-level management of kernel memory
Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
Abstract PDF 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

Abstract PDF Peter Chubb
Terabytes on a diet
Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Australia, September, 2002
Abstract PDF Shane Stephens and Gernot Heiser
Fault tolerance and avoidance in biomedical systems
SIGOPS European Workshop, St Emilion, France, September, 2002
Abstract PDF Peter Chubb
YOU ARE LOST in a maze of BitKeeper repositories — all almost the same
Australian Open Source Symposium, Sydney, Australia, July, 2002
Abstract PDF Simon Winwood, Yefim Shuf and Hubertus Franke
Multiple page size support in the Linux kernel
Ottawa Linux Symposium, Ottawa, Canada, June, 2002
Abstract PDF Daniel Potts, Simon Winwood and Gernot Heiser
Design and implementation of the L4 microkernel for Alpha multiprocessors
Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002
Abstract PDF 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
Abstract PDF Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser
Performance of address-space multiplexing on the Pentium
Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002

2001

Abstract PDF Gernot Heiser
Dealing with TLB tags
International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PDF Chris Szmajda
Calypso: A portable translation layer
International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PDF Antony Edwards and Gernot Heiser
Secure OS extensibility needn't cost an arm and a leg
Workshop on Hot Topics in Operating Systems (HotOS), pp. 168, Schloss Elmau, DE, May, 2001
Abstract PDF Antony Edwards and Gernot Heiser
A component architecture for system extensibility
Technical Report UNSW-CSE-TR-0103, School of Computer Science and Engineering, March, 2001
Abstract PDF Daniel Potts, Simon Winwood and Gernot Heiser
L4 reference manual: Alpha 21x64
Technical Report UNSW-CSE-TR-0104, School of Computer Science and Engineering, March, 2001
Abstract PDF 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
Abstract PDF Alan Au and Gernot Heiser
Enhancing IA64 memory management
Linux.conf.au, Sydney, Australia, January, 2001
Abstract PDF Antony Edwards and Gernot Heiser
Components + Security = OS Extensibility
Asia-Pacific Computer Systems Architecture Conference, pp. 27–34, Gold Coast, Australia, January, 2001
Abstract PDF Gernot Heiser
Inside L4/MIPS: Anatomy of a high-performance microkernel
Sydney, Australia, January, 2001

2000

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

1999

Abstract PDF Luke Deller and Gernot Heiser
Linking programs in a single address space
USENIX, pp. 283–294, Monterey, Ca, USA, June, 1999
Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual: MIPS R4x00, version 1.11, kernel version 79
Sydney, Australia, May, 1999
Abstract PDF Kevin Elphinstone
Virtual memory in a 64-bit microkernel
PhD Thesis, UNSW, Sydney, Australia, March, 1999
Abstract PDF Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko and Yoonho Park
Flexible access control using IPC redirection
Workshop on Hot Topics in Operating Systems (HotOS), pp. 191–196, Rio Rico, AZ, USA, March, 1999
Abstract PDF 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

Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
Page tables for 64-bit computer systems
Technical Report UNSW-CSE-TR-9804, School of Computer Science and Engineering, August, 1998
Abstract PDF Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke
The Mungi single-address-space operating system
Software: Practice and Experience, Volume 28, Number 9, pp. 901–928, July, 1998
Abstract PDF Jerry Vochteloo
Design, implementation and performance of protection in the Mungi single-address-space operating system
PhD Thesis, UNSW, Sydney, Australia, July, 1998
Abstract PDF Alan Au and Gernot Heiser
L4 User Manual — version 1.0
Technical Report UNSW-CSE-TR-9801, School of Computer Science and Engineering, April, 1998
Abstract PDF 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

Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual – MIPS R4x00 — Version 1.0
Technical Report UNSW-CSE-TR-9709, School of Computer Science and Engineering, December, 1997
Abstract PDF Gernot Heiser, Fondy Lam and Stephen Russell
Resource management in the Mungi single-address-space operating system
Technical Report UNSW-CSE-TR-9705, UNSW, August, 1997
Abstract PDF Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke
Implementation and performance of the Mungi single-address-space operating system
Technical Report UNSW-CSE-TR-9704, UNSW, June, 1997
Abstract PDF Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam and Trent Jaeger
Achieved IPC performance (still the foundation for extensibility)
Workshop on Hot Topics in Operating Systems (HotOS), pp. 28–31, Cape Cod, MA, USA, May, 1997
Abstract PDF Gernot Heiser, Jerry Vochteloo, Kevin Elphinstone and Stephen Russell
The Mungi kernel API/Release 1.0
Technical Report UNSW-CSE-TR-9701, School of Computer Science and Engineering, March, 1997

1996

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Jochen Liedtke and Kevin Elphinstone
Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization
ACM Operating Systems Review, Volume 30, Number 1, pp. 4–15, January, 1996

1995

Abstract PDF Jochen Liedtke and Kevin Elphinstone
Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization
Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, November, 1995
Abstract PDF Tim Wilkinson, Kevin Murray, Stephen Russell, Gernot Heiser and Jochen Liedtke
Single address space operating systems
Technical Report UNSW-CSE-TR-9504, UNSW, November, 1995
Abstract PDF 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

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

Abstract PDF 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
Abstract PDF Kevin Elphinstone
Address space management issues in the Mungi operating system
Technical Report UNSW-CSE-TR-9312, School of Computer Science and Engineering, November, 1993
Abstract PDF Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo
Mungi: A distributed single address-space operating system
Technical Report UNSW-CSE-TR-9314, School of Computer Science and Engineering, November, 1993
Abstract PDF Gernot Heiser, Kevin Elphinstone, Stephen Russell and Graham R. Hellestrand
A distributed single address space system supporting persistence
Technical Report UNSW-CSE-TR-9302, UNSW, March, 1993

1992

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

Post-graduate Student Theses

2023

Abstract PDF Zilin Chen
Towards a practical high-assurance systems programming language
PhD Thesis, UNSW, Sydney, Australia, March, 2023

2020

Abstract
Slides
PDF Rob Sison
Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs
PhD Thesis, UNSW, Sydney, Australia, October, 2020

2019

Abstract PDF Qian Ge
Principled elimination of microarchitectural timing channels through operating-system enforced time protection
PhD Thesis, UNSW, Sydney, Australia, October, 2019
Abstract PDF Liam O'Connor
Type systems for systems types
PhD Thesis, UNSW, Sydney, Australia, August, 2019
Abstract to be published Hira Taqdees Syeda
Low-level program verification under cached address translation
PhD Thesis, UNSW, Sydney, Australia, August, 2019
Abstract PDF Yanyan Shen
Microkernel mechanisms for improving the trustworthiness of commodity hardware
PhD Thesis, UNSW, Sydney, Australia, March, 2019

2018

Abstract PDF Anna Lyons
Mixed-criticality scheduling and resource sharing for high-assurance operating systems
PhD Thesis, UNSW, August, 2018
Abstract PDF Daniel Matichuk
Automation for proof engineering: Machine-checked proofs at scale
PhD Thesis, UNSW, Sydney, Australia, July, 2018
Abstract PDF Mohammad Abdulaziz
Formally verified compositional algorithms for factored transition systems
PhD Thesis, Australian National University, June, 2018

2017

Abstract PDF Thomas Sewell
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, July, 2017
Abstract PDF Aaron Carroll
Understanding and reducing smartphone energy consumption
PhD Thesis, UNSW, Sydney, Australia, May, 2017

2016

Abstract PDF Alexander Legg
A counterexample guided method for reactive synthesis
PhD Thesis, UNSW, Sydney,Australia, September, 2016
Abstract PDF Sidney Amani
A methodology for trustworthy file systems
PhD Thesis, CSE, UNSW, Sydney, Australia, August, 2016
Abstract PDF Matthew Fernandez
Formal verification of a component platform
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016

2015

Abstract PDF David Greenaway
Automated proof-producing abstraction of c code
PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015

2014

Abstract PDF Andrew Boyton
Secure architectures on a verified microkernel
PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014
Abstract PDF David Cock
Leakage in trustworthy systems
PhD Thesis, UNSW, Sydney, Australia, August, 2014

2013

Abstract PDF Michael von Tessin
The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2013
Abstract PDF Bernard Blackham
Towards verified microkernels for real-time mixed-criticality systems
PhD Thesis, UNSW, Sydney, Australia, October, 2013
2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation

2011

Abstract PDF Rafal Kolanski
Verification of programs in virtual memory using separation logic
PhD Thesis, UNSW, Sydney, Australia, July, 2011
Abstract PDF Etienne Le Sueur
An analysis of the effectiveness of energy management on modern computer processors
MSc Thesis, UNSW, Sydney, Australia, June, 2011
Abstract PDF Nicholas FitzRoy-Dale
Architecture optimisation
PhD Thesis, UNSW, Sydney, Australia, March, 2011

2010

Abstract PDF Dhammika Elkaduwe
A principled approach to kernel memory management
PhD Thesis, UNSW, Sydney, Australia, May, 2010
Abstract PDF Dave Snowdon
OS-level power management
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, March, 2010
Abstract PDF Leonid Ryzhyk
On the construction of reliable device drivers
PhD Thesis, UNSW, Sydney, Australia, January, 2010

2009

Abstract PDF Joshua LeVasseur
Device-driver reuse via virtual machines
PhD Thesis, UNSW, Sydney, Australia, May, 2009
Abstract PDF Matthew Chapman
vNUMA: Virtual shared-memory multiprocessors
PhD Thesis, UNSW, Sydney, Australia, March, 2009

2008

Abstract PDF Harvey Tuch
Formal memory models for verifying C systems code
PhD Thesis, UNSW, Sydney, Australia, August, 2008
Abstract PDF Ian Wienand
Transparent large-page support for Itanium Linux
ME Thesis, UNSW, Sydney, Australia, July, 2008
Abstract PDF Daniel Potts
Eidolon: Adapting distributed applications to their environment
PhD Thesis, UNSW, Sydney, Australia, January, 2008

2007

Abstract PDF Luke Macpherson
Performing under overload
PhD Thesis, UNSW, Sydney, Australia, September, 2007
Abstract PDF Andrew Baumann
Dynamic update for operating systems
PhD Thesis, UNSW, Sydney, Australia, August, 2007

2005

Abstract link Volkmar Uhlig
Scalability of microkernel-based systems
PhD Thesis, University of Karlsruhe, Karlsruhe, DE, June, 2005

1999

Abstract PDF Kevin Elphinstone
Virtual memory in a 64-bit microkernel
PhD Thesis, UNSW, Sydney, Australia, March, 1999

1998

Abstract PDF Jerry Vochteloo
Design, implementation and performance of protection in the Mungi single-address-space operating system
PhD Thesis, UNSW, Sydney, Australia, July, 1998

Selected Undergraduate Student Theses

Below are a selection of honours theses done with the group.

2023

Abstract PDF Lucy Parker
High-performance networking on seL4
BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2023

2022

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

Abstract PDF Sebastian Holzapfel
User-level mixed criticality systems scheduling on multicore processors
BE Thesis, School of Electrical Engineering and Telecommunication, Sydney, Australia, November, 2018
Abstract PDF Jack Suann
Zircon on seL4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, May, 2018

2017

Abstract PDF A. Felizzi
Trianqles: Porting qubes to seL4
BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2017

2016

Abstract PDF Kent McLeod
Usermode OS components on seL4 with rump kernels
BE Thesis, School of Electrical Engineering and Telecommunication, Sydney, Australia, October, 2016

2011

Abstract PDF Alexandra Boulgakov
Sunswift IV strategy for the 2011 World Solar Challenge
BE Thesis, School of Electrical Engineering, Sydney, Australia, November, 2011
Abstract PDF Aleksander Budzynowski
Operating system for a flow-graph machine
BE Thesis, School of Mechanical and Manufacturing Engineering, Sydney, Australia, October, 2011
Abstract PDF Anna Lyons
Efficient concurrency control for high-performance microkernels
BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, July, 2011

2010

Abstract PDF Prashant Varanasi
Implementing hardware-supported virtualization in OKL4 on ARM
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2010
Abstract PDF Josh Matthews
Native OKL4 web browser
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2010

2009

Abstract PDF Michael Hills
Native OKL4 Android stack
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2009
Abstract PDF Andrew Wrigley
Steering-Integrated driver controls for sunswift IV
BE Thesis, School of Electrical Engineering, Sydney, Australia, November, 2009

2008

Abstract PDF Aaron Carroll
I/O scheduling on RAID
BE Thesis, School of Electrical Engineering, Sydney, Australia, July, 2008

2007

Abstract PDF David Greenaway
Quantifying the effects of scheduling on IPC performance
BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2007
Abstract PDF Joshua Root
Virtualising Darwin on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, February, 2007

2006

Abstract PDF 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
Abstract PDF Tom Birch
Performance limits of Darwin on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006

2005

Abstract PDF Geoffrey Lee
I/O kit drivers for L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2005
Abstract PDF Matthew Warton
Single kernel stack L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2005
Abstract PDF Philip Geoffrey Derrin
A secure microkernel
BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2005
Abstract PDF Abi Nourai
A physically-addressed L4 kernel
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, March, 2005

2003

Abstract PS Ka-shu Wong
MacOS X on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, December, 2003

2002

Abstract PS Andrew Baumann
A thread model for Mungi
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002
Abstract PS Ben Leslie
Mungi device drivers
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002
Abstract PDF 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
Abstract PS 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

Abstract PS Antony Edwards
A component architecture for system extensibility
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000
Abstract PS Simon Winwood
Flexible scheduling mechanisms in L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000
Abstract PDF 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

Abstract PS Luke Deller
Loading and debugging tasks in SawMill
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS Vincent Jayawardene
An intensional engine on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS Daniel Potts
L4 on uni- and multiprocessor Alpha
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS Cristan Szmajda
A new virtual memory implementation for L4/MIPS
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS 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