Skip to main content

Publications

Publications, Theses and Technical Reports

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

Our Best Papers

Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471-481, Seattle, Washington, USA, June, 2013
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
An analysis of power consumption in a smartphone
USENIX Annual Technical Conference, pp. 271-284, Boston, MA, USA, June, 2010
Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73-86, Big Sky, MT, US, October, 2009
Abstract PDF Dave Snowdon, Etienne Le Sueur, Stefan Petters and Gernot Heiser
Koala: A platform for OS-level power management
Eurosys 2009, pp. 289-302, Nuremburg, DE, April, 2009

All TS Publications

2017

Abstract to be published Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen
Verifying efficient function calls in CakeML
International Conference on Functional Programming, pp. 26, Oxford, September, 2017
Abstract PDF Rob van Glabbeek
Lean and full congruence formats for recursion
Proceedings 32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, June, 2017
Abstract PDF Annabelle McIver, Carroll Morgan and Tahiry Rabehaja
Algebra for quantitative information flow
International Conference on Relational and Algebraic Methods in Computer Science , pp. 3-23, Lyon, France, May, 2017
Abstract PDF Hira Syeda and Gerwin Klein
Reasoning about translation lookaside buffers
Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 490–508, Maun, Botswana, May, 2017
Abstract PDF Yuval Yarom, Daniel Genkin and Nadia Heninger
CacheBleed: A timing attack on OpenSSL constant time RSA
Journal of Cryptographic Engineering, Volume 7, Number 2, pp. 99–112, May, 2017
Abstract PDF Paul Grubbs, Thomas Ristenpart and Yuval Yarom
Modifying an enciphering scheme after deployment
Eurocrypt, Paris, FR, April, 2017
Abstract PDF Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish
Verified characteristic formulae for CakeML
European Symposium on Programming, pp. 584-610, Uppsala, Sweden, April, 2017
Abstract PDF Holger Hermanns and Peter Hoefner
Preface: Proceedings of the 2nd workshop on models for formal analysis of real systems
Electronic Proceedings in Theoretical Computer Science, pp. -, 2017
Abstract PDF Peter Hoefner, Damien Pous and Georg Struth
Preface: Proceedings of the 16th conference on relational and algebraic methods in computer science
Lecture Notes in Computer Science, pp. 2, 2017
Abstract PDF Ahmed Hussein, Mathias Payer, Tony Hosking and Chris Vick
One process to reap them all: Garbage collection as-a-service
ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments, pp. 171-186, Xi'an, China, April, 2017
Abstract PDF Rob van Glabbeek and Peter Hoefner
Split, send, reassemble: A formal specification of a CAN bus protocol stack
2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), pp. 14-52, Uppsala, Sweden, March, 2017
Abstract PDF Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138-150, Paris, France, January, 2017
Abstract PDF Anthony Fox, Magnus Myreen, Yong Kiam Tan and Ramana Kumar
Verified compilation of CakeML to multiple machine-code targets
Certified Programs and Proofs 2017, pp. 125-137, Paris, France, January, 2017
Abstract PDF Carroll Morgan
A demonic lattice of information
Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 203-222, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017
Abstract PDF Rob van Glabbeek
A branching time model of CSP
Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 272-293, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017

2016

Abstract PDF Thomas Allan, Billy Bob Brumley, Katrina Falkner, Joop van de Pol and Yuval Yarom
Amplifying side channels through performance degradation
Annual Computer Security Applications Conference, pp. 422-435, Los Angeles, CA, US, December, 2016
Abstract PDF Rudolf Berghammer, Nikita Danilenko, Peter Hoefner and Insa Stucke
Cardinality of relations with applications
Discrete Mathematics, Volume 339, Number 12, pp. 3089-3115, December, 2016
Abstract PDF 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 -, pp. 1-27, December, 2016
Abstract PDF Rob van Glabbeek
An algebraic treatment of recursion
Liber Amicorum for Jan A. Bergstra, pp. 58-59, Informatics Institute, University of Amsterdam, 2016
Abstract PDF Steve Blackburn, Amer Diwan, Mathias Hauswirth, Peter F. Sweeney, José Nelson Amaral, Timothy Brecht, L. Bulej, Cliff Click, Lieven Eeckhout, S. Fischmeister, Daniel Frampton, Laurie J. Hendren, M. Hind, Tony Hosking, Richard E. Jones, T. Kalibera, N. Keynes, N. Nystrom and Andreas Zeller
The truth, the whole truth, and nothing but the truth: A pragmatic guide to assessing empirical evaluations
ACM Transactions on Programming Languages and Systems, Volume 38, Number 4, pp. 15:1-20, October, 2016
Abstract to be published Stephen Blackburn, Amer Diwan, Matthias Hauswirth, Peter Sweeney, José Nelson Amaral, Tim Brecht, Lubomír Bulej, Cliff Click, Lieven Eeckhout, Sebastian Fischmeister, Daniel Frampton, Laurie Hendren, Michael Hind, Tony Hosking, Richard Jones, Tomas Kalibera, Nathan Keynes, Nathaniel Nystrom and Andreas Zeller
The truth, the whole truth, and nothing but the truth: A pragmatic guide to assessing empirical evaluations
ACM Transactions on Programming Languages, Volume 38, pp. 15:1-20, October, 2016
Abstract PDF Keith Chapman, Tony Hosking and Eliot Moss
Hybrid STM/HTM for nested transactions on OpenJDK
Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 660-676, Amsterdam, The Netherlands, October, 2016
Abstract PDF Keith Chapman, Tony Hosking and Eliot Moss
Extending OpenJDK to support hybrid STM/HTM
ACM SIGPLAN Workshop on Virtual Machines and Intermediate Languages, pp. 1-5, Amsterdam, The Netherlands, October, 2016
Abstract PDF Daniel Genkin, Lev Pachmanov, Itamar Pipman, Eran Tromer and Yuval Yarom
ECDSA key extraction from mobile devices via nonintrusive electromagnetic attacks
ACM Conference on Computer and Communications Security, pp. 1626-1638, Vienna, Austria, October, 2016
Abstract PDF César Pereida García, Billy Bob Brumly and Yuval Yarom
“Make sure DSA signing exponentiations really are constant-time”
ACM Conference on Computer and Communications Security, pp. 1639-1650, Vienna, Austria, October, 2016
Abstract PDF Yutaka Nagashima and Liam O'Connor
Close encounters of the higher kind - emulating constructor classes in standard ML
Abstract, ACM SIGPLAN Workshop on ML, September, 2016.
Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish
A new verified compiler backend for CakeML
International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016
Abstract PDF June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah
Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
International Conference on Interactive Theorem Proving, pp. 52-68, Nancy, France, August, 2016
Abstract PDF Joseph Chan and Michael Norrish
Proof pearl: Bounding least common multiples with triangles
International Conference on Interactive Theorem Proving, pp. 140–150, Nancy, France, August, 2016
Abstract PDF Leon Groot Bruinderink, Andreas Hülsing, Tanja Lange and Yuval Yarom
Flush, gauss, and reload – a cache attack on the BLISS lattice-based signature scheme
Conference on Cryptographic Hardware and Embedded Systems 2016 (CHES 2016), pp. 323-345, Santa Barbara, CA, US, August, 2016
Abstract PDF Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein
A framework for the automatic formal verification of refinement from Cogent to C
International Conference on Interactive Theorem Proving, Nancy, France, August, 2016
Abstract PDF Rob van Glabbeek, Peter Hoefner, Marius Portmann and Wee Lum Tan
Modelling and verifying the AODV routing protocol
Distributed Computing, Volume 29, Number 4, pp. 279-315, August, 2016
Abstract PDF Yuval Yarom, Daniel Genkin and Nadia Heninger
CacheBleed: A timing attack on OpenSSL constant time RSA
Conference on Cryptographic Hardware and Embedded Systems 2016 (CHES 2016), pp. 346-367, Santa Barbara, CA, US, August, 2016
Abstract PDF Wan Fokkink and Rob van Glabbeek
Divide and congruence II: delay and weak bisimilarity
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 778-787, New York City, USA, July, 2016
Abstract PDF Yong Kiam Tan, Scott Owens and Ramana Kumar
A verified type system for CakeML
Implementation and application of functional and programming languages, pp. 12, Koblenz, Germany, July, 2016
Winner: 2016 Peter Landin Prize for best paper
Abstract PDF Peter Hoefner and Bernhard Möller
Extended feature algebra
Journal of Logical and Algebraic Methods in Programming, Volume 85, Number 5, pp. 952-971, June, 2016
Abstract PDF Yi Lin, Steve Blackburn, Tony Hosking and Michael Norrish
Rust as a language for high performance GC implementation
International Symposium on Memory Management, pp. 89-98, Santa Barbara, California, USA, June, 2016
Abstract PDF Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
Compositional verification and refinement of concurrent value-dependent noninterference
IEEE Computer Security Foundations Symposium, pp. 417-431, Lisbon, Portugal, June, 2016
Abstract PDF Rudolf Berghammer, Peter Hoefner and Insa Stucke
Cardinality of relations and relational approximation algorithms
Journal of Logical and Algebraic Methods in Programming, Volume 85, Number 2, pp. 269-286, May, 2016
Abstract PDF Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser
Cogent: verifying high-assurance file system implementations
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175-188, Atlanta, GA, USA, April, 2016
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing (extended abstract)
European Symposium on Programming, pp. 95-122, Eindhoven, The Netherlands, April, 2016
Abstract PDF Wan Fokkink and Rob van Glabbeek
Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
Technical Report 9351, NICTA, April, 2016
Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Mechanizing a process algebra for network protocols
Journal of Automated Reasoning, Volume 56, Number 3, pp. 309-341, March, 2016
Abstract PDF Fangfei Liu, Qian Ge, Yuval Yarom, Frank Mckeen, Carlos Rozas, Gernot Heiser and Ruby B Lee
CATalyst: defeating last-level cache side channel attacks in cloud computing
IEEE Symposium on High-Performance Computer Architecture, pp. 406-418, Barcelona, Spain, March, 2016
Abstract PDF Daniel Matichuk, Toby Murray and Makarius Wenzel
Eisbach: A proof method language for isabelle
Journal of Automated Reasoning, Volume 56, Number 3, pp. 261-282, March, 2016
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing
Technical Report, NICTA, February, 2016

