capDL: a language for describing capability-based systems. - Ihor Kuz; Gerwin Klein; Corey Lewis; Adam Walker (ApSys, 2010)

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

Formal specifications better than function points for code sizing. - Mark Staples; Rafal Kolanski; Gerwin Klein; Corey Lewis; June Andronick; Toby C. Murray; D. Ross Jeffery; Len Bass (ICSE, 2013)

seL4: From General Purpose to a Proof of Information Flow Enforcement. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Timothy Bourke; Sean Seefried; Corey Lewis; Xin Gao; Gerwin Klein (IEEE Symposium on Security and Privacy, 2013)

Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System. - June Andronick; Corey Lewis; Carroll Morgan (MARS, 2015)

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. - June Andronick; Corey Lewis; Daniel Matichuk; Carroll Morgan; Christine Rizkallah (ITP, 2016)

COMPLX: A Verification Framework for Concurrent Imperative Programs. - Sidney Amani; June Andronick; Maksym Bortin; Corey Lewis; Christine Rizkallah; Joseph Tuong (Arch. Formal Proofs, 2016)

Finite Machine Word Library. - Joel Beeren; Matthew Fernandez; Xin Gao; Gerwin Klein; Rafal Kolanski; Japheth Lim; Corey Lewis; Daniel Matichuk; Thomas Sewell (Arch. Formal Proofs, 2016)

Cyberassured Systems Engineering at Scale. - Darren D. Cofer; Isaac Amundson; Junaid Babar; David S. Hardin; Konrad Slind; Perry Alexander; John Hatcliff; Robby; Gerwin Klein; Corey Lewis; Eric Mercer; John Shackleton (IEEE Secur. Priv., 2022)