Using Coq to Verify Java Card Applet Isolation Properties. - June Andronick; Boutheina Chetali; Olivier Ly (TPHOLs, 2003)

Formal Verification of Security Properties of Smart Card Embedded Source Code. - June Andronick; Boutheina Chetali; Christine Paulin-Mohring (FM, 2005)

Formally Proved Anti-tearing Properties of Embedded C Code. - June Andronick (ISoLA, 2006)

Certifying an embedded remote method invocation protocol. - June Andronick; Quang Huy Nguyen 002 (SAC, 2008)

seL4: formal verification of an OS kernel. - Gerwin Klein; Kevin Elphinstone; Gernot Heiser; June Andronick; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (SOSP, 2009)

Mind the Gap. - Simon Winwood; Gerwin Klein; Thomas Sewell; June Andronick; David A. Cock; Michael Norrish (TPHOLs, 2009)

The road to trustworthy systems. - Gernot Heiser; June Andronick; Kevin Elphinstone; Gerwin Klein; Ihor Kuz; Leonid Ryzhyk (STC@CCS, 2010)

From a Proven Correct Microkernel to Trustworthy Large Systems. - June Andronick (FoVeOOS, 2010)

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

seL4: formal verification of an operating-system kernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (Commun. ACM, 2010)

seL4 Enforces Integrity. - Thomas Sewell; Simon Winwood; Peter Gammie; Toby C. Murray; June Andronick; Gerwin Klein (ITP, 2011)

Large-scale formal verification in practice: A process perspective. - June Andronick; D. Ross Jeffery; Gerwin Klein; Rafal Kolanski; Mark Staples; He Zhang 001; Liming Zhu 001 (ICSE, 2012)

Simulation modeling of a large-scale formal verification process. - He Zhang 001; Gerwin Klein; Mark Staples; June Andronick; Liming Zhu 001; Rafal Kolanski (ICSSP, 2012)

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)

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)

Towards a verified component platform. - Matthew Fernandez; Ihor Kuz; Gerwin Klein; June Andronick (PLOS@SOSP, 2013)

Productivity for proof engineering. - Mark Staples; D. Ross Jeffery; June Andronick; Toby C. Murray; Gerwin Klein; Rafal Kolanski (ESEM, 2014)

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

Comprehensive formal verification of an OS microkernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Toby C. Murray; Thomas Sewell; Rafal Kolanski; Gernot Heiser (ACM Trans. Comput. Syst., 2014)

Automated Verification of RPC Stub Code. - Matthew Fernandez; June Andronick; Gerwin Klein; Ihor Kuz (FM, 2015)

Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. - Daniel Matichuk; Toby C. Murray; June Andronick; D. Ross Jeffery; Gerwin Klein; Mark Staples (ICSE (1), 2015)

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

An empirical research agenda for understanding formal methods productivity. - D. Ross Jeffery; Mark Staples; June Andronick; Gerwin Klein; Toby C. Murray (Inf. Softw. Technol., 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)

Reasoning About Concurrency in High-Assurance, High-Performance Software Systems. - June Andronick (CADE, 2017)

Formally verified software in the real world. - Gerwin Klein; June Andronick; Matthew Fernandez; Ihor Kuz; Toby C. Murray; Gernot Heiser (Commun. ACM, 2018)

A Formal Approach to Constructing Secure Air Vehicle Software. - Darren D. Cofer; Andrew Gacek; John Backes; Michael W. Whalen; Lee Pike; Adam Foltzer; Michal Podhradsky; Gerwin Klein; Ihor Kuz; June Andronick; Gernot Heiser; Douglas Stuart (Computer, 2018)

Successes in Deployed Verified Software (and Insights on Key Social Factors). - June Andronick (FM, 2019)

A Million Lines of Proof About a Moving Target (Invited Talk). - June Andronick (ITP, 2019)

seL4 in Australia: from research to real-world trustworthy systems. - Gernot Heiser; Gerwin Klein; June Andronick (Commun. ACM, 2020)

The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). - June Andronick (CPP, 2022)

The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved. - June Andronick (FMCAD, 2022)