2015

Abstract PDF Sidney Amani and Toby Murray
Specifying a realistic file system
Workshop on Models for Formal Analysis of Real Systems, pp. 1-9, Suva, Fiji, November, 2015
Abstract
Slides
PDF June Andronick, Corey Lewis and Carroll Morgan
Controlled owicki-gries concurrency: reasoning about the preemptible eChronos embedded operating system
Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10-24, Suva, Fiji, November, 2015
Abstract PDF Rob van Glabbeek, Jan Friso Groote and Peter Hoefner
Preface: Proceedings of the workshop on models for formal analysis of real systems
Electronic Proceedings in Theoretical Computer Science, pp. -, Open Publishing Association, 2015
Abstract PDF Peter Hoefner
Using process algebra to design better protocols (abstract)
Forum “Math-for-Industry” 2015, pp. 31-33, Fukuoka, Japan, October, 2015
Abstract PDF Rudolf Berghammer, Peter Hoefner and Insa Stucke
Tool-based verification of a relational vertex coloring program
International Conference on Relational and Algebraic Methods in Computer Science , pp. 18, Braga, September, 2015
Abstract PDF Mojgan Kamali, Peter Hoefner, Maryam Kamali and Luigia Petre
Formal analysis of proactive, distributed routing
Software Engineering and Formal Methods, pp. 15, York, UK, September, 2015
Abstract PDF Paul Rimba, Liming Zhu, Len Bass, Ihor Kuz and Steve Reeves
Composing patterns to construct secure systems
European Dependable Computing Conference, pp. 213-224, Paris, France, September, 2015
Abstract PDF Rob van Glabbeek
Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP
Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, pp. 99-130, Oldenburg, Germany, September, 2015
Abstract PDF Rob van Glabbeek, Taolue Chen and Wan Fokkink
On the axiomatizability of impossible futures
Logical Methods in Computer Science, Volume 11, Number 3, pp. 1-31, September, 2015
Abstract PDF Yuval Yarom, Qian Ge, Fangfei Liu, Ruby B. Lee and Gernot Heiser
Mapping the Intel last-level cache
The Cryptology ePrint Archive, September, 2015
Abstract PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Verified over-approximation of the diameter of propositionally factored transition systems
International Conference on Interactive Theorem Proving, pp. 1-16, Nanjing, China, August, 2015
Abstract PDF Peter Baumgartner
SMTtoTPTP - a converter for theorem proving formats
International Conference on Automated Deduction, pp. 285-294, Berlin, Germany, August, 2015
Abstract PDF Peter Baumgartner, Joshua Bax and Uwe Waldmann
Beagle - a hierarchic superposition theorem prover
International Conference on Automated Deduction, pp. 367-377, Berlin, Germany, August, 2015
Abstract PDF Joseph Chan and Michael Norrish
Mechanisation of AKS algorithm: Part 1 – the main theorem
International Conference on Interactive Theorem Proving, pp. 117-136, Nanjing, China, August, 2015
Abstract PDF Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of a component platform
Technical Report, NICTA and UNSW, August, 2015
Abstract PDF Kirstin Peters and Rob van Glabbeek
Analysing and comparing encodability criteria
Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, pp. 46-60, Madrid, Spain, August, 2015
Abstract PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Exploiting symmetries by planning for a descriptive quotient
Proceedings of the 24th International Joint Conference on Artificial Intelligence, pp. 1479-1486, Buenos Aires, July, 2015
Abstract
Slides
PDF Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach
From non-preemptive to preemptive scheduling using synchronization synthesis
International Conference on Computer Aided Verification, San Francisco, USA, July, 2015
Abstract PDF Carroll Morgan
Abstract hidden markov models: A monadic account of quantitative information flow
IEEE Symposium on Logic in Computer Science, pp. 597-608, Tokyo, Japan, July, 2015
Abstract PDF Toby Murray
On high-assurance information-flow-secure programming languages
ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 43-48, Prague, Czech Republic, July, 2015
Abstract
Slides
PDF Sean Peters, Adrian Danis, Kevin Elphinstone and Gernot Heiser
For a microkernel, a big lock is fine
Asia-Pacific Workshop on Systems (APSys), Tokyo, JP, July, 2015
Abstract
Slides
PDF Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of RPC stub code
International Symposium on Formal Methods, pp. 273-290, Oslo, Norway, June, 2015
Abstract PDF Peter Gammie, Tony Hosking and Kai Engelhardt
Relaxing safely: verified on-the-fly garbage collection for x86-TSO
PLDI 2015: the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation., pp. 11, Portland, Oregon, United States, June, 2015
Abstract PDF Yi Lin, Stephen M. Blackburn, Kunshan Wang, Tony Hosking and Michael Norrish
Stop and go: Understanding yieldpoint behavior
International Symposium on Memory Management, pp. 70–80, Portland, OR, USA, June, 2015
Abstract
Slides
PDF Carroll Morgan
a nondeterministic lattice of information
One-hour invited talk at Mathematics of Program Construction, Königswinter, Germany, June, 2015
Abstract PDF Wolfram Kahl, Timothy G. Griffin and Peter Hoefner
Preface: Special issue on relational and algebraic methods in computer science
Journal of Logical and Algebraic Methods in Programming, pp. 283-284, 2015
Abstract PDF Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser and Ruby B Lee
Last-level cache side-channel attacks are practical
IEEE Symposium on Security and Privacy, pp. 605-622, San Jose, CA, US, May, 2015
Abstract PDF Michael Norrish and Michelle Mills Strout
An approach for proving the correctness of inspector/executor transformations
Languages and Compilers for Parallel Computing, pp. 131–145, Hillsboro, Oregon, USA, May, 2015
Abstract PDF Kunshan Wang, Yi Lin, Stephen M Blackburn, Michael Norrish and Tony Hosking
Draining the swamp: Micro virtual machines as a solid foundation for language development
SNAPL, pp. 321–336, Asilomar, California, May, 2015
Abstract PDF Franck Cassez, Takashi Matsuoka, Edward Pierzchalski and Nathan Smyth
Perentie: Modular trace refinement and selective value tracking
SV-COMP-2015, pp. 439-442, London, UK, April, 2015
Abstract PDF Rob van Glabbeek and Peter Hoefner
CCS: It's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
Acta Informatica, Volume 52, Number 2-3, pp. 175-205, April, 2015
Abstract PDF Don Batory, Peter Hoefner, Dominik Köppl and Bernhard Möller
Structured document algebra in action
Lecture Notes in Computer Science, Volume 8950, pp. 291-311, March, 2015
Abstract Slides Gernot Heiser
seL4: Present and future
invited talk at FOSDEM'15, Brussels, BE, February, 2015
Abstract PDF Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples
Empirical study towards a leading indicator for cost of formal software verification
International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015
Abstract PDF Rob van Glabbeek, Ursula Goltz and Ernst-Rüdiger Olderog
Special issue on "Combining Compositionality and Concurrency": Part 1
Acta Informatica, pp. 3-4, Springer, 2015
Abstract Slides
Video
Peter Chubb
SD cards and filesystems for embedded systems
linux.conf.au, Auckland, NZ, January, 2015
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
SAT-based strategy extraction in reachability games
AAAI, Austin, TX, USA, January, 2015
Abstract Slides
Video
Gernot Heiser
seL4 is free – what does this mean for you?
Abstract, LCA.
Abstract PDF Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray
An empirical research agenda for understanding formal methods productivity
Information and Software Technology, Volume 60, pp. 102-112, January, 2015
Abstract PDF Rob van Glabbeek and Peter Hoefner
Progress, fairness and justness in process algebra
Technical Report 8501, NICTA, January, 2015

2014

