June Andronick

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