June Andronick
Senior Researcher; Conjoint Senior Lecturer, UNSW

Photo of %s

Contact Details

Phone: +61 2 8306 0581
Email:June.Andronick@nicta.com.au

More contact information is available at the Contact page.

Research Interests

June's main research interest is in formal verification and certification of software systems, and more precisely in formal proof of correctness and security properties of programs using interactive theorem proving.

Publication List

Projects

Current

June is part of the formal verification team of NICTA's Software Systems Research Group (SSRG). She was previously involved in the L4.verified project, contributing to the proof of the functional correctness of the seL4 kernel. She's now part of the Trustworthy Systems project, focusing on building a framework to formally prove security properties for systems over a million lines of code.

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 Master intern, then as a PhD student within the company, and finally as a research engineer, 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 Lecturer at the School of Computer Science and Engineering of UNSW.

Recognition and Awards

  • 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
Proceedings of the 2nd 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!


NICTA Papers

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, 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. 6, 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
Proceedings of the 15th 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
Proceedings of the 3rd International Conference on Interactive Theorem Proving, pp. 99-115, Princeton, New Jersey, August, 2012
The final publication is available at www.springerlink.com
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
Proceedings of the 2nd 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, David Greenaway and Kevin Elphinstone
Towards proving security in the presence of large untrusted components
Proceedings of the 5th Systems Software Verification, Vancouver, Canada, October, 2010
Abstract PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
Proceedings of the 5th ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3–9, Chicago, IL, USA, October, 2010
Invited paper
Abstract PDF June Andronick
From a proven correct microkernel to trustworthy large systems
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), pp. 1–9, Paris, France, 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

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!
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
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, August, 2009

Non-NICTA Papers

2008

Abstract PDF June Andronick and Quang-Huy Nguyen
Certifying an Embedded Remote Method Invocation Protocol
Proceedings of the 23rd 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
Proceedings of the 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
Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics, pp. 335–351, Rome, Italy, September, 2003

Served by Apache on Linux on seL4