Skip to main content

David Greenaway

David Greenaway
Researcher

Research Interests

David is currently researching how formal verification of low-level C code can be simplified, using automatic specification abstraction in Isabelle/HOL.

Contact Details

Phone: +61 2 8306 0564
Web:http://www.davidgreenaway.com/

More contact information is available at the Contact page.

Photo of David Greenaway

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.

NICTA Papers

2014

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

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
Proceedings of the 15th International Conference on Formal Engineering Methods, pp. 70-85, Queenstown, New Zealand, October, 2013

2012

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

2010

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

2007

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

Served by Apache on Linux on seL4.