Trustworthy Systems

June Andronick
Adjunct Professor; Founder and CEO at Proofcraft

Research Interests

June had joined the Trustworthy Systems research group in 2008 (in NICTA), and led the group from end of 2016 to end of 2020. Her main research interest is in formal verification and certification of software systems, more precisely in formal proof of correctness and security properties of programs using interactive theorem proving, as well as concurrency reasoning, targeting interruptible and multicore systems.

Contact Details

Email:june.andronick@unsw.edu.au

More contact information is available at the Contact page.

Photo of June Andronick

Publication List

Projects

Past

Career Summary

Prior to joining NICTA, June worked more than 6 years in the Formal Methods team of Gemalto, the worldwide leading smart card manufacturer. First as a PhD student within the company, then as a researcher, June worked on formal verification and certification of smart card embedded programs.

Qualifications

June holds a PhD in Computer Science of the University of Paris-Sud, France, that she defended in March 2006.

Affiliations

June is Conjoint Professor at the School of Computer Science and Engineering of UNSW.

Recognition and Awards

  • 2019: ACM SIGOPS Hall of Fame Award.
  • 2011: MIT TR35, Top 35 young innovators in 2011.
  • 2011 (with L4.verified team): MIT TR10, Top 10 emerging technologies in 2011.
  • 2011 (with L4.verified team): Finalist for Australian Museum Eureka Prize in Computer Science.
  • 2009 (with L4.verfied team): SOSP'09 Best Paper Award.

Publications

Best Papers

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 Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Best Paper Award
Hall of Fame Award


Trustworthy Systems Group Papers

2020

Abstract PDF Gernot Heiser, Gerwin Klein and June Andronick
seL4 in Australia: From research to real-world trustworthy systems
Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020

2019

Abstract to be published June Andronick
Successes in deployed verified software (and insights on key social factors)
FM 2019: Formal Methods – The Next 30 Years, pp. 11-17, Porto, Portugal, October, 2019

2018

Abstract PDF Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart
A formal approach to constructing secure air vehicle software
IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018
Abstract PDF Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018

2017

Abstract PDF June Andronick
From Hoare logic to Owicki-Gries and rely-guarantee for interruptible eChronos and multicore seL4
International Colloquium on Theoretical Aspects of Computing (ICTAC), pp. XIII-XV, Hanoi, Vietnam, October, 2017
Abstract PDF Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor
Provably trustworthy systems
Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017
Abstract PDF June Andronick
Reasoning about concurrency in high-assurance, high-performance software systems
International Conference on Automated Deduction, pp. 1–7, Gothenburg, August, 2017
Abstract PDF Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joey Tuong
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138–150, Paris, France, January, 2017

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

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 Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of a component platform
Technical Report, NICTA and UNSW, August, 2015
Abstract
Slides
PDF Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of RPC stub code
International Symposium on Formal Methods (FM), pp. 273–290, Oslo, Norway, June, 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 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

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

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
Slides
PDF Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell
Formally verified system initialisation
International Conference on Formal Engineering Methods, pp. 70–85, Queenstown, New Zealand, October, 2013
Abstract 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

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 June Andronick and Gerwin Klein
Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022
Technical Report, NICTA, 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 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

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 Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
Abstract PDF June Andronick and Gerwin Klein
Formal system verification for trustworthy embedded systems, final report AOARD 094160
Technical Report, NICTA, April, 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 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 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

2009

Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Best Paper Award
Hall of Fame Award
Abstract PDF 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

Papers without TS Affiliation

2008

Abstract PDF June Andronick and Quang-Huy Nguyen
Certifying an Embedded Remote Method Invocation Protocol
Proceedings of the ACM Symposium on Applied Computing, pp. 352–359, Fortaleza, Ceara, Brazil, March, 2008

2006

Abstract PDF June Andronick
Formally Proved Anti-tearing Properties of Embedded C Code
Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 129–136, Paphos, Cyprus, November, 2006
Abstract PDF June Andronick
Modélisation et Vérification Formelles de Systèmes Embarqués dans les Cartes à Microprocesseur – Plate-Forme Java Card et Système d'Exploitation
PhD Thesis, Université Paris-Sud, 2006

2005

Abstract PDF June Andronick, Boutheina Chetali and Christine Paulin-Mohring
Formal Verification of Security Properties of Smart Card Embedded Source Code
International Symposium on Formal Methods (FM), pp. 302–317, Newcastle, UK, July, 2005

2003

Abstract PDF June Andronick, Boutheina Chetali and Olivier Ly
Using Coq to Verify Java Card Applet Isolation Properties
International Conference on Theorem Proving in Higher Order Logics, pp. 335–351, Rome, Italy, September, 2003

Research Theses Supervised

2016

Abstract PDF Matthew Fernandez
Formal verification of a component platform
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016

2015

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

2014

Abstract PDF Andrew Boyton
Secure architectures on a verified microkernel
PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014