Abstract PDF Hyungsoo Jung, Hyuck Han, Alan Fekete, Gernot Heiser and Heon Yeom
A scalable lock manager for multicores
ACM Transactions on Database Systems, Volume 39, Number 4, pp. 29:1–29:29, December, 2014
Abstract
Slides
PDF Anna Lyons and Gernot Heiser
Mixed-criticality support in a high-assurance, general-purpose microkernel
Workshop on Mixed Criticality Systems, pp. 9-14, Rome, Italy, December, 2014
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
A mechanized proof of loop freedom of the (untimed) AODV routing protocol
International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 47-63, Sydney, Australia, November, 2014
Abstract PDF David Cock, Qian Ge, Toby Murray and Gernot Heiser
The last mile: An empirical study of some timing channels on seL4
ACM Conference on Computer and Communications Security, pp. 570-581, Scottsdale, AZ, USA, November, 2014
Abstract PDF Matthias Daum, Nelson Billing and Gerwin Klein
Concerned with the unprivileged: User programs in kernel refinement
Formal Aspects of Computing, Volume 26, Number 6, pp. 1205-1229, October, 2014
Abstract PDF Liam O'Connor-Davis, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah
CDSL version 1: Simplifying verification with linear types
Technical Report, NICTA, October, 2014
Abstract
Slides
PDF Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm and Mona Vij
User-guided device driver synthesis
USENIX Symposium on Operating Systems Design and Implementation, pp. 661-676, Broomfield, CO, USA, October, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014
Abstract PDF Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski
Productivity for proof engineering
Empirical Software Engineering and Measurement, pp. 15, Turin, Italy, September, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Technical Report NRL-8281, NICTA, August, 2014
Abstract PDF Peter Baumgartner, Joshua Bax and Uwe Waldmann
Finite quantification in hierarchic theorem proving
International Joint Conference on Automated Reasoning (IJCAR), pp. 152-167, Vienna, Austria, July, 2014
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Showing invariance compositionally for a process algebra for network protocols
International Conference on Interactive Theorem Proving, pp. 44-59, Vienna, Austria, July, 2014
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Regression-free synthesis for concurrency
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF David Cock
From probabilistic operational semantics to information theory - side channels with pGCL in isabelle
Proceedings of the 5th International Conference on Interactive Theorem Proving, pp. 1–15, Vienna, Austria, July, 2014
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Real reward testing for probabilistic processes
Theoretical Computer Science, Volume 538, pp. 16-36, July, 2014
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Interpolants in two-player games
Abstract, iPRA workshop, July, 2014.
Abstract PDF Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish
Beagle as a HOL4 external ATP method
Practical Aspects of Automated Reasoning, pp. 50-59, Vienna, July, 2014
Abstract PDF Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Practical CNF interpolants via BDDs
Abstract, iPRA workshop, July, 2014.
Abstract PDF Daniel Matichuk, Makarius Wenzel and Toby Murray
An Isabelle proof method language
International Conference on Interactive Theorem Proving, pp. 390-405, Vienna, Austria, July, 2014
Abstract PDF Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith
Additive and multiplicative notions of leakage, and their capacities
computer security foundations, pp. 308-322, vienna, Austria, July, 2014
Abstract PDF Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Christopher Walker
Solving games without controllable predecessor
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF Daniel Potts, Rene Bourquin, Leslie Andresen, June Andronick, Gerwin Klein and Gernot Heiser
Mathematically verified software kernels: Raising the bar for high assurance implementations
Technical Report, NICTA, July, 2014
Abstract PDF Thomas Sewell
Formal replay of translation validation for highly optimised c: Work in progress
Verification and Program Transformation, Vienna, Austria, July, 2014
Abstract
Slides
PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Mechanising theoretical upper bounds in planning
Workshop on Knowledge Engineering for Planning and Scheduling, Portsmouth, USA, June, 2014
Abstract PDF David Greenaway, Japheth Lim, June Andronick and Gerwin Klein
Don't sweat the small stuff: Formal verification of C code without the pain
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 429–439, Edinburgh, UK, June, 2014
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu
Automatic verification of active device drivers
ACM Operating Systems Review, Volume 48, Number 1, May, 2014
Abstract PDF Peter Hoefner, Peter Jipsen, Wolfram Kahl and Martin Eric Müller
Preface: Relational and algebraic methods in computer science
Lecture Notes in Computer Science, pp. 2, 2014
Abstract PDF Gerwin Klein
Proof engineering challenges for large-scale verification
Abstract, AI4FM/2014 Workshop.
Abstract PDF Gerwin Klein and Tobias Nipkow
Applications of interactive proof to data flow analysis and security
Software Systems Safety, pp. 77-134, Volume 36 in NATO Science for Peace and Security Series , IOS Press BV, 2014
Abstract PDF Rudolf Berghammer, Peter Hoefner and Insa Stucke
Automated verification of relational while-programs
14th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2014), pp. 16, Marienstatt im Westerwald, Germany, April, 2014
Abstract
Slides
PDF Bernard Blackham, Mark Liffiton and Gernot Heiser
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 169-178, Berlin, Germany, April, 2014
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
Unifying DVFS and offlining in mobile multicores
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 287-296, Berlin, Germany, April, 2014
Abstract PDF Peter Hoefner and Annabelle McIver
Hopscotch—reaching the target hop by hop
Journal of Logical and Algebraic Methods in Programming (JLAMP), Volume 83, Number 2, pp. 212-224, April, 2014
Abstract
Slides
PDF Gerwin Klein
Proof engineering considered essential
International Symposium on Formal Methods (FM), pp. 16-21, Singapore, April, 2014
Abstract PDF Carroll Morgan, Annabelle McIver, Geoffrey Smith, Barbara Espinoza and Larisa Meinicke
Abstract channels and their robust information-leakage ordering
Principles of Security and Trust (ETAPS), pp. 83-102, Grenoble, France, April, 2014
Abstract PDF Aditi Barthwal and Michael Norrish
A mechanisation of some context-free language theory in HOL4
Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 2014
Abstract PDF Peter Baumgartner
Model evolution based theorem proving
IEEE Intelligent Systems Magazine (IEEE ISM), Volume 29, Number 1, pp. 4-10, February, 2014
Abstract PDF Peter Baumgartner and Uwe Waldmann
Hierarchic superposition with weak abstraction and the beagle theorem prover
Deduction and Arithmetic (Dagstuhl Seminar 13411), pp. 7, Dagstuhl, Germany,, February, 2014
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract PDF Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens
CakeML: A verified implementation of ML
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014

2013

