Publications, Theses and Technical Reports
| Paper/Talk Abstract |
|
Paper in PDF format |
|
| Presentation slides |
|
Video of the presentation |
|
| A reference to a location |
|
Paper yet to be published |
|
- Trustworthy Systems Publication Target List
- Best papers from the Trustworthy Systems Group
- All publications from Trustworthy Systems ( 2024, 2023, 2022, 2021, 2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005, 2004, 2003, 2002, 2001, 2000, 1999, 1998, 1997, 1996, 1995, 1994, 1993, 1992 )
- Early publications by the UNSW OS group, before TS ( 2009, 2008, 2006, 2005, 2004, 2003, 2002, 2001, 2000, 1999, 1998, 1997, 1996, 1995, 1994, 1993, 1992 )
- Postgraduate theses
- Selected undergraduate student theses
Our Best Papers
 
|
  |
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award |
|
|
|
Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time EuroSys Conference, Porto, Portugal, April, 2018 |
|
|
|
Gernot Heiser and Kevin Elphinstone L4 microkernels: The lessons from 20 years of research and deployment ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016 |
|
|
|
Thomas Sewell, 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 |
|
|
|
Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith Additive and multiplicative notions of leakage, and their capacities Computer Security Foundations, pp. 308–322, Vienna, Austria, July, 2014 Winner of the 2015 NSA Best Scientific Cybersecurity Paper Award |
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014 |
|
|
|
Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
|
|
|
Aaron Carroll and Gernot Heiser An analysis of power consumption in a smartphone USENIX Annual Technical Conference, pp. 271–284, Boston, MA, US, June, 2010 |
|
|
|
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award |
|
|
|
Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic device driver synthesis with Termite ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009 |
|
|
|
Dave Snowdon, Etienne Le Sueur, Stefan M. Petters and Gernot Heiser Koala: A platform for OS-level power management EuroSys Conference, pp. 289–302, Nuremberg, DE, April, 2009 |
All TS Publications
2024
|
|
|
Gernot Heiser LionsOS: A highly dependable operating system for cyberphysical systems Keynote at International Symposium on Parallel Computing and Distributed Systems, September, 2024 |
|
|
|
Nils Wistoff, Gernot Heiser and Luca Benini fence.t.s: Closing timing channels in high-performance out-of-order cores through ISA-supported temporal partitioning International Conference on Applications in Electronics Pervading Industry, Environment and Society (ApplePies), Turin, IT, September, 2024 |
|
|
|
Gernot Heiser LionsOS: Towards a truly dependable operating system Keynote at International Conference on Dependable Systems and Networks (DSN), June, 2024 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Peter Chubb Running your own mailserver Everything Open, Gladstone, QLD, AU, April, 2024 |
|
|
|
Gernot Heiser Lions OS: secure – fast – adaptable Everything Open, Gladstone, QLD, AU, April, 2024 |
|
|
|
Gernot Heiser, Peter Chubb, Alex Brown, Courtney Darville and Lucy Parker sDDF design: design, implementation and evaluation of the seL4 device driver framework 2024 |
2023
|
|
|
Marcelo Orenes-Vera, Hyunsung Yun, Nils Wistoff, Gernot Heiser, Luca Benini, David Wentzlaff and Margaret Martonosi AutoCC: Automatic discovery of covert channels in time-shared hardware International Symposium on Microarchitecture (MICRO), Toronto, ON, CA, October, 2023 |
|
|
|
Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, 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 |
|
|
|
Gernot Heiser The seL4 microkernel: Provable security for the real world Keynote at the International Workshop on Advanced Industrial Science and Technology, September, 2023 |
|
|
|
Lucy Parker The seL4 device driver framework Talk at the 5th seL4 Summit, September, 2023 |
|
|
|
Ivan Velickovic The seL4 Microkit Talk at the 5th seL4 Summit, September, 2023 |
|
|
|
Mathieu Paturel, Isitha Subasinghe and Gernot Heiser First steps in verifying the seL4 Core Platform Asia-Pacific Workshop on Systems (APSys), Seoul, KR, August, 2023 |
|
|
|
Gernot Heiser Intelligent vehicle security needs a verified operating system Keynote at the International Workshop on Safety and Security of Intelligent Vehicles, June, 2023 |
|
|
|
Gernot Heiser seL4 update: Foundation and TS R&D news Invited talk at the Trusted Computing Center of Excellence 2023 Summit, May, 2023 |
|
|
|
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 |
|
|
|
Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson and Christine Rizkallah Dargent: A silver bullet for verified data layout refinement Proc. ACM Program. Lang., Volume 7, Number POPL, January, 2023 |
|
|
|
Jason Belt, John Hatcliff, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren Cofer, David Hardin, Karl Hoech, Konrad Slind, Ihor Kuz and Kent Mcleod Model-driven development for the seL4 microkernel using the HAMR framework Journal of Systems Architecture, Volume 134, pp. 102789, 2023 |
|
|
|
Scott Buckley, 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 |
|
|
|
Gernot Heiser R&D update from Trustworthy Systems Talk at the 5th seL4 Summit, 2023 |
|
|
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 |
|
|
|
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Gernot Heiser and Luca Benini Systematic prevention of on-core timing channels by full temporal partitioning IEEE Transactions on Computers, Volume 72, Number 5, pp. 1420–1430, 2023 |
2022
|
|
|
Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser and Gabriele Keller Property-based testing: Climbing the stairway to verification ACM SIGPLAN International Conference on Software Language Engineering, Auckland, New Zealand, December, 2022 Distinguished Artifact Award |
|
|
|
Gernot Heiser, Lucy Parker, 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 |
|
|
|
Gernot Heiser State of seL4-related research Keynote at the seL4 Summit, October, 2022 |
|
|
|
Gernot Heiser seL4 overview: Principles, abstractions, use Invited talk at the seL4 Summit, October, 2022 |
|
|
|
Lucy Parker The seL4 device driver framework Talk at the 4th seL4 Summit, October, 2022 |
|
|
|
Arve Gengelbach and Johannes Åman Pohjola A verified cyclicity checker: For theories with overloaded constants International Conference on Interactive Theorem Proving, pp. 15:1–15:18, Haifa, Israel, August, 2022 |
|
|
|
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker and Michael Norrish Kalas: A verified, end-to-end compiler for a choreographic language International Conference on Interactive Theorem Proving, pp. 27:1–27:18, Haifa, Israel, August, 2022 |
|
|
|
Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer and John Shackleton Cyberassured systems engineering at scale IEEE Security and Privacy, Volume 20, Number 3, pp. 52–64, March, 2022 |
|
|
|
Gernot Heiser The seL4 report: State of the seL4 ecosystem Keynote at the Trusted Computing Center of Excellence 2022 Summit, February, 2022 |
|
|
|
Gernot Heiser The seL4 Foundation – growing through upheaval On-line, January, 2022 |
|
|
|
Mário Alvim, Natasha Fernandes, Annabelle McIver, Carroll Morgan and Gabriel Nunes Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata Proc. Priv. Enhancing Technol. 2022(4), pp. 378–99, 2022 |
|
|
|
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
|
|
|
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser Microarchitectural timing channels and their prevention on an open-source 64-bit RISC-V core Design, Automation and Test in Europe (DATE), virtual, February, 2021 Best Paper Award |
|
|
|
Richard S. Bird, Jeremy Gibbons, Ralf Hinze, Peter 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 |
|
|
|
Natasha Fernandes, Annabelle McIver and Carroll Morgan The Laplace mechanism has optimal utility for differential privacy over continuous queries 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021 |
|
|
|
Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell and Gabriele Keller Cogent: Uniqueness types and certifying compilation Journal of Functional Programming, Volume 31, 2021 |
|
|
|
Rob Sison and Toby Murray Verified secure compilation for mixed-sensitivity concurrent programs Journal of Functional Programming, Volume 31, pp. e18, 2021 |
2020
|
|
|
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Logical Methods in Computer Science, Volume 16, Issue 4, pp. 16:1-16:28, December, 2020 |
|
|
|
Jeremy Gibbons, Annabelle McIver, Carroll Morgan and Tom Schrijvers Quantitative information flow with monads in Haskell Foundations of Probabilistic Programming, pp. 391–448, Cambridge University Press, 2020 |
|
|
|
Alejandro 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 |
|
|
|
Gernot Heiser The formally verified seL4 microkernel – a high-assurance foundation for MCS Keynote at IEEE Conference on Embedded and Real-Time Computing and Applications, August, 2020 |
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein Towards provable timing-channel prevention ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Michael Norrish and Yiming Xu Mechanised modal model theory International Joint Conference on Automated Reasoning, pp. 518-533, Paris, July, 2020 |
|
|
|
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 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Formal reasoning under cached address translation Journal of Automated Reasoning, Volume 64, Issue 6, pp. 911-945, June, 2020 |
|
|
|
Johannes Åman Pohjola and Arve Gengelbach A mechanised semantics for HOL with ad-hoc overloading LPAR23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 498-515, Alicante, Spain, May, 2020 |
|
|
|
Gernot Heiser The seL4 microkernel – an introduction seL4 Foundation Whitepaper, May, 2020 |
|
|
|
Erik van der Kouwe, Gernot Heiser, Dennis Andriesse, Herbert Bos and Cristiano Giuffrida Benchmarking flaws undermine security research IEEE Security and Privacy, Volume 18, Issue 3, May, 2020 |
|
|
|
Rob van Glabbeek and Kees Middelburg On infinite guarded recursive specifications in process algebra Technical Report, Data61, CSIRO, May, 2020 |
|
|
|
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser Prevention of microarchitectural covert channels on an open-source 64-bit RISC-V core Workshop on Computer Architecture Research with RISC-V (CARRV), Valencia, Spain, May, 2020 |
|
|
|
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 |
|
|
|
Jack Drury, Peter Hoefner and Weiyou Wang Formal models of the OSPF routing protocol MARS2020, pp. 72–120, Dublin, Ireland, April, 2020 |
|
|
|
Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020 |
|
|
|
Gernot Heiser Verified seL4 on secure RISC-V processors at linux.conf.au, Gold Coast, January, 2020 |
|
|
|
Konrad Slind, David Hardin, Johannes Åman Pohjola and Michael Sproul Synthesis of verified architectural components for autonomy hosted on a verified microkernel Hawaii International Conference on System Sciences, pp. 6365-6374, Grand Wilea, Hawaii, January, 2020 |
|
|
|
Annabelle McIver and Carroll Morgan Correctness by construction for probabilistic programs Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles—9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I, pp. 216–239, 2020 |
2019
|
|
|
Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat Cross-chain payment protocols with success guarantees Technical Report, Data61, CSIRO, December, 2019 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Johannes Åman Pohjola, Henrik Rostedt and Magnus Myreen Characteristic formulae for liveness properties of non-terminating CakeML programs International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019 |
|
|
|
Ihor Kuz Building trustworthy systems on seL4 seL4 Summit, Herndon, VA, USA, September, 2019 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Rob van Glabbeek and Peter Hoefner Progress, justness and fairness ACM Computing Surveys, Volume 52, Issue 4, pp. 69:1–69:38, August, 2019 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser Security needs a better hardware-software contract Invited talk at Design Automation Conference (DAC), Las Vegas, NV, USA, June, 2019 |
|
|
|
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 |
|
|
|
Yanyan Shen, Gernot Heiser and Kevin Elphinstone Fault tolerance through redundant execution on COTS multicores: Exploring trade-offs International Conference on Dependable Systems and Networks (DSN), pp. 188-200, Portland, Oregon, USA, June, 2019 |
|
|
|
Erik van der Kouwe, Gernot Heiser, Dennis Andriesse, Herbert Bos and Cristiano Giuffrida SoK: benchmarking flaws in systems security European Conference on Security and Privacy (EuroS&P), Stockholm, Sweden, June, 2019 |
|
|
|
Gernot Heiser, Gerwin Klein and Toby Murray Can we prove time protection? Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019 |
|
|
|
Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Technical Report, Data61, CSIRO, April, 2019 |
|
|
|
Peter Hoefner, Rob van Glabbeek and Michael Markl A process algebra for link layer protocols European Symposium on Programming, Prague, Czech Republic, April, 2019 |
|
|
|
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 |
|
|
|
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award |
|
|
|
Gernot Heiser How to not only do great systems research, but also convince others Keynote at EuroSys Doctoral Workshop, Dresden, DE, March, 2019 |
|
|
|
Carroll Morgan, Annabelle McIver and Tahiry Rabehaja Abstract hidden markov models: A monadic account of quantitative information flow Mathematical Structures in Computer Science, Volume 15, Issue 1, pp. 36:1-36:50, March, 2019 |
|
|
|
Hing-Lun Chan and Michael Norrish Proof pearl: Bounding least common multiples with triangles Journal of Automated Reasoning, Volume 62, Issue 2, pp. 171-192, February, 2019 |
|
|
|
Gernot Heiser What's new in the world of seL4? Talk at FOSDEM'19, Brussels, February, 2019 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish The verified CakeML compiler backend Journal of Functional Programming, Volume 29, February, 2019 |
|
|
|
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith and Keith Wanbrough Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API Journal of the ACM, Volume 66, Issue 1, January, 2019 |
|
|
|
Zilin Chen, Matt Di Meglio, Liam O'Connor, Partha Susarla Ajay, Christine Rizkallah and Gabriele Keller A data layout description language for Cogent at PriSC, Lisbon, Portugal, January, 2019 |
|
|
|
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 |
|
|
|
Mário S. Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith An axiomatization of information flow measures Theoretical Computer Science, Volume 777, pp. 32-54, 2019 |
|
|
|
Annabelle McIver and Carroll Morgan Proving that programs are differentially private Programming Languages and Systems, pp. 3–18, 2019 |
|
|
|
Tahiry Rabehaja, Annabelle McIver, Carroll Morgan and Georg Struth Categorical information flow The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 329–343, Springer International Publishing, 2019 |
2018
|
|
|
Milad Ghale, Dirk Pattinson, Ramana Kumar and Michael Norrish Verified certificate checking for counting votes Verified Software: Theories, Tools and Experiments, pp. 69–87, Oxford, December, 2018 |
|
|
|
Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart A formal approach to constructing secure air vehicle software IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018 |
|
|
|
Hugo Feree, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus Myreen and Son Ho Program verification in the presence of I/O: semantics, verified library routines, and verified applications Verified Software: Theories, Tools and Experiments, pp. 88-111, Oxford, UK, November, 2018 |
|
|
|
X. Sharon Hu, Rolf Ernst, Petru Eles, Gernot Heiser, Kurt Keutzer, Daehyun Kim and Tetsuya Tohdo Roundtable: Machine learning for embedded systems IEEE Design and Test, Volume 35, Issue 6, pp. 86-93, November, 2018 |
|
|
|
Liam O'Connor, Zilin Chen, Partha Susarla Ajay, Christine Rizkallah, Gerwin Klein and Gabriele Keller Bringing effortless refinement of data layouts to Cogent International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 134-149, Limassol, Cyprus, November, 2018 |
|
|
|
Callum Bannister and Peter 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 |
|
|
|
Alejandro Gomez-Londono and Johannes Åman Pohjola Connecting choreography languages with verified stacks at Nordic Workshop on Programming Theory, Oslo, Norway, October, 2018 |
|
|
|
Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez Formally verified software in the real world Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018 |
|
|
|
Rob van Glabbeek and Peter Hoefner Progress, justness and fairness Technical Report, Data61, CSIRO, October, 2018 |
|
|
|
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 |
|
|
|
Rob van Glabbeek Is speed-independent mutual exclusion implementable? International Conference on Concurrency Theory (CONCUR), Beijing, China, September, 2018 |
|
|
|
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 |
|
|
|
Simon Biggs, Damon Lee and Gernot Heiser The jury is in: Monolithic OS design is flawed Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018 |
|
|
|
Qian Ge, Yuval Yarom and Gernot Heiser No security without time protection: we need a new hardware-software contract Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018 Best Paper Award Complete timing-channel data for evaluated x86 and Arm platforms. |
|
|
|
Callum Bannister, Peter Hoefner and Gerwin Klein Backwards and forwards with separation logic International Conference on Interactive Theorem Proving, pp. 68–87, Oxford, July, 2018 |
|
|
|
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus Myreen, Yong Kiam Tan and Michael Norrish Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions International Joint Conference on Automated Reasoning, pp. 646-662, Oxford, July, 2018 |
|
|
|
Simon Jantsch and Michael Norrish Verifying the LTL to Büchi automata translation via very weak alternating automata International Conference on Interactive Theorem Proving, pp. 306-323, Oxford, July, 2018 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Program verification in the presence of cached address translation International Conference on Interactive Theorem Proving, pp. 542-559, Oxford, UK, July, 2018 |
|
|
|
Qian Ge, Yuval Yarom, David Cock and Gernot Heiser A survey of microarchitectural timing attacks and countermeasures on contemporary hardware Journal of Cryptographic Engineering, Volume 8, Issue 1, pp. 1-27, April, 2018 |
|
|
|
Gernot Heiser The quest for the perfect API Invited "Fireside Talk" at VMware on occasion of the virtualisation pioneer's 20th anniversary, April, 2018 |
|
|
|
Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time EuroSys Conference, Porto, Portugal, April, 2018 |
|
|
|
Toby Murray, 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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser For safety's sake: we need a new hardware-software contract! IEEE Design and Test, Volume 35, Issue 2, pp. 27-30, March, 2018 |
|
|
|
Kunshan Wang, Stephen Blackburn, Tony Hosking and Michael Norrish Hop, skip, & jump: Practical on-stack replacement for a cross-platform language-neutral VM International Conference on Virtual Execution Environments, pp. 1-16, Williamsburg, VA, March, 2018 |
|
|
|
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 |
|
|
|
Rudolf Brghammer, Hitoshi Furusawa, Walter Guttmann and Peter Hoefner Relational characterisations of paths Technical Report, Data61, CSIRO, January, 2018 |
|
|
|
Gernot Heiser Flying autonomous aircraft: Mixed-criticality support in seL4 at linux.conf.au, Sydney, January, 2018 |
|
|
|
Annabelle McIver, Carroll Morgan, Benjamin Kaminski and Joost-Pieter Katoen A new proof rule for almost-sure termination ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, January, 2018 |
|
|
|
Rob Sison Per-thread compositional compilation for confidentiality-preserving concurrent programs 2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018 |
|
|
|
Solrun Halla Einarsdottir, Moa Johansson and Johannes Åman Pohjola Into the infinite - theory exploration for coinduction Artificial Intelligence and Symbolic Computation, pp. 70-86, Suzhou, China, 2018 |
2017
|
|
|
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 |
|
|
|
June Andronick From Hoare logic to Owicki-Gries and rely-guarantee for interruptible eChronos and multicore seL4 International Colloquium on Theoretical Aspects of Computing (ICTAC), pp. XIII-XV, Hanoi, Vietnam, October, 2017 |
|
|
|
Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein and Gernot Heiser The Cogent case for property-based testing Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Shanghai, China, October, 2017 |
|
|
|
Annabelle McIver, Tahiry Rabehaja, Roland Wen and Carroll Morgan Privacy in elections: How small is "small"? Journal of Information Security and Applications, Volume 36, Issue 1, pp. 112-126, October, 2017 |
|
|
|
Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson Secure mathematically-assured composition of control models Technical Report, Data61, CSIRO, September, 2017 |
|
|
|
Kevin Elphinstone, Amirreza 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 |
|
|
|
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 |
|
|
|
Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor Provably trustworthy systems Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017 |
|
|
|
Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen Verifying efficient function calls in CakeML International Conference on Functional Programming, Oxford, September, 2017 |
|
|
|
Thomas Sewell, Felix Kam and Gernot Heiser High-assurance timing analysis for a high-assurance real-time OS Real-Time Systems, Volume 53, Issue 5, pp. 812-853, September, 2017 |
|
|
|
June Andronick Reasoning about concurrency in high-assurance, high-performance software systems International Conference on Automated Deduction, pp. 1–7, Gothenburg, August, 2017 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Rob van Glabbeek Lean and full congruence formats for recursion Annual IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, August, 2017 |
|
|
|
Nicolas Bordenabe, Annabelle McIver, Carroll Morgan and Tahiry Rabehaja Reasoning about distributed secrets FORTE, pp. 156-170, Shanghai, June, 2017 |
|
|
|
Annabelle McIver, Carroll Morgan and Tahiry Rabehaja Algebra for quantitative information flow International Conference on Relational and Algebraic Methods in Computer Science, pp. 3–23, Lyon, France, May, 2017 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Reasoning about translation lookaside buffers International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 490–508, Maun, Botswana, May, 2017 |
|
|
|
Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish Verified characteristic formulae for CakeML European Symposium on Programming, pp. 584–610, Uppsala, Sweden, April, 2017 |
|
|
|
Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish Verified characteristic formulae for CakeML European Symposium on Programming, pp. 584-610, Uppsala, April, 2017 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joey Tuong COMPLX: A verification framework for concurrent imperative programs International Conference on Certified Programs and Proofs, pp. 138–150, Paris, France, January, 2017 |
|
|
|
Anthony Fox, Magnus Myreen, Yong Kiam Tan and Ramana Kumar Verified compilation of CakeML to multiple machine-code targets International Conference on Certified Programs and Proofs, pp. 125–137, Paris, France, January, 2017 |
|
|
|
Carroll Morgan A demonic lattice of information Concurrency, Security, and Puzzles — Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 203–222, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
Rob van Glabbeek An algebraic treatment of recursion Liber Amicorum for Jan Bergstra, pp. 58-59, University of Amsterdam, 2016 |
|
|
|
Yutaka Nagashima and Liam O'Connor Close encounters of the higher kind — emulating constructor classes in standard ML Abstract, ACM SIGPLAN Workshop on ML, September, 2016. |
|
|
|
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein Refinement through restraint: Bringing down the cost of verification International Conference on Functional Programming, Nara, Japan, September, 2016 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish A new verified compiler backend for CakeML International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016 |
|
|
|
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah Proof of OS scheduling behavior in the presence of interrupt-induced concurrency International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016 |
|
|
|
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein A framework for the automatic formal verification of refinement from Cogent to C International Conference on Interactive Theorem Proving, Nancy, France, August, 2016 |
|
|
|
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 |
|
|
|
Yong Kiam Tan, Scott Owens and Ramana Kumar A verified type system for CakeML Implementation and application of functional and programming languages, pp. 12, Koblenz, Germany, July, 2016 Winner: 2016 Peter Landin Prize for best paper |
|
|
|
Mario Alvim, Kostantinos Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith Axioms for information leakage Computer Security Foundations, pp. 77-92, Lisbon, June, 2016 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser and Kevin Elphinstone L4 microkernels: The lessons from 20 years of research and deployment ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016 |
|
|
|
Thomas Sewell, 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 |
|
|
|
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 |
|
|
|
Fangfei Liu, Qian Ge, Yuval Yarom, Frank Mckeen, Carlos Rozas, Gernot Heiser and Ruby B Lee CATalyst: defeating last-level cache side channel attacks in cloud computing IEEE Symposium on High-Performance Computer Architecture, pp. 406–418, Barcelona, Spain, March, 2016 |
|
|
|
Daniel Matichuk, Toby Murray and Makarius Wenzel Eisbach: A proof method language for isabelle Journal of Automated Reasoning, Volume 56, Number 3, pp. 261–282, March, 2016 |
|
|
|
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
|
|
|
Sidney Amani and Toby Murray Specifying a realistic file system Workshop on Models for Formal Analysis of Real Systems, pp. 1–9, Suva, Fiji, November, 2015 |
|
|
|
June Andronick, Corey Lewis and Carroll Morgan Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015 |
|
|
|
Peter Hoefner Using process algebra to design better protocols (abstract) Forum “Math-for-Industry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Paul Rimba, Liming Zhu, Len Bass, Ihor Kuz and Steve Reeves Composing patterns to construct secure systems European Dependable Computing Conference, pp. 213–224, Paris, France, September, 2015 |
|
|
|
Yuval Yarom, Qian Ge, Fangfei Liu, Ruby B. Lee and Gernot Heiser Mapping the Intel last-level cache The Cryptology ePrint Archive, September, 2015 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Verified over-approximation of the diameter of propositionally factored transition systems International Conference on Interactive Theorem Proving, pp. 1–16, Nanjing, China, August, 2015 |
|
|
|
Joseph Chan and Michael Norrish Mechanisation of AKS algorithm: Part 1 — the main theorem International Conference on Interactive Theorem Proving, pp. 117–136, Nanjing, China, August, 2015 |
|
|
|
Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of a component platform Technical Report, NICTA and UNSW, August, 2015 |
|
|
|
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 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Exploiting symmetries by planning for a descriptive quotient International Joint Conference on Artificial Intelligence, pp. 1479–1486, Buenos Aires, July, 2015 |
|
|
|
Jasmin Blanchette, Maximilian Haslbeck, Daniel Matichuk and Tobias Nipkow Mining the archive of formal proofs Conference on Intelligent Computer Mathematics, pp. 3–17, Washington DC, USA, July, 2015 |
|
|
|
Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach From non-preemptive to preemptive scheduling using synchronization synthesis International Conference on Computer Aided Verification, San Francisco, USA, July, 2015 |
|
|
|
Carroll Morgan, Annabelle McIver and Tahiry Rabehaja Abstract hidden Markov models: A monadic account of quantitative information flow Annual IEEE Symposium on Logic in Computer Science, pp. 597–608, Tokyo, Japan, July, 2015 |
|
|
|
Toby Murray On high-assurance information-flow-secure programming languages ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 43–48, Prague, Czech Republic, July, 2015 |
|
|
|
Sean Peters, Adrian Danis, Kevin Elphinstone and Gernot Heiser For a microkernel, a big lock is fine Asia-Pacific Workshop on Systems (APSys), Tokyo, JP, July, 2015 |
|
|
|
Peter Gammie, Tony 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 |
|
|
|
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 |
|
|
|
Carroll Morgan a nondeterministic lattice of information One-hour invited talk at Mathematics of Program Construction, Königswinter, Germany, June, 2015 |
|
|
|
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 |
|
|
|
Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser and Ruby B Lee Last-level cache side-channel attacks are practical IEEE Symposium on Security and Privacy, pp. 605–622, San Jose, CA, US, May, 2015 |
|
|
|
Michael Norrish and Michelle Mills Strout An approach for proving the correctness of inspector/executor transformations Languages and Compilers for Parallel Computing, pp. 131–145, Hillsboro, Oregon, USA, May, 2015 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser seL4: Present and future invited talk at FOSDEM'15, Brussels, BE, February, 2015 |
|
|
|
Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples Empirical study towards a leading indicator for cost of formal software verification International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015 |
|
|
|
Peter Chubb SD cards and filesystems for embedded systems linux.conf.au, Auckland, NZ, January, 2015 |
|
|
|
Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk SAT-based strategy extraction in reachability games AAAI, Austin, TX, USA, January, 2015 |
|
|
|
Gernot Heiser seL4 is free — what does this mean for you? Abstract, LCA. |
|
|
|
Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray An empirical research agenda for understanding formal methods productivity Information and Software Technology, Volume 60, pp. 102–112, January, 2015 |
|
|
|
Annabelle McIver, Larissa Meinicke and Carroll Morgan Hidden-markov program algebra with iteration Mathematical Structures in Computer Science, Volume 25, Number 2, pp. 320–360, 2015 |
2014
|
|
|
Hyungsoo Jung, Hyuck Han, Alan Fekete, Gernot Heiser and Heon Yeom A scalable lock manager for multicores ACM Transactions on Database Systems, Volume 39, Number 4, pp. 29:1–29:29, December, 2014 |
|
|
|
Anna Lyons and Gernot Heiser Mixed-criticality support in a high-assurance, general-purpose microkernel Workshop on Mixed Criticality Systems, pp. 9–14, Rome, Italy, December, 2014 |
|
|
|
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 |
|
|
|
David Cock, Qian Ge, Toby Murray and Gernot Heiser The last mile: An empirical study of some timing channels on seL4 ACM Conference on Computer and Communications Security, pp. 570–581, Scottsdale, AZ, USA, November, 2014 |
|
|
|
Matthias Daum, Nelson Billing and Gerwin Klein Concerned with the unprivileged: User programs in kernel refinement Formal Aspects of Computing, Volume 26, Number 6, pp. 1205–1229, October, 2014 |
|
|
|
Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah CDSL version 1: Simplifying verification with linear types Technical Report, NICTA, October, 2014 |
|
|
|
Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm and Mona Vij User-guided device driver synthesis USENIX Symposium on Operating Systems Design and Implementation, pp. 661–676, Broomfield, CO, USA, October, 2014 |
|
|
|
Adam Christopher Walker and Leonid Ryzhyk Predicate abstraction for reactive synthesis Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014 |
|
|
|
Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski Productivity for proof engineering Empirical Software Engineering and Measurement, pp. 15, Turin, Italy, September, 2014 |
|
|
|
Adam Christopher Walker and Leonid Ryzhyk Predicate abstraction for reactive synthesis Technical Report NRL-8281, NICTA, August, 2014 |
|
|
|
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 |
|
|
|
Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach Regression-free synthesis for concurrency International Conference on Computer Aided Verification, Vienna, Austria, July, 2014 |
|
|
|
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Real reward testing for probabilistic processes Theoretical Computer Science, Volume 538, pp. 16–36, July, 2014 |
|
|
|
Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk Interpolants in two-player games Abstract, iPRA workshop, July, 2014. |
|
|
|
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish Beagle as a HOL4 external ATP method Practical Aspects of Automated Reasoning, pp. 50–59, Vienna, July, 2014 |
|
|
|
Alexander Legg, Nina Narodytska and Leonid Ryzhyk Practical CNF interpolants via BDDs Abstract, iPRA workshop, July, 2014. |
|
|
|
Daniel Matichuk, Makarius Wenzel and Toby Murray An Isabelle proof method language International Conference on Interactive Theorem Proving, pp. 390–405, Vienna, Austria, July, 2014 |
|
|
|
Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith Additive and multiplicative notions of leakage, and their capacities Computer Security Foundations, pp. 308–322, Vienna, Austria, July, 2014 Winner of the 2015 NSA Best Scientific Cybersecurity Paper Award |
|
|
|
Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Christopher Walker Solving games without controllable predecessor International Conference on Computer Aided Verification, Vienna, Austria, July, 2014 |
|
|
|
Daniel Potts, Rene Bourquin, Leslie Andresen, June Andronick, Gerwin Klein and Gernot Heiser Mathematically verified software kernels: Raising the bar for high assurance implementations Technical Report, NICTA, July, 2014 |
|
|
|
Thomas Sewell Formal replay of translation validation for highly optimised c: Work in progress Verification and Program Transformation, Vienna, Austria, July, 2014 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Mechanising theoretical upper bounds in planning Workshop on Knowledge Engineering for Planning and Scheduling, Portsmouth, USA, June, 2014 |
|
|
|
David Greenaway, Japheth Lim, June Andronick and Gerwin Klein Don't sweat the small stuff: Formal verification of C code without the pain ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 429–439, Edinburgh, UK, June, 2014 |
|
|
|
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu Automatic verification of active device drivers ACM Operating Systems Review, Volume 48, Number 1, May, 2014 |
|
|
|
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 |
|
|
|
Gerwin Klein Proof engineering challenges for large-scale verification Abstract, AI4FM/2014 Workshop. |
|
|
|
Gerwin Klein and Tobias Nipkow Applications of interactive proof to data flow analysis and security Software Systems Safety, pp. 77–134, Volume 36 in NATO Science for Peace and Security Series , IOS Press BV, 2014 |
|
|
|
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 |
|
|
|
Bernard Blackham, Mark Liffiton and Gernot Heiser Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 169–178, Berlin, Germany, April, 2014 |
|
|
|
Aaron Carroll and Gernot Heiser Unifying DVFS and offlining in mobile multicores IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 287–296, Berlin, Germany, April, 2014 |
|
|
|
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 |
|
|
|
Gerwin Klein Proof engineering considered essential International Symposium on Formal Methods (FM), pp. 16–21, Singapore, April, 2014 |
|
|
|
Carroll Morgan, Annabelle McIver, Geoffrey Smith, Barbara Espinoza and Larisa Meinicke Abstract channels and their robust information-leakage ordering Principles of Security and Trust (ETAPS), pp. 83–102, Grenoble, France, April, 2014 |
|
|
|
Aditi Barthwal and Michael Norrish A mechanisation of some context-free language theory in HOL4 Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 2014 |
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014 |
|
|
|
Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens CakeML: A verified implementation of ML ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014 |
2013
|
|
|
Joseph Chan and Michael Norrish A string of pearls: Proofs of fermat's little theorem Journal of Formal Reasoning, Volume 6, Number 1, pp. 63–87, December, 2013 |
|
|
|
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 |
|
|
|
Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Christopher Walker and Alexander Legg Device driver synthesis Intel Technology Journal, Volume 17, Number 2, pp. 136–157, December, 2013 |
|
|
|
Aaron Carroll and Gernot Heiser Mobile multicores: Use them or waste them Workshop on Power Aware Computing and Systems, pp. 5, Farmington, PA, USA, November, 2013 A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 44-48. |
|
|
|
Kevin Elphinstone and Gernot Heiser From L3 to seL4 – what have we learnt in 20 years of L4 microkernels? ACM Symposium on Operating Systems Principles, pp. 133–150, Farmington, PA, USA, November, 2013 |
|
|
|
Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick Towards a verified component platform Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013 |
|
|
|
Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser File systems deserve verification too! Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, Pennsylvania, USA, November, 2013 A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64. |
|
|
|
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 |
|
|
|
Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell Formally verified system initialisation International Conference on Formal Engineering Methods, pp. 70–85, Queenstown, New Zealand, October, 2013 |
|
|
|
Yao Shi, Bernard Blackham and Gernot Heiser Code optimizations using formally verified properties Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 427–442, Indianapolis, USA, October, 2013 |
|
|
|
Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish Tableaux for verification of data-centric processes Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28–43, Nancy, France, September, 2013 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Aaron Carroll and Gernot Heiser The systems hacker’s guide to the Galaxy: Energy usage in a modern smartphone Asia-Pacific Workshop on Systems (APSys), pp. 7, Singapore, July, 2013 Best Student Paper Award |
|
|
|
Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach Efficient synthesis for concurrency by semantics-preserving transformations International Conference on Computer Aided Verification, pp. 1–16, Saint Petersburg, Russia, July, 2013 |
|
|
|
Gernot Heiser Can truly dependable systems be affordable? Keynote at APSys'13, Singapore, July, 2013 |
|
|
|
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 |
|
|
|
Hyungsoo Jung, Hyuck Han, Alan Fekete, Gernot Heiser and Heon Y. Yeom A scalable lock manager for multicores ACM SIGMOD Conference, pp. 73–84, New York, USA, June, 2013 Honorable Mention Award |
|
|
|
Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013 |
|
|
|
Aleksander Budzynowski and Gernot Heiser The von Neumann architecture is due for retirement Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, Santa Ana Pueblo, NM, USA, May, 2013 |
|
|
|
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 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
|
|
|
Toby Murray and Thomas Sewell Above and beyond: seL4 noninterference and binary verification Abstract, 2013 High Confidence Software and Systems Conference, Annapolis, MD, May, 2013. |
|
|
|
Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass Formal specifications better than function points for code sizing International Conference on Software Engineering, pp. 1257–1260, San Francisco, USA, May, 2013 |
|
|
|
Bernard Blackham and Gernot Heiser Sequoll: A framework for model checking binaries IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 97–106, Philadelphia, USA, April, 2013 Best Paper Award |
|
|
|
Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie and Gustavo Alonso RapiLog: reducing system complexity through verification EuroSys Conference, pp. 323–336, Prague, Czech Republic, April, 2013 |
|
|
|
Tudor-Ioan Salomie, Gustavo Alonso, Timothy Roscoe and Kevin Elphinstone Application level ballooning for efficient server consolidation EuroSys Conference, pp. 337–350, Prague, Czech Republic, April, 2013 |
|
|
|
Gernot Heiser Protecting e-government against attacks EP Workshop on Security of e-Government, pp. 5, Brussels, Belgium, February, 2013 |
|
|
|
Toby Murray On the limits of refinement-testing for model-checking CSP Formal Aspects of Computing, Volume 25, Number 2, pp. 219–256, February, 2013 |
2012
|
|
|
Daniel Matichuk and Toby Murray Extensible specifications for automatic re-use of specifications and proofs 10th International Conference on Software Engineering and Formal Methods, pp. 8, Thessaloniki, Greece, December, 2012 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein Noninterference for operating system kernels International Conference on Certified Programs and Proofs, pp. 126–142, Kyoto, Japan, December, 2012 |
|
|
|
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Automatic verification of message-based device drivers Systems Software Verification, pp. 1–14, Sydney, Australia, November, 2012 |
|
|
|
Daniel Matichuk Automatic function annotations for hoare logic Systems Software Verification, pp. 10, Sydney, Australia, November, 2012 |
|
|
|
June Andronick, Andrew Boyton and Gerwin Klein Final report for AOARD grant #FA2386-11-1-4070, formal system verification — extension Technical Report, NICTA, October, 2012 |
|
|
|
June Andronick, Gerwin Klein and Toby Murray Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105 Technical Report, NICTA, October, 2012 |
|
|
|
Hing-Lun Chan and Michael Norrish A string of pearls: Proofs of fermat’s little theorem International Conference on Certified Programs and Proofs, pp. 188–207, Kyoto, Japan, October, 2012 |
|
|
|
Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu Active device drivers Technical Report, NICTA, September, 2012 |
|
|
|
Nick Barnes, Peter Baumgartner, Tiberio Caetano, Hugh Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter Stuckey, Sylvie Thiebaux, Pascal Van Hentenryck and Toby Walsh AI @ NICTA AI Magazine, Volume 33, Number 3, pp. 115–127, September, 2012 |
|
|
|
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 |
|
|
|
June Andronick and Gerwin Klein Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022 Technical Report, NICTA, August, 2012 |
|
|
|
James Cheney, Michael Norrish and René Vestergaard Formalizing adequacy: A case study for higher-order abstract syntax Journal of Automated Reasoning, Volume 49, Number 2, pp. 209–239, August, 2012 |
|
|
|
David Greenaway, June Andronick and Gerwin Klein Bridging the gap: Automatic verified abstraction of C International Conference on Interactive Theorem Proving, pp. 99–115, Princeton, New Jersey, USA, August, 2012 |
|
|
|
Peter Hoefner Towards a representation theorem for coloring algebra Abstract, Workshop on Lattices and Relations, August, 2012. |
|
|
|
Peter Hoefner Kleene modules for routing procedures Abstract, Workshop on Lattices and Relations, August, 2012. |
|
|
|
Gerwin Klein, Rafal Kolanski and Andrew Boyton Mechanised separation algebra International Conference on Interactive Theorem Proving, pp. 332–337, Princeton, USA, August, 2012 |
|
|
|
Ihor Kuz, Liming Zhu, Len Bass, Mark Staples and Sherry Xu An architectural approach for cost effective trustworthy systems IEEE/IFIP Working Conference on Software Architecture (WICSA), pp. 325–328, Helsinki, Finland, August, 2012 |
|
|
|
Bernard Blackham and Gernot Heiser Correct, fast, maintainable — choose any three! Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012 |
|
|
|
Bernard Blackham, Vernon Tang and Gernot Heiser To preempt or not to preempt, that is the question Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012 |
|
|
|
Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski Challenges and experiences in managing large-scale proofs Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, pp. 32–48, Bremen, Germany, July, 2012 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski Simulation modeling of a large scale formal verification process International Conference on Software and Systems Process, pp. 3–12, Zurich, Switzerland, June, 2012 |
|
|
|
June Andronick, Gerwin Klein and Andrew Boyton Formal system verification — extension, AOARD 114070 Technical Report, NICTA, May, 2012 |
|
|
|
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 |
|
|
|
Bernard Blackham, Yao Shi and Gernot Heiser Improving interrupt response time in a verifiable protected microkernel EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012 |
|
|
|
Matthew Fernandez, Gerwin Klein and Ihor Kuz Microkernel verification down to assembly Poster presented at EuroSys 2012, April, 2012 |
|
|
|
Gerwin Klein Interactive proof: Applications to semantics Software Safety and Security: Tools for Analysis and Verification, pp. 85–125, IOS Press, 2012 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein It's time for trustworthy systems IEEE Symposium on Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012 |
|
|
|
Peter Chubb Bourne shell tutorial Tutorial at Linux.conf.au, Ballarat, January, 2012 |
|
|
|
Peter Chubb Linux as a boot loader Talk at linux.conf.au, Ballarat, January, 2012 |
|
|
|
Stefan M. Petters, Kevin Elphinstone and Gernot Heiser Trustworthy real-time systems Advances in Real-Time Systems, pp. 191–206, Springer, 2012 |
2011
|
|
|
June Andronick, Gerwin Klein and Toby Murray Formal system verification for trustworthy embedded systems, final report option 1 — AOARD 104105 Technical Report, NICTA, November, 2011 |
|
|
|
Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser Timing analysis of a protected operating system kernel IEEE Real-Time Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Michael Norrish Mechanised computability theory International Conference on Interactive Theorem Proving, pp. 297—311, Nijmegen, The Netherlands, August, 2011 |
|
|
|
Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein seL4 enforces integrity International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011 |
|
|
|
Sidney Amani, Leonid Ryzhyk, Alastair Donaldson, Gernot Heiser, Alexander Legg and Yanjin Zhu Static analysis of device drivers: we can do better! Asia-Pacific Workshop on Systems (APSys), pp. 1–5, Shanghai, China, July, 2011 |
|
|
|
Bernard Blackham, Yao Shi and Gernot Heiser Protected hard real-time: The next frontier Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011 |
|
|
|
Yuxin Deng, 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 |
|
|
|
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 |
|
|
|
Prashant Varanasi and Gernot Heiser Hardware-supported virtualization on ARM Asia-Pacific Workshop on Systems (APSys), pp. 5 pages, Shanghai, China, July, 2011 |
|
|
|
Han-Hing Dang, Bernhard Möller and Peter Hoefner Algebraic separation logic The Journal of Logic and Algebraic Programming, Volume 80, Number 6, pp. 221–247, June, 2011 |
|
|
|
Gernot Heiser Virtualizing embedded systems — why bother? Design Automation Conference (DAC), pp. 901–905, Dan Diego, CA, USA, June, 2011 |
|
|
|
Peter Hoefner and Bernhard Möller Fixing zeno gaps Theoretical Computer Science, Volume 412, Number 28, pp. 3303–3322, June, 2011 |
|
|
|
Etienne Le Sueur and Gernot Heiser Slow down or sleep, that is the question USENIX Technical Conference, Portland, Oregon, USA, June, 2011 |
|
|
|
Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski What if you could actually Trust your kernel? Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011 |
|
|
|
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 |
|
|
|
Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood Provable security: How feasible is it? Workshop on Hot Topics in Operating Systems (HotOS), pp. 5, Napa, USA, May, 2011 |
|
|
|
Ihor Kuz, Zachary Anderson, Pravin Shinde and Timothy Roscoe Multicore OS benchmarks: we can do better Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011 |
|
|
|
June Andronick and Gerwin Klein Formal system verification for trustworthy embedded systems, final report AOARD 094160 Technical Report, NICTA, April, 2011 |
|
|
|
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved device driver reliability through hardware verification reuse International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 1–12, Newport Beach, CA, USA, March, 2011 |
2010
|
|
|
June Andronick From a proven correct microkernel to trustworthy large systems International Conference on Formal Verification of Object-Oriented Software, pp. 1–9, Paris, December, 2010 |
|
|
|
Gerwin Klein From a verified kernel towards verified systems Asian Symposium on Programming Languages and Systems (APLAS), pp. 21–33, Shanghai, China, November, 2010 Invited extended abstract. |
|
|
|
June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Systems Software Verification, pp. 9, Vancouver, CA, October, 2010 |
|
|
|
Yuxin Deng and 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 |
|
|
|
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The road to trustworthy systems ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3–10, Chicago, IL, USA, October, 2010 |
|
|
|
Etienne Le Sueur and Gernot Heiser Dynamic voltage and frequency scaling: The laws of diminishing returns Workshop on Power Aware Computing and Systems, pp. 1–5, Vancouver, Canada, October, 2010 |
|
|
|
Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser Improved device driver reliability through verification reuse Workshop on Hot Topics in System Dependability, pp. 1–6, Vancouver, Canada, October, 2010 |
|
|
|
Aditi Barthwal and Michael Norrish A formalisation of the normal forms of context-free grammars in HOL4 19th EACSL Annual Conferences on Computer Science Logic, pp. 95–109, Brno, Czech Republic, August, 2010 |
|
|
|
Nicholas Fitzroy-Dale, Ihor Kuz and Gernot Heiser Architecture optimisation with Currawong Asia-Pacific Workshop on Systems (APSys), pp. 7–12, New Delhi, India, August, 2010 |
|
|
|
Gernot Heiser and Ben Leslie The OKL4 microvisor: Convergence point of microkernels and hypervisors Asia-Pacific Workshop on Systems (APSys), pp. 19–24, New Delhi, India, August, 2010 |
|
|
|
Gerwin Klein The l4.verified project – next steps Verified Software: Theories, Tools and Experiments, pp. 86–96, Edinburgh, UK, August, 2010 |
|
|
|
Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker capDL: A language for describing capability-based systems Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010 |
|
|
|
Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser The case for active device drivers Asia-Pacific Workshop on Systems (APSys), pp. 25–30, New Delhi, India, August, 2010 |
|
|
|
Aditi Barthwal and Michael Norrish Mechanisation of PDA and grammar equivalence for context-free languages 17th Workshop on Logic, Language, Information and Computation , pp. 125–135, Brasília, Brazil, July, 2010 |
|
|
|
Gerwin Klein A formally verified OS kernel. now what? International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010 |
|
|
|
Ramana Kumar and Michael Norrish (nominal) unification by recursive descent with triangular substitutions International Conference on Interactive Theorem Proving, pp. 51–66, Edinburgh, United Kingdom, July, 2010 |
|
|
|
Aaron Carroll and Gernot Heiser An analysis of power consumption in a smartphone USENIX Annual Technical Conference, pp. 271–284, Boston, MA, US, June, 2010 |
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an operating-system kernel Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010 Research Highlights paper |
|
|
|
Gerwin Klein, Thomas Sewell and Simon Winwood Refinement in the formal verification of seL4 Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323–339, Springer, 2010 |
|
|
|
Peter Chubb Decent MIDI from LilyPond Linux.conf.au, January, 2010 |
|
|
|
Peter Chubb and John Judge When the arduino meets year 9 Other Conference Presentation, linux.conf.au, Wellington, New Zealand, January, 2010. |
|
|
|
Peter Chubb and Yang Song Interrupts considered harmful Other Conference Presentation, Linux.conf.au, Wellington, NZ, January, 2010. |
2009
|
|
|
Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009 |
|
|
|
Andrew Boyton A verified shared capability model Systems Software Verification, pp. 25–44, Aachen, Germany, October, 2009 |
|
|
|
Ralf Huuck, Gerwin Klein and Schlich Bastian Proc. 4th international workshop on system software verification (SSV09) Electronic Notes in Theoretical Computer Science, Volume 254, pp. 1–3, October, 2009 |
|
|
|
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award |
|
|
|
Michael Norrish Rewriting conversions implemented with continuations Journal of Automated Reasoning, Volume 43, Number 3, pp. 305–336, October, 2009 |
|
|
|
Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic device driver synthesis with Termite ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009 |
|
|
|
Yuxin Deng, 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 |
|
|
|
Rafal Kolanski and Gerwin Klein Types, maps and separation logic International Conference on Theorem Proving in Higher Order Logics, pp. 276–292, Munich, Germany, August, 2009 |
|
|
|
Stefan M. Petters, Martin Lawitzky, Ryan Heffernan and Kevin Elphinstone Towards real multi-criticality scheduling IEEE Conference on Embedded and Real-Time Computing and Applications, pp. 155–164, Beijing, China, August, 2009 |
|
|
|
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish Mind the gap: A verification framework for low-level C International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, August, 2009 |
|
|
|
Matthew Chapman and Gernot Heiser vNUMA: A virtual shared-memory multiprocessor USENIX Annual Technical Conference, pp. 349–362, San Diego, USA, June, 2009 |
|
|
|
Gerwin Klein, Ralf Huuck and Bastian Schlich Operating system verification Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009 |
|
|
|
Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser Dingo: Taming device drivers EuroSys Conference, pp. 275–288, Nuremberg, DE, April, 2009 |
|
|
|
Dave Snowdon, Etienne Le Sueur, Stefan M. Petters and Gernot Heiser Koala: A platform for OS-level power management EuroSys Conference, pp. 289–302, Nuremberg, DE, April, 2009 |
|
|
|
Aditi Barthwal and Michael Norrish Verified, executable parsing European Symposium on Programming, pp. 160–174, York, March, 2009 |
|
|
|
James Cheney, René Vestergaard and Michael Norrish Formalizing adequacy 2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming, York, March, 2009 |
|
|
|
Nicholas Fitzroy-Dale and Ihor Kuz Towards automatic optimisation of componentised systems Workshop on Isolation and Integration in Embedded Systems, pp. 6, Nuremberg, Germany, March, 2009 |
|
|
|
Gernot Heiser Many-core chips — a case for virtual shared memory Workshop on Managed Many-Core Systems, pp. 4 pages, Washington, DC, USA, March, 2009 |
|
|
|
Gerwin Klein Operating system verification — an overview Sadhana, Volume 34, Number 1, pp. 26–69, February, 2009 Invited paper. Journal homepage. |
|
|
|
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 |
|
|
|
Gernot Heiser Hypervisors for consumer electronics IEEE Consumer Communications and Networking Conference, pp. 1–5, Las Vegas, NV, USA, January, 2009 |
2008
|
|
|
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 |
|
|
|
André Hergenhan and Gernot Heiser Operating systems technology for converged ECUs Embedded Security in Cars Conference (escar), pp. 3 pages, Hamburg, Germany, November, 2008 |
|
|
|
Stefan M. Petters, Martin Lawitzky, Kevin Elphinstone and Ryan Heffernan Fitting an EDF based scheduling approach to componentised real(-time) systems IEEE Real-Time Systems Symposium, Barcelona, Spain, November, 2008 |
|
|
|
Yuxin Deng, 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 |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Verified Software: Theories, Tools and Experiments, pp. 99–115, Toronto, Canada , October, 2008 |
|
|
|
Rafal Kolanski and Gerwin Klein Mapped separation logic Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008 |
|
|
|
5th international verification workshop — VERIFY'08 CEUR Workshop Proceedings, 2008 |
|
|
|
David Cock Bitfields and tagged unions in C — verification through automatic generation International Verification Workshop, pp. 44–55, Sydney, August, 2008 |
|
|
|
David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement International Conference on Theorem Proving in Higher Order Logics, pp. 167–182, Montreal, Canada, August, 2008 |
|
|
|
Joshua LeVasseur, Volkmar Uhlig, Yaowei Yang, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser Pre-virtualization: Soft layering for virtual machines Asia-Pacific Computer Systems Architecture Conference, pp. 1–9, Hsinchu, Taiwan, August, 2008 Best Paper Award |
|
|
|
Konrad Slind and Michael Norrish A brief overview of HOL4 International Conference on Theorem Proving in Higher Order Logics, pp. 28–32, Montréal, Canada, August, 2008 |
|
|
|
Proceedings of the 3rd international workshop on systems software verification (SSV 2008) Volume 217 in ENTCS, Elsevier, 2008 |
|
|
|
Rafal Kolanski A logic for virtual memory Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008 |
|
|
|
Gernot Heiser Trusted ⇐ trustworthy ⇐ proof – Position paper Conference on Future of Trust in Computing, pp. 55–59, Berlin, DE, May, 2008 |
|
|
|
Tom Ridge, Michael Norrish and Peter Sewell A rigorous approach to networking: TCP, from implementation to protocol to service International Symposium on Formal Methods (FM), pp. 294—309, Turku, Finland, May, 2008 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel design for isolation and assurance of physical memory Workshop on Isolation and Integration in Embedded Systems, pp. 35–40, Glasgow, UK, April, 2008 |
|
|
|
Gernot Heiser The role of virtualization in embedded systems Workshop on Isolation and Integration in Embedded Systems, pp. 11–16, Glasgow, UK, April, 2008 |
|
|
|
Gernot Heiser Do microkernels suck? Other Conference Presentation, Linux.conf.au, Melbourne, Australia, January, 2008. |
|
|
|
Ihor Kuz and 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
|
|
|
Kevin Elphinstone, David Greenaway and Sergio Ruocco Lazy queueing and direct process switch — merit or myths? Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 69–77, Pisa, Italy, December, 2007 |
|
|
|
Gernot Heiser Your system is secure? Prove it! USENIX ;login:, Volume 32(6), pp. 35—38, December, 2007 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: Taking microkernels to the next level ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007 |
|
|
|
Stefan M. Petters, Patryk Zadarnowski and Gernot Heiser Measurements or static analysis or both? Workshop on Worst-Case Execution-Time Analysis, pp. 5–11, Pisa, Italy, December, 2007 |
|
|
|
Dave Snowdon, Godfrey van der Linden, Stefan M. Petters and Gernot Heiser Accurate run-time prediction of performance degradation under frequency scaling Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 58–64, Pisa, Italy, December, 2007 |
|
|
|
Dave Snowdon, Stefan M. Petters and Gernot Heiser Accurate on-line prediction of processor and memory energy usage under voltage scaling International Conference on Embedded Software, pp. 84–93, Salzburg, Austria, December, 2007 |
|
|
|
Michael Norrish A formal semantics for c++ Technical Report, NICTA, November, 2007 |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007 |
|
|
|
Leonid Ryzhyk, Ihor Kuz and Gernot Heiser Formalising device driver interfaces Workshop on Programming Languages and Operating Systems (PLOS), pp. 5, Stevenson, WA, USA, October, 2007 |
|
|
|
Michael Norrish and René Vestergaard Proof pearl: de bruijn terms really do work International Conference on Theorem Proving in Higher Order Logics, pp. 207–222, Kaiserslautern, September, 2007 |
|
|
|
Yuxin Deng, 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 |
|
|
|
Jia Meng, Lawrence C. Paulson and Gerwin Klein A termination checker for isabelle hoare logic International Verification Workshop, pp. 104–118, Bremen, Germany, July, 2007 |
|
|
|
Leonid Ryzhyk, Timothy Bourke and Ihor Kuz Reliable device drivers require well-defined protocols Workshop on Hot Topics in System Dependability, pp. Article 3, Edinburgh, UK, June, 2007 |
|
|
|
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, San Diego, CA, USA, May, 2007 |
|
|
|
Timothy Roscoe, Kevin Elphinstone and Gernot Heiser Hype and virtue Workshop on Hot Topics in Operating Systems (HotOS), pp. 19–24, San Diego, USA, May, 2007 |
|
|
|
Yuxin Deng, 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 |
|
|
|
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 |
|
|
|
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
|
|
|
Kevin Elphinstone and Scott Brandt Proceedings of the 2007 workshop on operating system platforms for embedded real-time applications Technical Report, NICTA, July, 2006 |
|
|
|
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55—66, Charleston, South Carolina, USA, January, 2006 |
2005
|
|
|
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
|
|
|
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
|
|
|
Michael Norrish Complete integer decision procedures as derived rules in HOL International Conference on Theorem Proving in Higher Order Logics, pp. 71–86, Rome, September, 2003 |
|
|
|
Adam Wiggins A survey on the interaction between caching, translation and protection Technical Report UNSW-CSE-TR-0321, School of Computer Science and Engineering, August, 2003 |
2002
|
|
|
Shane Stephens and Gernot Heiser Fault tolerance and avoidance in biomedical systems SIGOPS European Workshop, St Emilion, France, September, 2002 |
|
|
|
Daniel Potts, Simon Winwood and Gernot Heiser Design and implementation of the L4 microkernel for Alpha multiprocessors Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002 |
|
|
|
Kingsley Cheung and Gernot Heiser A resource management framework for priority-based physical-memory allocation Asia-Pacific Computer Systems Architecture Conference, Monash University, Melbourne, Australia, January, 2002 |
|
|
|
Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser Performance of address-space multiplexing on the Pentium Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002 |
2001
|
|
|
Gernot Heiser Dealing with TLB tags International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001 |
|
|
|
Antony Edwards and Gernot Heiser Secure OS extensibility needn't cost an arm and a leg Workshop on Hot Topics in Operating Systems (HotOS), pp. 168, Schloss Elmau, DE, May, 2001 |
|
|
|
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 |
|
|
|
Alan Au and Gernot Heiser Enhancing IA64 memory management Linux.conf.au, Sydney, Australia, January, 2001 |
|
|
|
Antony Edwards and Gernot Heiser Components + Security = OS Extensibility Asia-Pacific Computer Systems Architecture Conference, pp. 27–34, Gold Coast, Australia, January, 2001 |
|
|
|
Gernot Heiser Inside L4/MIPS: Anatomy of a high-performance microkernel Sydney, Australia, January, 2001 |
2000
|
|
|
Adam Wiggins and Gernot Heiser Fast address-space switching on the StrongARM SA-1100 processor Australasian Computer Architecture Conference, pp. 97–104, Canberra, Australia, January, 2000 |
1999
|
|
|
Luke Deller and Gernot Heiser Linking programs in a single address space USENIX, pp. 283–294, Monterey, Ca, USA, June, 1999 |
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual: MIPS R4x00, version 1.11, kernel version 79 Sydney, Australia, May, 1999 |
|
|
|
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
|
|
|
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 |
|
|
|
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
|
|
|
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
|
|
|
Jerry Vochteloo, Kevin Elphinstone, Stephen Russell and Gernot Heiser Protection domain extensions in Mungi IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 161–165, Seattle, WA, USA, October, 1996 |
|
|
|
Jinsong Ouyang and Gernot Heiser Libra: A library for reliable distributed applications International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 801–810, Sunnyvale, CA, USA, August, 1996 |
|
|
|
Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke Supporting persistent object systems in a single address space International Workshop on Persistent Object Systems (POS), pp. 111–119, Cape May, NJ, USA, May, 1996 |
1995
|
|
|
Tim Wilkinson, Kevin Murray, Stephen Russell, Gernot Heiser and Jochen Liedtke Single address space operating systems Technical Report UNSW-CSE-TR-9504, UNSW, November, 1995 |
|
|
|
Jinsong Ouyang and Gernot Heiser Checkpointing and recovery for distributed shared memory applications IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 191–9, Lund, SE, August, 1995 |
1994
|
|
|
Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo Mungi: A distributed single-address-space operating system Australasian Computer Science Conference (ACSC), pp. 271–80, Christchurch, New Zealand, January, 1994 |
1993
|
|
|
Jerry Vochteloo, Stephen Russell and Gernot Heiser Capability-based protection in the Mungi operating system IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 108–15, Asheville, NC, USA, December, 1993 |
1992
|
|
|
Stephen Russell, Alan Skea, Kevin Elphinstone, Gernot Heiser, Keith Burston, Ian Gorton and Graham Hellestrand Distribution + persistence = global virtual memory IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 96–99, Dourdan, France, September, 1992 |
Other technical reports of the School of Computer Science & Engineering.
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
|
|
|
Joshua LeVasseur Device-driver reuse via virtual machines PhD Thesis, UNSW, Sydney, Australia, May, 2009 |
2008
|
|
|
Ian Wienand Transparent large-page support for Itanium Linux ME Thesis, UNSW, Sydney, Australia, July, 2008 |
|
|
|
Daniel Potts Eidolon: Adapting distributed applications to their environment PhD Thesis, UNSW, Sydney, Australia, January, 2008 |
2006
|
|
|
Myrto Zehnder and Peter Chubb Virtualising PCI Gelato ICE, Singapore, October, 2006 |
|
|
|
Shehjar Tikoo and Peter Chubb Improving NFS performance Gelato ICE conference, San Jose, CA, April, 2006 |
2005
|
|
|
Peter Chubb Bugs: getting them stomped! Gelato ICE, Brazil, October, 2005 |
|
|
|
Peter Chubb Which filesystem? Gelato ICE, Brazil, October, 2005 |
|
|
|
Peter Chubb and Darren Williams Linux scalability — from the micro to the HUGE Linux.conf.au, Canberra, ACT, April, 2005 |
2004
|
|
|
Peter Chubb Get more device drivers out of the kernel! Ottawa Linux Symposium, Ottawa, Canada, July, 2004 |
|
|
|
Peter Chubb Linux kernel infrastructure for user-level device drivers Linux.conf.au, Adelaide, Australia, January, 2004 |
2003
|
|
|
Peter Chubb Where's all the time going? Microstate accounting in Linux 2.5 Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Australia, September, 2003 |
|
|
|
Andreas Haeberlen and Kevin Elphinstone User-level management of kernel memory Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003 |
|
|
|
Adam Wiggins A survey on the interaction between caching, translation and protection Technical Report UNSW-CSE-TR-0321, School of Computer Science and Engineering, August, 2003 |
2002
|
|
|
Peter Chubb Terabytes on a diet Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Australia, September, 2002 |
|
|
|
Shane Stephens and Gernot Heiser Fault tolerance and avoidance in biomedical systems SIGOPS European Workshop, St Emilion, France, September, 2002 |
|
|
|
Peter Chubb YOU ARE LOST in a maze of BitKeeper repositories — all almost the same Australian Open Source Symposium, Sydney, Australia, July, 2002 |
|
|
|
Simon Winwood, Yefim Shuf and Hubertus Franke Multiple page size support in the Linux kernel Ottawa Linux Symposium, Ottawa, Canada, June, 2002 |
|
|
|
Daniel Potts, Simon Winwood and Gernot Heiser Design and implementation of the L4 microkernel for Alpha multiprocessors Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002 |
|
|
|
Kingsley Cheung and Gernot Heiser A resource management framework for priority-based physical-memory allocation Asia-Pacific Computer Systems Architecture Conference, Monash University, Melbourne, Australia, January, 2002 |
|
|
|
Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser Performance of address-space multiplexing on the Pentium Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002 |
2001
|
|
|
Gernot Heiser Dealing with TLB tags International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001 |
|
|
|
Chris Szmajda Calypso: A portable translation layer International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001 |
|
|
|
Antony Edwards and Gernot Heiser Secure OS extensibility needn't cost an arm and a leg Workshop on Hot Topics in Operating Systems (HotOS), pp. 168, Schloss Elmau, DE, May, 2001 |
|
|
|
Antony Edwards and Gernot Heiser A component architecture for system extensibility Technical Report UNSW-CSE-TR-0103, School of Computer Science and Engineering, March, 2001 |
|
|
|
Daniel Potts, Simon Winwood and Gernot Heiser L4 reference manual: Alpha 21x64 Technical Report UNSW-CSE-TR-0104, School of Computer Science and Engineering, March, 2001 |
|
|
|
Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller The SawMill framework for VM diversity Asia-Pacific Computer Systems Architecture Conference, pp. 3–10, Gold Coast, Australia, January, 2001 |
|
|
|
Alan Au and Gernot Heiser Enhancing IA64 memory management Linux.conf.au, Sydney, Australia, January, 2001 |
|
|
|
Antony Edwards and Gernot Heiser Components + Security = OS Extensibility Asia-Pacific Computer Systems Architecture Conference, pp. 27–34, Gold Coast, Australia, January, 2001 |
|
|
|
Gernot Heiser Inside L4/MIPS: Anatomy of a high-performance microkernel Sydney, Australia, January, 2001 |
2000
|
|
|
Adam Wiggins and Gernot Heiser Fast address-space switching on the StrongARM SA-1100 processor Australasian Computer Architecture Conference, pp. 97–104, Canberra, Australia, January, 2000 |
|
|
|
Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther The Sawmill multiserver approach SIGOPS European Workshop, pp. 109–114, Kolding, Denmark, 2000 |
1999
|
|
|
Luke Deller and Gernot Heiser Linking programs in a single address space USENIX, pp. 283–294, Monterey, Ca, USA, June, 1999 |
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual: MIPS R4x00, version 1.11, kernel version 79 Sydney, Australia, May, 1999 |
|
|
|
Kevin Elphinstone Virtual memory in a 64-bit microkernel PhD Thesis, UNSW, Sydney, Australia, March, 1999 |
|
|
|
Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko and Yoonho Park Flexible access control using IPC redirection Workshop on Hot Topics in Operating Systems (HotOS), pp. 191–196, Rio Rico, AZ, USA, March, 1999 |
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Australasian Computer Architecture Conference, pp. 211-226, Auckland, New Zealand, January, 1999 |
1998
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Technical Report UNSW-CSE-TR-9804, School of Computer Science and Engineering, August, 1998 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke The Mungi single-address-space operating system Software: Practice and Experience, Volume 28, Number 9, pp. 901–928, July, 1998 |
|
|
|
Jerry Vochteloo Design, implementation and performance of protection in the Mungi single-address-space operating system PhD Thesis, UNSW, Sydney, Australia, July, 1998 |
|
|
|
Alan Au and Gernot Heiser L4 User Manual — version 1.0 Technical Report UNSW-CSE-TR-9801, School of Computer Science and Engineering, April, 1998 |
|
|
|
Gernot Heiser, Fondy Lam and Stephen Russell Resource management in the Mungi single-address-space operating system Australasian Computer Science Conference (ACSC), pp. 417–428, Perth, Australia, February, 1998 |
1997
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual – MIPS R4x00 — Version 1.0 Technical Report UNSW-CSE-TR-9709, School of Computer Science and Engineering, December, 1997 |
|
|
|
Gernot Heiser, Fondy Lam and Stephen Russell Resource management in the Mungi single-address-space operating system Technical Report UNSW-CSE-TR-9705, UNSW, August, 1997 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke Implementation and performance of the Mungi single-address-space operating system Technical Report UNSW-CSE-TR-9704, UNSW, June, 1997 |
|
|
|
Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam and Trent Jaeger Achieved IPC performance (still the foundation for extensibility) Workshop on Hot Topics in Operating Systems (HotOS), pp. 28–31, Cape Cod, MA, USA, May, 1997 |
|
|
|
Gernot Heiser, Jerry Vochteloo, Kevin Elphinstone and Stephen Russell The Mungi kernel API/Release 1.0 Technical Report UNSW-CSE-TR-9701, School of Computer Science and Engineering, March, 1997 |
1996
|
|
|
Jerry Vochteloo, Kevin Elphinstone, Stephen Russell and Gernot Heiser Protection domain extensions in Mungi IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 161–165, Seattle, WA, USA, October, 1996 |
|
|
|
Jinsong Ouyang and Gernot Heiser Libra: A library for reliable distributed applications International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 801–810, Sunnyvale, CA, USA, August, 1996 |
|
|
|
Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke Supporting persistent object systems in a single address space International Workshop on Persistent Object Systems (POS), pp. 111–119, Cape May, NJ, USA, May, 1996 |
|
|
|
Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization ACM Operating Systems Review, Volume 30, Number 1, pp. 4–15, January, 1996 |
1995
|
|
|
Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, November, 1995 |
|
|
|
Tim Wilkinson, Kevin Murray, Stephen Russell, Gernot Heiser and Jochen Liedtke Single address space operating systems Technical Report UNSW-CSE-TR-9504, UNSW, November, 1995 |
|
|
|
Jinsong Ouyang and Gernot Heiser Checkpointing and recovery for distributed shared memory applications IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 191–9, Lund, SE, August, 1995 |
1994
|
|
|
Kevin Elphinstone, Stephen Russell and Gernot Heiser Issues in implementing virtual memory Technical Report UNSW-CSE-TR-9411, School of Computer Science and Engineering, September, 1994 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo Mungi: A distributed single-address-space operating system Australasian Computer Science Conference (ACSC), pp. 271–80, Christchurch, New Zealand, January, 1994 |
1993
|
|
|
Jerry Vochteloo, Stephen Russell and Gernot Heiser Capability-based protection in the Mungi operating system IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 108–15, Asheville, NC, USA, December, 1993 |
|
|
|
Kevin Elphinstone Address space management issues in the Mungi operating system Technical Report UNSW-CSE-TR-9312, School of Computer Science and Engineering, November, 1993 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo Mungi: A distributed single address-space operating system Technical Report UNSW-CSE-TR-9314, School of Computer Science and Engineering, November, 1993 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Stephen Russell and Graham R. Hellestrand A distributed single address space system supporting persistence Technical Report UNSW-CSE-TR-9302, UNSW, March, 1993 |
1992
|
|
|
Stephen Russell, Alan Skea, Kevin Elphinstone, Gernot Heiser, Keith Burston, Ian Gorton and Graham Hellestrand Distribution + persistence = global virtual memory IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 96–99, Dourdan, France, September, 1992 |
Post-graduate Student Theses
2023
|
|
|
Zilin Chen Towards a practical high-assurance systems programming language PhD Thesis, UNSW, Sydney, Australia, March, 2023 |
2020
|
|
|
Rob Sison Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs PhD Thesis, UNSW, Sydney, Australia, October, 2020 |
2019
|
|
|
Qian Ge Principled elimination of microarchitectural timing channels through operating-system enforced time protection PhD Thesis, UNSW, Sydney, Australia, October, 2019 |
|
|
|
Liam O'Connor Type systems for systems types PhD Thesis, UNSW, Sydney, Australia, August, 2019 |
|
|
|
Hira Taqdees Syeda Low-level program verification under cached address translation PhD Thesis, UNSW, Sydney, Australia, August, 2019 |
|
|
|
Yanyan Shen Microkernel mechanisms for improving the trustworthiness of commodity hardware PhD Thesis, UNSW, Sydney, Australia, March, 2019 |
2018
|
|
|
Anna Lyons Mixed-criticality scheduling and resource sharing for high-assurance operating systems PhD Thesis, UNSW, August, 2018 |
|
|
|
Daniel Matichuk Automation for proof engineering: Machine-checked proofs at scale PhD Thesis, UNSW, Sydney, Australia, July, 2018 |
|
|
|
Mohammad Abdulaziz Formally verified compositional algorithms for factored transition systems PhD Thesis, Australian National University, June, 2018 |
2017
|
|
|
Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, July, 2017 |
|
|
|
Aaron Carroll Understanding and reducing smartphone energy consumption PhD Thesis, UNSW, Sydney, Australia, May, 2017 |
2016
|
|
|
Alexander Legg A counterexample guided method for reactive synthesis PhD Thesis, UNSW, Sydney,Australia, September, 2016 |
|
|
|
Sidney Amani A methodology for trustworthy file systems PhD Thesis, CSE, UNSW, Sydney, Australia, August, 2016 |
|
|
|
Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016 |
2015
|
|
|
David Greenaway Automated proof-producing abstraction of c code PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015 |
2014
|
|
|
Andrew Boyton Secure architectures on a verified microkernel PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014 |
|
|
|
David Cock Leakage in trustworthy systems PhD Thesis, UNSW, Sydney, Australia, August, 2014 |
2013
|
|
|
Michael von Tessin The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2013 |
|
|
|
Bernard Blackham Towards verified microkernels for real-time mixed-criticality systems PhD Thesis, UNSW, Sydney, Australia, October, 2013 2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation |
2011
|
|
|
Rafal Kolanski Verification of programs in virtual memory using separation logic PhD Thesis, UNSW, Sydney, Australia, July, 2011 |
|
|
|
Etienne Le Sueur An analysis of the effectiveness of energy management on modern computer processors MSc Thesis, UNSW, Sydney, Australia, June, 2011 |
|
|
|
Nicholas FitzRoy-Dale Architecture optimisation PhD Thesis, UNSW, Sydney, Australia, March, 2011 |
2010
|
|
|
Dhammika Elkaduwe A principled approach to kernel memory management PhD Thesis, UNSW, Sydney, Australia, May, 2010 |
|
|
|
Dave Snowdon OS-level power management PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, March, 2010 |
|
|
|
Leonid Ryzhyk On the construction of reliable device drivers PhD Thesis, UNSW, Sydney, Australia, January, 2010 |
2009
|
|
|
Joshua LeVasseur Device-driver reuse via virtual machines PhD Thesis, UNSW, Sydney, Australia, May, 2009 |
|
|
|
Matthew Chapman vNUMA: Virtual shared-memory multiprocessors PhD Thesis, UNSW, Sydney, Australia, March, 2009 |
2008
|
|
|
Harvey Tuch Formal memory models for verifying C systems code PhD Thesis, UNSW, Sydney, Australia, August, 2008 |
|
|
|
Ian Wienand Transparent large-page support for Itanium Linux ME Thesis, UNSW, Sydney, Australia, July, 2008 |
|
|
|
Daniel Potts Eidolon: Adapting distributed applications to their environment PhD Thesis, UNSW, Sydney, Australia, January, 2008 |
2007
|
|
|
Luke Macpherson Performing under overload PhD Thesis, UNSW, Sydney, Australia, September, 2007 |
|
|
|
Andrew Baumann Dynamic update for operating systems PhD Thesis, UNSW, Sydney, Australia, August, 2007 |
2005
|
|
 |
