Trustworthy Systems

David Greenaway
PhD Student

Research Interests

David was researching how formal verification of low-level C code can be simplified, using automatic specification abstraction in Isabelle/HOL. He now works at Google.

Contact Details

Phone: +61 2 8306 0564

More contact information is available at the Contact page.

Photo of David Greenaway

Publication List



David is part of NICTA's Embedded Real-time and Operating Systems (ERTOS) research group.


David holds a Bachelor of Science (Computer Science) with first class honours from the University of New South Wales.


Trustworthy Systems Group Papers


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


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