Abstract to be published Peter Baumgartner
Automatische inferenz
Handbuch der Kuenstlichen Intelligenz, pp. 129-167, Oldenbourg Verlag, 2013
Abstract PDF Peter Baumgartner and Joshua Bax
Proving infinite satisfiability
International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 86-95, Stellenbosch, South Africa, December, 2013
Abstract PDF Joseph Chan and Michael Norrish
A string of pearls: Proofs of fermat's little theorem
Journal of Formal Reasoning, Volume 6, Number 1, pp. 63–87, December, 2013
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV
Technical Report 5513, NICTA, December, 2013
Abstract PDF Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Christopher Walker and Alexander Legg
Device driver synthesis
Intel Technology Journal, Volume 17, Number 2, pp. 136-157, December, 2013
Abstract PDF Peter Baumgartner and Uwe Waldmann
Hierarchic superposition: Completeness without compactness
Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), pp. 8-12, Nanning, China, November, 2013
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
Mobile multicores: Use them or waste them
Workshop on Power Aware Computing and Systems, pp. 5, Farmington, PA, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 44-48.
Abstract
Slides
PDF
Presentation Video
Kevin Elphinstone and Gernot Heiser
From L3 to seL4 – what have we learnt in 20 years of L4 microkernels?
ACM Symposium on Operating Systems Principles, pp. 133-150, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor-Davis, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser
File systems deserve verification too!
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Farmington, Pennsylvania, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64.
Abstract PDF Rob van Glabbeek, Peter Hoefner, Wee Lum Tan and Marius Portmann
Sequence numbers do not guarantee loop freedom - AODV can yield routing loops
16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems, pp. 91-100, Barcelona, Spain, November, 2013
Abstract PDF Don Batory, Peter Hoefner, Bernhard Möller and Andreas Zelend
Features, modularity, and variation points
Fifth International Workshop on Feature-Oriented Software Development (FOSD), pp. 8, Indianapolis, Indiana, USA, October, 2013
Abstract
Slides
PDF Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell
Formally verified system initialisation
Proceedings of the 15th International Conference on Formal Engineering Methods, pp. 70-85, Queenstown, New Zealand, October, 2013
Abstract
Slides
PDF Yao Shi, Bernard Blackham and Gernot Heiser
Code optimizations using formally verified properties
Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 427-442, Indianapolis, USA, October, 2013
Abstract PDF Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish
Tableaux for verification of data-centric processes
Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28-43, Nancy, France, September, 2013
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann
On characterising distributability
Logical Methods in Computer Science, Volume 9, Number 3, pp. 1-58, September, 2013
Abstract PDF Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta
Topology-based mobility models for wireless networks
10th International Conference on Quantitative Evaluation of SysTems (QEST 2013), pp. 16, Buenos Aires, Argentina, August, 2013
Abstract PDF Peter Hoefner and Maryam Kamali
Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking
11th International Conference on Formal Modeling and Analysis of Timed Systems (Formats '13), pp. 15, Buenos Aires, Argentina, August, 2013
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
The systems hacker’s guide to the Galaxy: Energy usage in a modern smartphone
Asia-Pacific Workshop on Systems (APSys), pp. 7, Singapore, July, 2013
Best Student Paper Award!
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Efficient synthesis for concurrency by semantics-preserving transformations
25th International Conference on Computer Aided Verification, pp. 1–16, Saint Petersburg, Russia, July, 2013
Abstract PDF David Cock
Practical probability: Applying pGCL to lattice scheduling
Proceedings of the 4th International Conference on Interactive Theorem Proving, pp. 1–16, Rennes, France, July, 2013
Abstract
Slides
PDF Gernot Heiser
Can truly dependable systems be affordable?
Keynote at APSys'13, Singapore, July, 2013
Abstract
Slides
PDF Michael Norrish and Brian Huffman
Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁
International Conference on Interactive Theorem Proving, pp. 133-146, Rennes, France, July, 2013
Abstract PDF Peter Baumgartner and Uwe Waldmann
Hierarchic superposition with weak abstraction
Conference on Automated Deduction, pp. 39-57, Lake Placid, New York, USA, June, 2013
Abstract
Slides
PDF Hyungsoo Jung, Hyuck Han, Alan Fekete, Gernot Heiser and Heon Y. Yeom
A scalable lock manager for multicores
ACM SIGMOD Conference, pp. 73-84, New York, USA, June, 2013
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471-481, Seattle, Washington, USA, June, 2013
Abstract
Slides
PDF Aleksander Budzynowski and Gernot Heiser
The von Neumann architecture is due for retirement
Workshop on Hot Topics in Operating Systems, pp. 6, Santa Ana Pueblo, NM, USA, May, 2013
Abstract PDF Peter Hoefner and Annabelle McIver
Statistical model checking of wireless mesh routing protocols
5th NASA Formal Methods Symposium (NFM 2013), pp. 15, Moffett Field, CA, USA, May, 2013
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013
Abstract PDF Toby Murray and Thomas Sewell
Above and beyond: seL4 noninterference and binary verification
Abstract, 2013 High Confidence Software and Systems Conference, Annapolis, MD, May, 2013.
Abstract PDF Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass
Formal specifications better than function points for code sizing
International Conference on Software Engineering, pp. 1257-1260, San Francisco, USA, May, 2013
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Sequoll: A framework for model checking binaries
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 97-106, Philadelphia, USA, April, 2013
Best Paper Award!
Abstract
Slides
PDF Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie and Gustavo Alonso
RapiLog: reducing system complexity through verification
EuroSys Conference, pp. 323-336, Prague, Czech Republic, April, 2013
Abstract PDF Tudor-Ioan Salomie, Gustavo Alonso, Timothy Roscoe and Kevin Elphinstone
Application level ballooning for efficient server consolidation
EuroSys Conference, pp. 337 - 350, Prague, Czech Republic, April, 2013
Abstract
Slides
PDF Gernot Heiser
Protecting e-government against attacks
EP Workshop on Security of e-Government, pp. 5, Brussels, Belgium, February, 2013
Abstract PDF Toby Murray
On the limits of refinement-testing for model-checking CSP
Formal Aspects of Computing, Volume 25, Number 2, pp. 219-256, February, 2013

2012

Abstract PDF Daniel Matichuk and Toby Murray
Extensible specifications for automatic re-use of specifications and proofs
10th International Conference on Software Engineering and Formal Methods, pp. 8, Thessaloniki, Greece, December, 2012
Abstract PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein
Noninterference for operating system kernels
International Conference on Certified Programs and Proofs, pp. 126-142, Kyoto, Japan, December, 2012
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
Automatic verification of message-based device drivers
Systems Software Verification, pp. 1–14, Sydney, Australia, November, 2012
Abstract PDF David Cock
Verifying probabilistic correctness in Isabelle with pGCL
Proceedings of the 7th Systems Software Verification, pp. 1–10, Sydney, Australia, November, 2012
Abstract PDF June Andronick, Andrew Boyton and Gerwin Klein
Final report for AOARD grant #FA2386-11-1-4070, formal system verification - extension
Technical Report, NICTA, October, 2012
Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105
Technical Report, NICTA, October, 2012
Abstract PDF Hing-Lun Chan and Michael Norrish
A string of pearls: Proofs of fermat’s little theorem
International Conference on Certified Programs and Proofs, pp. 188-207, Kyoto, Japan, October, 2012
Abstract PDF Matthew Fernandez, Ihor Kuz and Gerwin Klein
Formalisation of a component platform
Poster presented at Operating Systems Design and Implementation 2012, October, 2012
Abstract PDF Peter Hoefner and Sarah Edenhofer
Towards a rigorous analysis of AODVv2 (DYMO)
2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), pp. 1-6, Austin, Texas, October, 2012
Abstract PDF Peter Hoefner, Rob van Glabbeek, Wee Lum Tan, Marius Portmann, Annabelle McIver and Ansgar Fehnker
A rigorous analysis of AODV and its variants
15th ACM/IEEE International Conference on Modelling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM 2012), pp. 203-212, Paphos, Cyprus, October, 2012
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
Active device drivers
Technical Report, NICTA, September, 2012
Abstract PDF Nick Barnes, Peter Baumgartner, Tiberio Caetano, Hugh Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter Stuckey, Sylvie Thiebaux, Pascal Van Hentenryck and Toby Walsh
AI @ NICTA
AI Magazine, Volume 33, Number 3, pp. 115-127, September, 2012
Abstract PDF Peter Baumgartner, Bjoern Pelzer and Cesare Tinelli
Model evolution with equality - revised and implemented
Journal of Symbolic Computation, Volume 47, Number 9, pp. 1011-1045, September, 2012
Abstract PDF Peter Hoefner, Bernhard Möller and Andreas Zelend
Foundations of coloring algebra with consequences for feature-oriented programming
13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 13), pp. 16, Cambridge, UK, September, 2012
Abstract PDF June Andronick and Gerwin Klein
Formal system verification - extension 2, final report AOARD #FA2386-12-1-4022
Technical Report, NICTA, August, 2012
Abstract PDF James Cheney, Michael Norrish and René Vestergaard
Formalizing adequacy: A case study for higher-order abstract syntax
Journal of Automated Reasoning, Volume 49, Number 2, pp. 209–239, August, 2012
Abstract PDF David Greenaway, June Andronick and Gerwin Klein
Bridging the gap: Automatic verified abstraction of C
International Conference on Interactive Theorem Proving, pp. 99-115, Princeton, New Jersey, USA, August, 2012
Abstract PDF Peter Hoefner
Towards a representation theorem for coloring algebra
Abstract, Workshop on Lattices and Relations, August, 2012.
Abstract PDF Peter Hoefner
Kleene modules for routing procedures
Abstract, Workshop on Lattices and Relations, August, 2012.
Abstract PDF Gerwin Klein, Rafal Kolanski and Andrew Boyton
Mechanised separation algebra
International Conference on Interactive Theorem Proving, pp. 332-337, Princeton, USA, August, 2012
Abstract PDF Ihor Kuz, Liming Zhu, Len Bass, Mark Staples and Sherry Xu
An architectural approach for cost effective trustworthy systems
IEEE/IFIP Working Conference on Software Architecture (WICSA), pp. 325-328, Helsinki, Finland, August, 2012
Abstract PDF Rob van Glabbeek
Musings on encodings and expressiveness
Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structural Operational Semantics, pp. 81–98, Newcastle upon Tyne, United Kingdom, August, 2012
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Correct, fast, maintainable – choose any three!
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract
Slides
PDF Bernard Blackham, Vernon Tang and Gernot Heiser
To preempt or not to preempt, that is the question
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract PDF Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski
Challenges and experiences in managing large-scale proofs
Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, pp. 32-48, Bremen, Germany, July, 2012
Abstract PDF Peter Hoefner, Rob van Glabbeek and Ian Hayes
Preface—Morgan: A suitable case for treatment
Formal Aspects of Computing, Volume 24, Number 4-6, pp. 417-422, July, 2012
Abstract PDF Peter Hoefner and Bernhard Möller
Dijkstra, Floyd and Warshall meet Kleene
Formal Aspects of Computing (FAOC), Volume 24, Number 4-6, pp. 459-476, July, 2012
Abstract PDF June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, Jason Zhang and Liming Zhu
Large-scale formal verification in practice: A process perspective
International Conference on Software Engineering, pp. 1002-1011, Zurich, Switzerland, June, 2012
Abstract PDF Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski
Simulation modeling of a large scale formal verification process
International Conference on Software and Systems Process, pp. 3-12, Zurich, Switzerland, June, 2012
Abstract PDF June Andronick, Gerwin Klein and Andrew Boyton
Formal system verification - extension, AOARD 114070
Technical Report, NICTA, May, 2012
Abstract PDF Wan Fokkink, Rob van Glabbeek and Paulien de Wind
Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity
Information and Computation (I&C), Volume 214, Number , pp. 59-85, May, 2012
Abstract
Slides
PDF Bernard Blackham, Yao Shi and Gernot Heiser
Improving interrupt response time in a verifiable protected microkernel
EuroSys Conference, pp. 323-336, Bern, Switzerland, April, 2012
Abstract PDF Matthew Fernandez, Gerwin Klein and Ihor Kuz
Microkernel verification down to assembly
Poster presented at EuroSys 2012, April, 2012
Abstract PDF Gerwin Klein
Interactive proof: Applications to semantics
Software Safety and Security: Tools for Analysis and Verification, pp. 85-125, IOS Press, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
A process algebra for wireless mesh networks
22nd European Symposium on Programming (ESOP 2012), pp. 295-315, Tallinn, Estonia, March, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Automated analysis of AODV using UPPAAL
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), pp. 173-187, Tallinn, Estonia, March, 2012
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
It's time for trustworthy systems
IEEE Security and Privacy, Volume 10, Number 2, pp. 67-70, March, 2012
Abstract PDF Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Peter Baumgartner
The TPTP typed first-order form and arithmetic
Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 406-419, Merida, Venezuela, March, 2012
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann
On distributability of petri nets (extended abstract)
15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), pp. 331–345, Tallinn, Estonia, March, 2012
Abstract Video Peter Chubb
Bourne shell tutorial
Tutorial at Linux.conf.au, Ballarat, January, 2012
Abstract Video Peter Chubb
Linux as a boot loader
Talk at linux.conf.au, Ballarat, January, 2012
Abstract PDF Stefan M Petters, Kevin Elphinstone and Gernot Heiser
Trustworthy real-time systems
Advances in Real-Time Systems, pp. 191-206, Springer, 2012

