David is currently researching how formal verification of low-level C code can be simplified, using automatic specification abstraction in Isabelle/HOL.
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.
|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
||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
|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, David Greenaway and Kevin Elphinstone|
Towards proving security in the presence of large untrusted components
Systems Software Verification, pp. 9, Vancouver, Canada , October, 2010
|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