Towards Proving Security in the Presence of Large Untrusted Components. - June Andronick; David Greenaway; Kevin Elphinstone (SSV, 2010)

Bridging the Gap: Automatic Verified Abstraction of C. - David Greenaway; June Andronick; Gerwin Klein (ITP, 2012)

Formally Verified System Initialisation. - Andrew Boyton; June Andronick; Callum Bannister; Matthew Fernandez; Xin Gao; David Greenaway; Gerwin Klein; Corey Lewis; Thomas Sewell (ICFEM, 2013)

Don't sweat the small stuff: formal verification of C code without the pain. - David Greenaway; Japheth Lim; June Andronick; Gerwin Klein (PLDI, 2014)

Automated proof-producing abstraction of C code. - David Greenaway (2014)

A Learning-Based Fact Selector for Isabelle/HOL. - Jasmin Christian Blanchette; David Greenaway; Cezary Kaliszyk; Daniel Kühlwein; Josef Urban (J. Autom. Reason., 2016)

AutoCorres2. - Matthew Brecknell; David Greenaway; Johannes Hölzl; Fabian Immler; Gerwin Klein; Rafal Kolanski; Japheth Lim; Michael Norrish; Norbert Schirmer; Salomon Sickert; Thomas Sewell; Harvey Tuch; et al. (Arch. Formal Proofs, 2024)