2011

Abstract PDF Rob van Glabbeek
Bisimulation
Encyclopedia of Parallel Computing, pp. 136-139, Volume 1 in , Springer, 2011
Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report option 1 – AOARD 104105
Technical Report, NICTA, November, 2011
Abstract PDF Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser
Timing analysis of a protected operating system kernel
IEEE Real-Time Systems Symposium, pp. 339-348, Vienna, Austria, November, 2011
Abstract PDF David Cock
Exploitation as an inference problem
4th Workshop on Artificial Intelligence and Security, pp. 105–106, Chicago, IL, USA, October, 2011
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Modelling and analysis of AODV in UPPAAL
1st International Workshop on Rigorous Protocol Engineering, pp. 1-6, Vancouver, October, 2011
Abstract PDF Peter Hoefner, Don Batory and Jongwook Kim
Feature interactions, products, and composition
Generative Programming and Component Engineering (GPCE'11), pp. 13-22, Portland, OR, United States, October, 2011
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
On causal semantics of petri nets (extended abstract)
22nd International Conference on Concurrency Theory, pp. 43-59, Aachen, Germany, September, 2011
Abstract PDF Peter Baumgartner and Uwe Waldmann
A combined superposition and model evolution calculus
Journal of Automated Reasoning, Volume 47, Number 2, pp. 191-227, August, 2011
Abstract
Slides
PDF Michael Norrish
Mechanised computability theory
International Conference on Interactive Theorem Proving, pp. 297–311, Nijmegen, The Netherlands, August, 2011
Abstract PDF Sidney Amani, Leonid Ryzhyk, Alastair Donaldson, Gernot Heiser, Alexander Legg and Yanjin Zhu
Static analysis of device drivers: we can do better!
Asia-Pacific Workshop on Systems (APSys), pp. 1-5, Shanghai, China, July, 2011
Abstract PDF Bernard Blackham, Yao Shi and Gernot Heiser
Protected hard real-time: The next frontier
Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Real reward testing for probabilistic processes (extended abstract)
Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), pp. 61-73, Saarbrücken, Germany, July, 2011
Abstract PDF Peter Hoefner, Ridha Khedri and Bernhard Möller
Supplementing product families with behaviour
International Journal of Software and Informatics (IJSI), Volume 5, Number 1-2, Part II, pp. 245-266, July, 2011
Abstract to be published Richard Jones, Tony Hosking and Eliot Moss
The garbage collection handbook: The art of automatic memory management
Chapman and Hall/CRC Press, 2011
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
Abstract processes of place/transition systems
Information Processing Letters, Volume 111, Number 13, pp. 626-633, July, 2011
Abstract PDF Prashant Varanasi and Gernot Heiser
Hardware-supported virtualization on ARM
Asia-Pacific Workshop on Systems (APSys), pp. 5 pages, Shanghai, China, July, 2011
Abstract PDF Han-Hing Dang, Bernhard Möller and Peter Hoefner
Algebraic separation logic
The Journal of Logic and Algebraic Programming, Volume 80, Number 6, pp. 221-247, June, 2011
Abstract PDF Gernot Heiser
Virtualizing embedded systems – why bother?
Design Automation Conference (DAC), pp. 901-905, Dan Diego, CA, USA, June, 2011
Abstract PDF Peter Hoefner and Bernhard Möller
Fixing zeno gaps
Theoretical Computer Science, Volume 412, Number 28, pp. 3303-3322, June, 2011
Abstract PDF Etienne Le Sueur and Gernot Heiser
Slow down or sleep, that is the question
USENIX Technical Conference, pp. 6, Portland, Oregon, USA, June, 2011
Abstract PDF Rob van Glabbeek
On cool congruence formats for weak bisimulations
Theoretical Computer Science, Volume 412, Number 28, pp. 3283-3302, June, 2011
Abstract
Slides
PDF Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski
What if you could actually Trust your kernel?
Workshop on Hot Topics in Operating Systems, pp. 1-5, Napa, CA, USA, May, 2011
Abstract PDF Peter Hoefner and Annabelle McIver
Towards an algebra of routing tables
12th International Conference on Relational and Algebraic Methods in Computer Science, pp. 212-229, Rotterdam, Netherlands, May, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems, pp. 5, Napa, USA, May, 2011
Abstract PDF Ihor Kuz, Zachary Anderson, Pravin Shinde and Timothy Roscoe
Multicore OS benchmarks: we can do better
Workshop on Hot Topics in Operating Systems, pp. 1-5, Napa, CA, USA, May, 2011
Abstract PDF June Andronick and Gerwin Klein
Formal system verification for trustworthy embedded systems, final report AOARD 094160
Technical Report, NICTA, April, 2011
Abstract PDF Peter Baumgartner and Cesare Tinelli
Model evolution with equality modulo built-in theories
International Conference on Automated Deduction, pp. 85-100, Wroclaw, Poland, April, 2011
Abstract PDF Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser
Improved device driver reliability through hardware verification reuse
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 1-12, Newport Beach, CA, USA, March, 2011

2010

Abstract PDF June Andronick
From a proven correct microkernel to trustworthy large systems
International Conference on Formal Verification of Object-Oriented Software, pp. 1-9, Paris, December, 2010
Abstract PDF June Andronick, David Greenaway and Kevin Elphinstone
Towards proving security in the presence of large untrusted components
Systems Software Verification, pp. 9, Vancouver, Canada , October, 2010
Abstract PDF David Cock
Lyrebird - assigning meanings to machines
Systems Software Verification, pp. 1–9, Vancouver, BC, Canada , October, 2010
Abstract PDF Yuxin Deng and Rob van Glabbeek
Characterising probabilistic processes logically (extended abstract)
Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 278-293, Yogyakarta, Indonesia, October, 2010
Abstract PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3-10, Chicago, IL, USA, October, 2010
Abstract PDF Etienne Le Sueur and Gernot Heiser
Dynamic voltage and frequency scaling: The laws of diminishing returns
Workshop on Power Aware Computing and Systems, pp. 1–5, Vancouver, Canada, October, 2010
Abstract PDF Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser
Improved device driver reliability through verification reuse
Workshop on Hot Topics in System Dependability, pp. 1-6, Vancouver, Canada, October, 2010
Abstract PDF Rob van Glabbeek
The coarsest precongruences respecting safety and liveness properties
Theoretical Computer Science 2010, pp. 32-52, Brisbane, September, 2010
Abstract PDF Rob van Glabbeek and Gordon Plotkin
On CSP and the algebraic theory of effects
Reflections on the Work of C.A.R. Hoare, pp. 333-369, Volume in History of Computing, Springer, 2010
Abstract PDF Aditi Barthwal and Michael Norrish
A formalisation of the normal forms of context-free grammars in HOL4
19th EACSL Annual Conferences on Computer Science Logic, pp. 95-109, Brno, Czech Republic, August, 2010
Abstract PDF Nicholas Fitzroy-Dale, Ihor Kuz and Gernot Heiser
Architecture optimisation with Currawong
Asia-Pacific Workshop on Systems (APSys), pp. 7-12, New Delhi, India, August, 2010
Abstract PDF Gernot Heiser and Ben Leslie
The OKL4 microvisor: Convergence point of microkernels and hypervisors
Asia-Pacific Workshop on Systems (APSys), pp. 19-24, New Delhi, India, August, 2010
Abstract PDF Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker
capDL: A language for describing capability-based systems
Asia-Pacific Workshop on Systems (APSys), pp. 31-35, New Delhi, India, August, 2010
Abstract PDF Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser
The case for active device drivers
Asia-Pacific Workshop on Systems (APSys), pp. 25-30, New Delhi, India, August, 2010
Abstract PDF Aditi Barthwal and Michael Norrish
Mechanisation of PDA and grammar equivalence for context-free languages
17th Workshop on Logic, Language, Information and Computation , pp. 125-135, Brasília, Brazil, July, 2010
Abstract
Slides
PDF Ramana Kumar and Michael Norrish
(nominal) unification by recursive descent with triangular substitutions
International Conference on Interactive Theorem Proving, pp. 51-66, Edinburgh, United Kingdom, July, 2010
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
An analysis of power consumption in a smartphone
USENIX Annual Technical Conference, pp. 271-284, Boston, MA, USA, June, 2010
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107-115, June, 2010
Research Highlights paper
Abstract PDF Peter Baumgartner and Evgenij Thorstensen
Instance based methods - an overview
Künstliche Intelligenz, Volume 24, Number 1, pp. 35-42, April, 2010
Abstract PDF Gerwin Klein, Thomas Sewell and Simon Winwood
Refinement in the formal verification of seL4
Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323-339, Springer, 2010
Abstract PDF Peter Baumgartner, Ulrich Furbach and Bjoern Pelzer
The hyper tableaux calculus with equality and an application to finite model computation
Journal of Logic and Computation, Volume 20, Number 1, pp. 77-101, February, 2010
Abstract PDF
Presentation Video
Peter Chubb
Decent MIDI from LilyPond
Linux.conf.au, January, 2010
Abstract PDF Peter Chubb and John Judge
When the arduino meets year 9
Other Conference Presentation, linux.conf.au, Wellington, New Zealand, January, 2010.
Abstract PDF Peter Chubb and Yang Song
Interrupts considered harmful
Other Conference Presentation, Linux.conf.au, Wellington, NZ, January, 2010.

