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
| Email: | davidg@trustworthy.systems |
|---|---|
| Web: | https:/ |
More contact information is available at the Contact page.
Projects
Past |
David is part of NICTA's Embedded Real-time and Operating Systems (ERTOS) research group.
Qualifications
David holds a Bachelor of Science (Computer Science) with first class honours from the University of New South Wales.
Publications
Trustworthy Systems Group Papers
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 (PLDI), pp. 429–439, Edinburgh, UK, June, 2014 |
2013
|
|
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
|
|
|
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 |
2010
|
|
|
June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Systems Software Verification, pp. 9, Vancouver, CA, October, 2010 |
2007
|
|
|
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 |