Volkmar Uhlig Scalability of microkernel-based systems PhD Thesis, University of Karlsruhe, Karlsruhe, DE, June, 2005 |
1999
|
|
|
Kevin Elphinstone Virtual memory in a 64-bit microkernel PhD Thesis, UNSW, Sydney, Australia, March, 1999 |
1998
|
|
|
Jerry Vochteloo Design, implementation and performance of protection in the Mungi single-address-space operating system PhD Thesis, UNSW, Sydney, Australia, July, 1998 |
Selected Undergraduate Student Theses
Below are a selection of honours theses done with the group.
2023
|
|
|
Lucy Parker High-performance networking on seL4 BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2023 |
2022
|
|
|
Mitchell Johnston Strengthening scheduling guarantees of seL4 MCS with IPC budget limits BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2022 |
2018
|
|
|
Sebastian Holzapfel User-level mixed criticality systems scheduling on multicore processors BE Thesis, School of Electrical Engineering and Telecommunication, Sydney, Australia, November, 2018 |
|
|
|
Jack Suann Zircon on seL4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, May, 2018 |
2017
|
|
|
A. Felizzi Trianqles: Porting qubes to seL4 BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2017 |
2016
|
|
|
Kent McLeod Usermode OS components on seL4 with rump kernels BE Thesis, School of Electrical Engineering and Telecommunication, Sydney, Australia, October, 2016 |
2011
|
|
|
Alexandra Boulgakov Sunswift IV strategy for the 2011 World Solar Challenge BE Thesis, School of Electrical Engineering, Sydney, Australia, November, 2011 |
|
|
|
Aleksander Budzynowski Operating system for a flow-graph machine BE Thesis, School of Mechanical and Manufacturing Engineering, Sydney, Australia, October, 2011 |
|
|
|
Anna Lyons Efficient concurrency control for high-performance microkernels BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, July, 2011 |
2010
|
|
|
Prashant Varanasi Implementing hardware-supported virtualization in OKL4 on ARM BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2010 |
|
|
|
Josh Matthews Native OKL4 web browser BE Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2010 |
2009
|
|
|
Michael Hills Native OKL4 Android stack BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2009 |
|
|
|
Andrew Wrigley Steering-Integrated driver controls for sunswift IV BE Thesis, School of Electrical Engineering, Sydney, Australia, November, 2009 |
2008
|
|
|
Aaron Carroll I/O scheduling on RAID BE Thesis, School of Electrical Engineering, Sydney, Australia, July, 2008 |
2007
|
|
|
David Greenaway Quantifying the effects of scheduling on IPC performance BSc Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2007 |
|
|
|
Joshua Root Virtualising Darwin on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, February, 2007 |
2006
|
|
|
Clarence Dang Optimising L4 on Blackfin 533/537: An investigation into a high performance L4 microkernel without virtual memory BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006 |
|
|
|
Tom Birch Performance limits of Darwin on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006 |
2005
|
|
|
Geoffrey Lee I/O kit drivers for L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2005 |
|
|
|
Matthew Warton Single kernel stack L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2005 |
|
|
|
Philip Geoffrey Derrin A secure microkernel BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, June, 2005 |
|
|
|
Abi Nourai A physically-addressed L4 kernel BE Thesis, School of Computer Science and Engineering, Sydney, Australia, March, 2005 |
2003
|
|
 |
Ka-shu Wong MacOS X on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, December, 2003 |
2002
|
|
|
Andrew Baumann A thread model for Mungi BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
|
|
|
Ben Leslie Mungi device drivers BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
|
|
|
David C. Snowdon Hard- and software framework for the optimisation of Sunswift-II BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
|
|
|
Harvey Tuch A comparison of address translation mechanisms for virtually-addressed caches in embedded systems BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002 |
2000
|
|
|
Antony Edwards A component architecture for system extensibility BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000 |
|
|
|
Simon Winwood Flexible scheduling mechanisms in L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000 |
|
|
|
Patryk Zadarnowski The design and implementation of an extendible instruction set simulator BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000 |
1999
|
|
|
Luke Deller Loading and debugging tasks in SawMill BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Vincent Jayawardene An intensional engine on L4 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Daniel Potts L4 on uni- and multiprocessor Alpha BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Cristan Szmajda A new virtual memory implementation for L4/MIPS BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |
|
|
|
Adam Wiggins The design and implementation of the L4 microkernel on the StrongARM SA-1100 BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999 |