2009

Abstract PDF Gerwin Klein
Correct OS kernel? Proof? Done!
USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009
Abstract PDF Rob van Glabbeek, Bas Luttik and Nikola Trčka
Computation tree logic with deadlock detection
Logical Methods in Computer Science, Volume 5, Number 4:5, pp. 1-24, December, 2009
Abstract PDF Ralf Huuck, Gerwin Klein and Schlich Bastian
Proc. 4th international workshop on system software verification (SSV09)
Electronic Notes in Theoretical Computer Science, Volume 254, pp. 1-3, October, 2009
Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF Michael Norrish
Rewriting conversions implemented with continuations
Journal of Automated Reasoning, Volume 43, Number 3, pp. 305-336, October, 2009
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73-86, Big Sky, MT, US, October, 2009
Abstract PDF Rob van Glabbeek and Gordon Plotkin
Configuration structures, event structures and petri nets
Theoretical Computer Science, Volume 410, Number 41, pp. 4111-4159, September, 2009
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Testing finitary probabilistic processes (extended abstract)
20th International Conference on Concurrency Theory (CONCUR 2009), pp. 274-288, Bologna, Italy, August, 2009
Abstract PDF Rafal Kolanski and Gerwin Klein
Types, maps and separation logic
International Conference on Theorem Proving in Higher Order Logics, pp. 276-292, Munich, Germany, August, 2009
Abstract PDF Stefan M. Petters, Martin Lawitzky, Ryan Heffernan and Kevin Elphinstone
Towards real multi-criticality scheduling
IEEE Conference on Embedded and Real-Time Computing and Applications, pp. 155-164, Beijing, China, August, 2009
Abstract PDF Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
International Conference on Theorem Proving in Higher Order Logics, pp. 500-515, Munich, Germany, August, 2009
Abstract PDF Franz Baader, Andreas Bauer, Peter Baumgartner, Anne Cregan, Alfredo Gabaldon, Krystian Ji, Kevin Lee, David Rajaratnam and Rolf Schwitter
A novel architecture for situation awareness systems
TABLEAUX 2009 - The 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 77-92, Oslo, Norway, July, 2009
Abstract PDF Peter Baumgartner and John Slaney
Constraint modelling: A challenge for first order automated reasoning
International Workshop on First-Order Theorem Proving (FTP'09), pp. 4-18, Oslo, Norway, July, 2009
Abstract PDF Peter Baumgartner and Uwe Waldmann
Superposition and model evolution combined
Automated Deduction - CADE-22, pp. 17-34, Montreal, Canada, July, 2009
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
Symmetric and asymmetric asynchronous interaction
Electronic Notes in Theoretical Computer Science, Volume 229, Number 3, pp. 77-95, July, 2009
Abstract PDF Matthew Chapman and Gernot Heiser
vNUMA: A virtual shared-memory multiprocessor
USENIX Annual Technical Conference, pp. 349-362, San Diego, USA, June, 2009
Abstract PDF Rob van Glabbeek, Bas Luttik and Nikola Trčka
Branching bisimilarity with explicit divergence
Fundamenta Informaticae, Volume 93, Number 4, pp. 371-392, June, 2009
Abstract PDF Gernot Heiser
Trusted <= trustworthy <= proof – position paper
Future of Trust in Computing, pp. 55-59, Berlin, May, 2009
Abstract PDF Gerwin Klein, Ralf Huuck and Bastian Schlich
Operating system verification
Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123-124, April, 2009
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser
Dingo: Taming device drivers
Eurosys 2009, pp. 275-288, Nuremberg, DE, April, 2009
Abstract PDF Dave Snowdon, Etienne Le Sueur, Stefan Petters and Gernot Heiser
Koala: A platform for OS-level power management
Eurosys 2009, pp. 289-302, Nuremburg, DE, April, 2009
Abstract PDF Aditi Barthwal and Michael Norrish
Verified, executable parsing
European Symposium on Programming, pp. 160-174, York, March, 2009
Abstract PDF James Cheney, René Vestergaard and Michael Norrish
Formalizing adequacy
2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming, York, March, 2009
Abstract PDF Nicholas Fitzroy-Dale and Ihor Kuz
Towards automatic optimisation of componentised systems
Workshop on Isolation and Integration in Embedded Systems, pp. 6, Nuremberg, Germany, March, 2009
Abstract PDF Gernot Heiser
Many-core chips — a case for virtual shared memory
Workshop on Managed Many-Core Systems, pp. 4 pages, Washington, DC, USA, March, 2009
Abstract PDF Rob van Glabbeek and Peter D. Mosses
Preface, special issue on structural operational semantics
Information and Computation, pp. 83-84, Elsevier, 2009
Abstract PDF Peter Baumgartner, Alexander Fuchs, Hans de Nivelle and Cesare Tinelli
Computing finite models by reduction to function-free clause logic
Journal of Applied Logic, Volume 7, Number 1, pp. 58-74, January, 2009
Abstract PDF Taolue Chen, Wan Fokkink and Rob van Glabbeek
On finite bases for weak semantics: Failures versus impossible futures
35th Conference on Current Trends in Theory and Practice of Computer Science, pp. 167-180, Spindleruv Mlyn, Czech Republic , January, 2009
Abstract PDF Gernot Heiser
Hypervisors for consumer electronics
IEEE Consumer Communications and Networking Conference, pp. 1-5, Las Vegas, NV, USA, January, 2009

2008

Abstract PDF Taolue Chen, Wan Fokkink and Rob van Glabbeek
Ready to preorder: The case of weak process semantics
Information Processing Letters, Volume 109, Number 2, pp. 104-111, December, 2008
Abstract PDF Peter Baumgartner, Alexander Fuchs and Cesare Tinelli
ME(LIA) - model evolution with linear integer arithmetic constraints
Proceedings of the 15thInternational Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 258-273, Doha, Qatar, November, 2008
Abstract PDF André Hergenhan and Gernot Heiser
Operating systems technology for converged ECUs
6th Embedded Security in Cars Conference (escar), pp. 3 pages, Hamburg, Germany, November, 2008
Abstract PDF Stefan Petters, Martin Lawitzky, Kevin Elphinstone and Ryan Heffernan
Fitting an EDF based scheduling approach to componentised real(-time) systems
IEEE Real-Time Systems Symposium, Barcelona, Spain, November, 2008
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Characterising testing preorders for finite probabilistic processes
Logical Methods in Computer Science, Volume 4, Number 4, pp. 1-33, October, 2008
Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Verified Software: Theories, Tools and Experiments, pp. 99–115, Toronto, Canada , October, 2008
Abstract PDF Rafal Kolanski and Gerwin Klein
Mapped separation logic
Verified Software: Theories, Tools and Experiments, pp. 15-29, Toronto, Canada, October, 2008
Abstract PDF Peter Baumgartner, Alessandro Armando and Gilles Dowek
Automated reasoning - 4th international conference, IJCAR 2008
Volume 5195 in Lecture Notes in Artificial Intelligence, Springer, 2008
Abstract PDF Bernhard Beckert and Gerwin Klein
5th international verification workshop – VERIFY'08
CEUR Workshop Proceedings, 2008
Abstract PDF David Cock
Bitfields and tagged unions in C – verification through automatic generation
VERIFY08, pp. 44-55, Sydney, August, 2008
Abstract PDF David Cock, Gerwin Klein and Thomas Sewell
Secure microkernels, state monads and scalable refinement
Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, pp. 167-182, Montreal, Canada, August, 2008
Abstract PDF Joshua LeVasseur, Volkmar Uhlig, Yaowei Yang, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser
Pre-virtualization: Soft layering for virtual machines
Asia-Pacific Computer Systems Architecture Conference, pp. 1-9, Hsinchu, Taiwan, August, 2008
Best Paper Award!
Abstract PDF Konrad Slind and Michael Norrish
A brief overview of HOL4
International Conference on Theorem Proving in Higher Order Logics, pp. 28-32, Montréal, Canada, August, 2008
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
On synchronous and asynchronous interaction in distributed systems
33nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2008), pp. 16-35, Torun, Poland, August, 2008
Abstract PDF Ralf Huuck, Gerwin Klein and Bastian Schlich
Proceedings of the 3rd international workshop on systems software verification (SSV 2008)
Volume 217 in ENTCS, Elsevier, 2008
Abstract PDF Rafal Kolanski
A logic for virtual memory
Systems Software Verification, pp. 61-77, Sydney, Australia, July, 2008
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
Symmetric and asymmetric asynchronous interaction
First Interaction and Concurrency Experience (ICE'08): Synchronous and Asynchronous Interactions in Concurrent Distributed Systems, pp. 5-22, Reykjavik, Iceland, July, 2008
Best student/young researcher paper.
Abstract PDF Rob van Glabbeek and Bas Ploeger
Correcting a space-efficient simulation algorithm
20th International Conference on Computer Aided Verification, CAV 2008, pp. 517-529, Princeton, USA, July, 2008
Abstract PDF Rob van Glabbeek and Bas Ploeger
Five determinisation algorithms
13th International Conference on Implementation and Application of Automata, pp. 161-170, San Francisco, July, 2008
Abstract PDF Tom Ridge, Michael Norrish and Peter Sewell
A rigorous approach to networking: TCP, from implementation to protocol to service
International Symposium on Formal Methods (FM), pp. 294–309, Turku, Finland, May, 2008
Abstract PDF Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone
Kernel design for isolation and assurance of physical memory
1st Workshop on Isolation and Integration in Embedded Systems, Glasgow, UK, April, 2008
Abstract PDF Gernot Heiser
The role of virtualization in embedded systems
Workshop on Isolation and Integration in Embedded Systems, pp. 11-16, Glasgow, UK, April, 2008
Abstract PDF Peter Baumgartner and Cesare Tinelli
The model evolution calculus as a first-order DPLL method
Artificial Intelligence, Volume 172, Number 4-5, pp. 591-632, January, 2008
Abstract PDF Ihor Kuz and Yan Liu
Extending the capabilities of component models for embedded systems
Third International Conference on the Quality of Software-Architectures (QoSA), pp. 182-196, Boston, MA, USA, January, 2008

2007

Abstract PDF Kevin Elphinstone, David Greenaway and Sergio Ruocco
Lazy queueing and direct process switch — merit or myths?
Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 69-77, Pisa, Italy, December, 2007
Abstract PDF Gernot Heiser
Your system is secure? Prove it!
USENIX ;login:, Volume 32(6), pp. 35–38, December, 2007
Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3-11, December, 2007
Abstract PDF Stefan Petters, Patryk Zadarnowski and Gernot Heiser
Measurements or static analysis or both?
Workshop on Worst-Case Execution-Time Analysis, pp. 5-11, Pisa, Italy, December, 2007
Abstract PDF Dave Snowdon, Godfrey van der Linden, Stefan Petters and Gernot Heiser
Accurate run-time prediction of performance degradation under frequency scaling
Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 58-64, Pisa, Italy, December, 2007
Abstract PDF Dave Snowdon, Stefan Petters and Gernot Heiser
Accurate on-line prediction of processor and memory energy usage under voltage scaling
International Conference on Embedded Software, pp. 84-93, Salzburg, Austria, December, 2007
Abstract PDF Michael Norrish
A formal semantics for c++
Technical Report, NICTA, November, 2007
Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 2007
Abstract PDF Leonid Ryzhyk, Ihor Kuz and Gernot Heiser
Formalising device driver interfaces
Workshop on Programming Languages and Operating Systems (PLOS), pp. 5, Stevenson, WA, USA, October, 2007
Abstract PDF Rob van Glabbeek and Matthew Hennessy
Preface, proceedings of the 4th workshop on structural operational semantics
Electronic Notes in Theoretical Computer Science, pp. 1-3, Elsevier, 2007
Abstract PDF Michael Norrish and René Vestergaard
Proof pearl: de bruijn terms really do work
International Conference on Theorem Proving in Higher Order Logics, pp. 207-222, Kaiserslautern, September, 2007
Abstract PDF Peter Baumgartner
Logical engineering with instance-based methods
CADE-21 - The 21st International Conference on Automated Deduction, pp. 404-409, July, 2007
Abstract PDF Peter Baumgartner, Ulrich Furbach and Bjoern Pelzer
Hyper tableaux with equality
CADE-21 – The 21st International Conference on Automated Deduction, pp. 492-507, Bremen, Germany, July, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang
Characterising testing preorders for finite probabilistic processes
22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 313-322, Wroclaw, Poland, July, 2007
Abstract PDF Jia Meng, Lawrence C. Paulson and Gerwin Klein
A termination checker for isabelle hoare logic
International Verification Workshop, pp. 104-118, Bremen, Germany, July, 2007
Abstract PDF Leonid Ryzhyk, Timothy Bourke and Ihor Kuz
Reliable device drivers require well-defined protocols
Workshop on Hot Topics in System Dependability, pp. Article 3, Edinburgh, UK, June, 2007
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems, pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF Timothy Roscoe, Kevin Elphinstone and Gernot Heiser
Hype and virtue
Workshop on Hot Topics in Operating Systems, pp. 19-24, San Diego, USA, May, 2007
Abstract PDF Rob van Glabbeek and Peter D. Mosses
Preface, proceedings of the 3rd workshop on structural operational semantics
Electronic Notes in Theoretical Computer Science, pp. 1-2, Elsevier, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang
Remarks on testing probabilistic processes
Electronic Notes in Theoretical Computer Science, Volume 172, Number , pp. 359-397, April, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang
Scalar outcomes suffice for finitary probabilistic testing
16th European Symposium on Programming, ESOP 2007, pp. 363-378, Braga, Portugal, March, 2007
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97-108, Nice, France, January, 2007

2006

Abstract PDF Kevin Elphinstone and Scott Brandt
Proceedings of the 2007 workshop on operating system platforms for embedded real-time applications
Technical Report, NICTA, July, 2006
Abstract PDF Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55–66, Charleston, South Carolina, USA, January, 2006

2005

Abstract PDF Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets
ACM Conference on Communications, pp. 265–276, Philadelphia, August, 2005

2004

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

2003

Abstract
Slides
PDF Michael Norrish
Complete integer decision procedures as derived rules in HOL
International Conference on Theorem Proving in Higher Order Logics, pp. 71-86, Rome, September, 2003

Other technical reports of the School of Computer Science & Engineering.

Non-Data61/NICTA Publications

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

2009

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

2008

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

2006

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

2005

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

2004

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

2003

Abstract PDF Peter Chubb
Where's all the time going? Microstate accounting in Linux 2.5
AUUG Winter Conference, Melbourne, Australia, September, 2003
Abstract PDF Andreas Haeberlen and Kevin Elphinstone
User-level management of kernel memory
Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
Abstract PDF Adam Wiggins
A survey on the interaction between caching, translation and protection
Technical Report UNSW-CSE-TR-0321, School of Computer Science and Engineering, August, 2003

2002

Abstract PS Peter Chubb
Terabytes on a diet
AUUG Winter Conference, Melbourne, Australia, September, 2002
Abstract PDF Shane Stephens and Gernot Heiser
Fault tolerance and avoidance in biomedical systems
Proceedings of the 10th SIGOPS European Workshop, St Emilion, France, September, 2002
Abstract PDF Peter Chubb
YOU ARE LOST in a maze of BitKeeper repositories — all almost the same
Australian Open Source Symposium, Sydney, Australia, July, 2002
Abstract PS Simon Winwood, Yefim Shuf and Hubertus Franke
Multiple page size support in the Linux kernel
Ottawa Linux Symposium, Ottawa, Canada, June, 2002
Abstract PDF Daniel Potts, Simon Winwood and Gernot Heiser
Design and implementation of the L4 microkernel for Alpha multiprocessors
Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002
Abstract PS Kingsley Cheung and Gernot Heiser
A resource management framework for priority-based physical-memory allocation
Proceedings of the 7th Asia-Pacific Computer Systems Architecture Conference, Monash University, Melbourne, Australia, January, 2002
Abstract PDF Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser
Performance of address-space multiplexing on the Pentium
Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002

2001

Abstract PDF Gernot Heiser
Dealing with TLB tags
International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PS Chris Szmajda
Calypso: A portable translation layer
International Workshop on Microkernels for Embedded Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PDF Antony Edwards and Gernot Heiser
Secure OS extensibility needn't cost an arm and a leg
Proceedings of the 8th Workshop on Hot Topics in Operating Systems, pp. 168, Schloss Elmau, Germany, May, 2001
Abstract PDF Antony Edwards and Gernot Heiser
A component architecture for system extensibility
Technical Report UNSW-CSE-TR-0103, School of Computer Science and Engineering, March, 2001
Abstract PDF Daniel Potts, Simon Winwood and Gernot Heiser
L4 reference manual: Alpha 21x64
Technical Report UNSW-CSE-TR-0104, School of Computer Science and Engineering, March, 2001
Abstract PS Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller
The SawMill framework for VM diversity
Proceedings of the 6th Asia-Pacific Computer Systems Architecture Conference, pp. 3–10, Gold Coast, Australia, January, 2001
Abstract PS Alan Au and Gernot Heiser
Enhancing IA64 memory management
2nd Linux.conf.au, Sydney, Australia, January, 2001
Abstract PDF Antony Edwards and Gernot Heiser
Components + Security = OS Extensibility
Proceedings of the 6th Asia-Pacific Computer Systems Architecture Conference, pp. 27–34, Gold Coast, Australia, January, 2001
Abstract PDF Gernot Heiser
Inside L4/MIPS: Anatomy of a high-performance microkernel
Sydney, Australia, January, 2001

2000

Abstract PS Adam Wiggins and Gernot Heiser
Fast address-space switching on the StrongARM SA-1100 processor
Proceedings of the 5th Australasian Computer Architecture Conference, pp. 97–104, Canberra, Australia, January, 2000
Abstract PDF Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther
The Sawmill multiserver approach
Proceedings of the 9th SIGOPS European Workshop, pp. 109–114, Kolding, Denmark, 2000

1999

Abstract PS Luke Deller and Gernot Heiser
Linking programs in a single address space
Proceedings of the 1999 USENIX Annual Technical Conference, pp. 283–294, Monterey, Ca, USA, June, 1999
Abstract PS Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual: MIPS R4x00, version 1.11, kernel version 79
Sydney, Australia, May, 1999
Abstract PS Kevin Elphinstone
Virtual memory in a 64-bit microkernel
PhD Thesis, UNSW, Sydney, Australia, March, 1999
Abstract PDF Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko and Yoonho Park
Flexible access control using IPC redirection
Proceedings of the 7th Workshop on Hot Topics in Operating Systems, Rio Rico, AZ, USA, March, 1999
Abstract PS Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
Page tables for 64-bit computer systems
Proceedings of the 4th Australasian Computer Architecture Conference, pp. 211-226, Auckland, New Zealand, January, 1999

1998

Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
Page tables for 64-bit computer systems
Technical Report UNSW-CSE-TR-9804, School of Computer Science and Engineering, August, 1998
Abstract PS Gernot Heiser, Kevin Elphinstone, Jerry Vochteloo, Stephen Russell and Jochen Liedtke
The Mungi single-address-space operating system
Software: Practice and Experience, Volume 28, Number 9, pp. 901–928, July, 1998
Abstract PS Jerry Vochteloo
Design, implementation and performance of protection in the Mungi single-address-space operating system
PhD Thesis, UNSW, Sydney, Australia, July, 1998
Abstract PDF Alan Au and Gernot Heiser
L4 User Manual — version 1.0
Technical Report UNSW-CSE-TR-9801, School of Computer Science and Engineering, April, 1998
Abstract PS Gernot Heiser, Fondy Lam and Stephen Russell
Resource management in the Mungi single-address-space operating system
Proceedings of the 21st Australasian Computer Science Conference (ACSC), pp. 417–428, Perth, Australia, February, 1998

1997

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

1996

Abstract PS Jerry Vochteloo, Kevin Elphinstone, Stephen Russell and Gernot Heiser
Protection domain extensions in Mungi
Proceedings of the 5th IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 161–165, Seattle, WA, USA, October, 1996
Abstract PS Jinsong Ouyang and Gernot Heiser
Libra: A library for reliable distributed applications
International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 801–810, Sunnyvale, CA, USA, August, 1996
Abstract PS Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke
Supporting persistent object systems in a single address space
Proceedings of the 7th International Workshop on Persistent Object Systems (POS), pp. 111–119, Cape May, NJ, USA, May, 1996
Abstract PDF Jochen Liedtke and Kevin Elphinstone
Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization
ACM Operating Systems Review, Volume 30, Number 1, pp. 4–15, January, 1996

1995

Abstract PDF Jochen Liedtke and Kevin Elphinstone
Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization
Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, November, 1995
Abstract PDF Tim Wilkinson, Kevin Murray, Stephen Russell, Gernot Heiser and Jochen Liedtke
Single address space operating systems
Technical Report UNSW-CSE-TR-9504, UNSW, November, 1995
Abstract PS Jinsong Ouyang and Gernot Heiser
Checkpointing and recovery for distributed shared memory applications
Proceedings of the 4th IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 191–9, Lund, Sweden, August, 1995

1994

Abstract PDF Kevin Elphinstone, Stephen Russell and Gernot Heiser
Issues in implementing virtual memory
Technical Report UNSW-CSE-TR-9411, School of Computer Science and Engineering, September, 1994
Abstract PS Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo
Mungi: A distributed single-address-space operating system
Proceedings of the 17th Australasian Computer Science Conference (ACSC), pp. 271–80, Christchurch, New Zealand, January, 1994

1993

Abstract PS Jerry Vochteloo, Stephen Russell and Gernot Heiser
Capability-based protection in the Mungi operating system
Proceedings of the 3rd IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 108–15, Asheville, NC, USA, December, 1993
Abstract PDF Kevin Elphinstone
Address space management issues in the Mungi operating system
Technical Report UNSW-CSE-TR-9312, School of Computer Science and Engineering, November, 1993
Abstract PDF Gernot Heiser, Kevin Elphinstone, Stephen Russell and Jerry Vochteloo
Mungi: A distributed single address-space operating system
Technical Report UNSW-CSE-TR-9314, School of Computer Science and Engineering, November, 1993
Abstract PDF Gernot Heiser, Kevin Elphinstone, Stephen Russell and Graham R. Hellestrand
A distributed single address space system supporting persistence
Technical Report UNSW-CSE-TR-9302, UNSW, March, 1993

1992

Abstract PS Stephen Russell, Alan Skea, Kevin Elphinstone, Gernot Heiser, Keith Burston, Ian Gorton and Graham Hellestrand
Distribution + persistence = global virtual memory
Proceedings of the 2nd IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS), pp. 96–99, Dourdan, France, September, 1992

