June Andronick
Principal Researcher; Con-joint Associate Professor, UNSW
Research Interests
June's 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
| Phone: | +61 2 9490 5881 |
|---|---|
| Email: | June.Andronick@data61.csiro.au |
| Web: | http:/ |
More contact information is available at the Contact page.
June's current projects include formally verifying eChronos, a small real-time interruptible OS, and modelling a multicore version of seL4. Previously, she has worked on the functional correctness proof of seL4; on measuring and estimating proof effort; and on the DARPA-funded SMACCM project.
Projects
Current |
Past |
Career Summary
Prior to joining Data61/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 Lecturer at the School of Computer Science and Engineering of UNSW.
Program Committees and Editorial Boards
- 2018: CPP'2018 (chair)
- 2017: POPL'2017 (ERC) , SNAPL'2017 , JFLA'2017
- 2016: SecDev'2016 , CSF'2016 , PAAR'2016 , VSTTE'2016 , SER&IP'2016
- 2015: FCS'2015, CPP'2015, SER&IP'2015
- 2014: ICSE'2014 - SEIP track, SER&IP'2014
- 2013: ICSE'2013 - SEIP track
- 2012: BYTECODE'2012
- 2009: SSV'2009, BYTECODE'2009
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
- Google Scholar profile
- Best Papers
- Data61 Papers (To appear, 2017, 2016)
- NICTA Papers (2015, 2014, 2013, 2012, 2011, 2010, 2009)
- Non-NICTA Papers (2008, 2006, 2005, 2003)
- Research Theses Supervised
Best Papers
|
 |
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser Comprehensive formal verification of an OS microkernel ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014 |
|
|
|
Thomas Sewell, 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 |
|
 |
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 |
Data61 Papers
To appear
|
|
|
Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez Formally verified software in the real world Communications of the ACM |
2017
|
|
|
Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk and Toby Murray Provably trustworthy systems Philosophical Transactions of the Royal SocietyA, Volume 375, pp. 1-23, September, 2017 |
|
|
|
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 |
2016
|
|
|
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah Proof of OS scheduling behavior in the presence of interrupt-induced concurrency International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016 |
NICTA Papers
2015
|
|
|
June Andronick, Corey Lewis and Carroll Morgan Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015 |
|
|
|
Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of a component platform Technical Report, NICTA and UNSW, August, 2015 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick Towards a verified component platform Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013 |
|
|
|
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 |
|
|
|
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
|
|
|
June Andronick, Andrew Boyton and Gerwin Klein Final report for AOARD grant #FA2386-11-1-4070, formal system verification — extension Technical Report, NICTA, October, 2012 |
|
|
|
June Andronick, Gerwin Klein and Toby Murray Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105 Technical Report, NICTA, October, 2012 |
|
|
|
June Andronick and Gerwin Klein Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022 Technical Report, NICTA, August, 2012 |
|
|
|
David Greenaway, June Andronick and Gerwin Klein Bridging the gap: Automatic verified abstraction of C International Conference on Interactive Theorem Proving, pp. 99–115, Princeton, New Jersey, USA, August, 2012 |
|
|
|
June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, Jason Zhang and Liming Zhu Large-scale formal verification in practice: A process perspective International Conference on Software Engineering, pp. 1002–1011, Zurich, Switzerland, June, 2012 |
|
|
|
Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski Simulation modeling of a large scale formal verification process International Conference on Software and Systems Process, pp. 3–12, Zurich, Switzerland, June, 2012 |
|
|
|
June Andronick, Gerwin Klein and Andrew Boyton Formal system verification — extension, AOARD 114070 Technical Report, NICTA, May, 2012 |
2011
|
|
|
June Andronick, Gerwin Klein and Toby Murray Formal system verification for trustworthy embedded systems, final report option 1 — AOARD 104105 Technical Report, NICTA, November, 2011 |
|
|
|
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 |
|
|
|
June Andronick and Gerwin Klein Formal system verification for trustworthy embedded systems, final report AOARD 094160 Technical Report, NICTA, April, 2011 |
2010
|
|
|
June Andronick From a proven correct microkernel to trustworthy large systems International Conference on Formal Verification of Object-Oriented Software, pp. 1–9, Paris, December, 2010 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
Non-NICTA Papers
2008
|
|
|
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
|
|
|
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 |
|
|
|
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
|
|
|
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
|
|
|
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 |
Research Theses Supervised
2016
|
|
|
Matthew Fernandez Formal verification of a component platform PhD Thesis, UNSW Computer Science & Engineering, Sydney, Australia, July, 2016 |
2014
|
|
|
Andrew Boyton Secure architectures on a verified microkernel PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014 |
