June Andronick

Publication Activity (10 Years)

Years Active: 2003-2022
Publications (10 Years): 15

Top Topics

Software Systems

Formal Verification

Top Venues

Publications

June Andronick
The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved. FMCAD (2022)
June Andronick
The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). CPP (2022)
Gernot Heiser, Gerwin Klein, June Andronick
seL4 in Australia: from research to real-world trustworthy systems. Commun. ACM 63 (4) (2020)
June Andronick
Successes in Deployed Verified Software (and Insights on Key Social Factors). FM (2019)
June Andronick
A Million Lines of Proof About a Moving Target (Invited Talk). ITP (2019)
Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, Gernot Heiser
Formally verified software in the real world. Commun. ACM 61 (10) (2018)
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
A Formal Approach to Constructing Secure Air Vehicle Software. Computer 51 (11) (2018)
June Andronick
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems. CADE (2017)
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong
Complx: a verification framework for concurrent imperative programs. CPP (2017)
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong
COMPLX: A Verification Framework for Concurrent Imperative Programs. Arch. Formal Proofs 2016 (2016)
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. ITP (2016)
Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz
Automated Verification of RPC Stub Code. FM (2015)
June Andronick, Corey Lewis, Carroll Morgan
Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System. MARS (2015)
D. Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein, Toby C. Murray
An empirical research agenda for understanding formal methods productivity. Inf. Softw. Technol. 60 (2015)
Daniel Matichuk, Toby C. Murray, June Andronick, D. Ross Jeffery, Gerwin Klein, Mark Staples
Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. ICSE (1) (2015)
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser
Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32 (1) (2014)
Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski
Productivity for proof engineering. ESEM (2014)
David Greenaway, Japheth Lim, June Andronick, Gerwin Klein
Don't sweat the small stuff: formal verification of C code without the pain. PLDI (2014)
Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby C. Murray, D. Ross Jeffery, Len Bass
Formal specifications better than function points for code sizing. ICSE (2013)
Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell
Formally Verified System Initialisation. ICFEM (2013)
Matthew Fernandez, Ihor Kuz, Gerwin Klein, June Andronick
Towards a verified component platform. PLOS@SOSP (2013)
He Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu, Rafal Kolanski
Simulation modeling of a large-scale formal verification process. ICSSP (2012)
David Greenaway, June Andronick, Gerwin Klein
Bridging the Gap: Automatic Verified Abstraction of C. ITP (2012)
June Andronick, D. Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, Liming Zhu
Large-scale formal verification in practice: A process perspective. ICSE (2012)
Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
seL4 Enforces Integrity. ITP (2011)
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
seL4: formal verification of an operating-system kernel. Commun. ACM 53 (6) (2010)
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz, Leonid Ryzhyk
The road to trustworthy systems. STC@CCS (2010)
June Andronick, David Greenaway, Kevin Elphinstone
Towards Proving Security in the Presence of Large Untrusted Components. SSV (2010)
June Andronick
From a Proven Correct Microkernel to Trustworthy Large Systems. FoVeOOS (2010)
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish
Mind the Gap. TPHOLs (2009)
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
seL4: formal verification of an OS kernel. SOSP (2009)
June Andronick, Quang Huy Nguyen
Certifying an embedded remote method invocation protocol. SAC (2008)
June Andronick
Formally Proved Anti-tearing Properties of Embedded C Code. ISoLA (2006)
June Andronick, Boutheina Chetali, Christine Paulin-Mohring
Formal Verification of Security Properties of Smart Card Embedded Source Code. FM (2005)
June Andronick, Boutheina Chetali, Olivier Ly
Using Coq to Verify Java Card Applet Isolation Properties. TPHOLs (2003)