Post-graduate Student Theses

2016

Abstract PDF Sidney Amani
A methodology for trustworthy file systems
PhD Thesis, CSE, UNSW, Sydney, Australia, August, 2016
Abstract PDF Matthew Fernandez
Formal verification of a component platform
PhD Thesis, UNSW Computer Science & Engineering, Sydney, Australia, July, 2016

2015

Abstract PDF Mustafa Hashmi
Evaluating business process compliance management frameworks
PhD Thesis, Business ProcessManagement Discipline Information Systems School Queensland University of Technology (QUT), Brisbane, Australia, December, 2015
Abstract PDF David Greenaway
Automated proof-producing abstraction of c code
PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015

2014

Abstract
Slides
PDF Francesco Olivieri
Compliance by design: Synthesis of business processes by declarative specifications
PhD Thesis, Griffith University/Institute for Integrated and Intelligent Systems, Brisbane, Australia, December, 2014
Abstract PDF Simone Scannapieco
Towards a methodology for business process revision under norm and outcome compliance
PhD Thesis, Institute for Integrated and Intelligent Systems, Griffith Sciences Group, Griffith University and the Department of Computer Science, University of Verona, Brisbane, Australia and Verona, Italy, December, 2014
Abstract PDF Andrew Boyton
Secure architectures on a verified microkernel
PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014
Abstract PDF David Cock
Leakage in trustworthy systems
PhD Thesis, UNSW, Sydney, Australia, August, 2014
Abstract
Slides
PDF Badiul Islam
PRIVACY BY DESIGN FOR SOCIAL NETWORKS
PhD Thesis, Queensland University of Technology/Information Systems, Brisbane, Australia, May, 2014
This research has established a new privacy framework, privacy model, and privacy architecture to create more transparent privacy for social networking users. The architecture is designed into three levels: Business, Data, and Technology, which is based on The Open Group Architecture Framework (TOGAF®). This framework and architecture provides a novel platform for investigating privacy in Social Networks (SNs). This approach mitigates many current SN privacy issues, and leads to a more controlled form of privacy assessment. Ultimately, more privacy will encourage more connections between people across SN services.

