Skip to main content

Matthew Fernandez

Matthew Fernandez
PhD Student

Research Interests

Matthew's research interests are in the application of formal methods to large software systems, and in componentised systems and proofs.

Contact Details

Phone: +61 2 8306 0784
Email:Matthew.Fernandez@nicta.com.au

More contact information is available at the Contact page.

Photo of Matthew Fernandez

Publication List

Projects

Past

Matthew is a PhD student in the Trustworthy Systems team. His current research focus is on verifying a component platform for use in the development of microkernel-based systems. He is the lead maintainer of the CAmkES component platform and its formal model in Isabelle/HOL. He also works on maintenance of the seL4 microkernel.

His other research interests include kernel design, security, correctness and compiler implementation. His side projects include work with the CompCert C compiler and tools for configuring separation kernels.

Collaborations

Matthew has worked with several other academic and industry organisations including:

Career Summary

Prior to joining NICTA, Matthew worked for several Not-For-Profit organisations and service providers. These roles involved application development, database design and system administration on a variety of platforms.

Qualifications

  • Bachelor of Advanced Science (Honours)
  • Bachelor of Arts

Recognition and Awards

  • UNSW Three Minute Thesis Competition finalist (2013)
  • UNSW Advanced Operating Systems Alumni Prize (2011)

Publications

Data61 Papers

2016

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

NICTA Papers

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 Rebekah Leslie-Hurd, Dror Caspi and Matthew Fernandez
Verifying linearizability of intel software guard extensions
International Conference on Computer Aided Verification, pp. 144–159, San Francisco, CA, USA, 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

2014

Abstract PDF Matthew Fernandez and Rebekah Leslie-Hurd
Accordion: An EDSL for hardware instruction set extensions
talk at Domain-Specific Language Design and Implementation, Portland, OR, USA, October, 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 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 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

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 Matthew Fernandez, Gerwin Klein and Ihor Kuz
Microkernel verification down to assembly
Poster presented at EuroSys 2012, April, 2012

Non-NICTA Papers

2016

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