2013

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

2011

Abstract PDF Aditi Barthwal
A formalisation of the theory of context-free languages in higher order logic
PhD Thesis, College of Engineering and Computer Science, ANU, Canberra, Australia, July, 2011
Abstract PDF Rafal Kolanski
Verification of programs in virtual memory using separation logic
PhD Thesis, UNSW, Sydney, Australia, July, 2011
Abstract PDF Etienne Le Sueur
An analysis of the effectiveness of energy management on modern computer processors
MSc Thesis, UNSW, Sydney, Australia, June, 2011
Abstract PDF Nicholas FitzRoy-Dale
Architecture optimisation
PhD Thesis, UNSW, Sydney, Australia, March, 2011

2010

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

2009

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

2008

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

2007

Abstract to be published Jacky Keung
Providing statistical inferences to case-based software cost estimation
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2007
Abstract PDF Luke Macpherson
Performing under overload
PhD Thesis, UNSW, Sydney, Australia, September, 2007
Abstract PDF Andrew Baumann
Dynamic update for operating systems
PhD Thesis, UNSW, Sydney, Australia, August, 2007
Abstract to be published Liming Zhu
Software architecture evaluation for framework-based systems
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, May, 2007

2005

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

1999

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

1998

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

2016

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

2011

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

2010

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

2009

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

2008

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

2007

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

2006

Abstract PDF Clarence Dang
Optimising L4 on Blackfin 533/537: An investigation into a high performance L4 microkernel without virtual memory
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006
Abstract PDF Tom Birch
Performance limits of Darwin on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006

2005

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

2003

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

2002

Abstract PS Andrew Baumann
A thread model for Mungi
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002
Abstract PS Ben Leslie
Mungi device drivers
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002
Abstract PDF David C. Snowdon
Hard- and software framework for the optimisation of Sunswift-II
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002
Abstract PS Harvey Tuch
A comparison of address translation mechanisms for virtually-addressed caches in embedded systems
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2002

2000

Abstract PS Antony Edwards
A component architecture for system extensibility
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000
Abstract PS Simon Winwood
Flexible scheduling mechanisms in L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000
Abstract PDF Patryk Zadarnowski
The design and implementation of an extendible instruction set simulator
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2000

1999

Abstract PS Luke Deller
Loading and debugging tasks in SawMill
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS Vincent Jayawardene
An intensional engine on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS Daniel Potts
L4 on uni- and multiprocessor Alpha
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS Cristan Szmajda
A new virtual memory implementation for L4/MIPS
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999
Abstract PS Adam Wiggins
The design and implementation of the L4 microkernel on the StrongARM SA-1100
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 1999