June Andronick

According to our database1, June Andronick authored at least 32 papers between 2003 and 2020.

Collaborative distances:



In proceedings 
PhD thesis 


Online presence:

On csauthors.net:


seL4 in Australia: from research to real-world trustworthy systems.
Commun. ACM, 2020

A Million Lines of Proof About a Moving Target (Invited Talk).
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Successes in Deployed Verified Software (and Insights on Key Social Factors).
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

A Formal Approach to Constructing Secure Air Vehicle Software.
Computer, 2018

Formally verified software in the real world.
Commun. ACM, 2018

Reasoning About Concurrency in High-Assurance, High-Performance Software Systems.
Proceedings of the Automated Deduction - CADE 26, 2017

COMPLX: A Verification Framework for Concurrent Imperative Programs.
Arch. Formal Proofs, 2016

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

An empirical research agenda for understanding formal methods productivity.
Inf. Softw. Technol., 2015

Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System.
Proceedings of the Proceedings Workshop on Models for Formal Analysis of Real Systems, 2015

Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Automated Verification of RPC Stub Code.
Proceedings of the FM 2015: Formal Methods, 2015

Comprehensive formal verification of an OS microkernel.
ACM Trans. Comput. Syst., 2014

Don't sweat the small stuff: formal verification of C code without the pain.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Productivity for proof engineering.
Proceedings of the 2014 ACM-IEEE International Symposium on Empirical Software Engineering and Measurement, 2014

Towards a verified component platform.
Proceedings of the Seventh Workshop on Programming Languages and Operating Systems, 2013

Formal specifications better than function points for code sizing.
Proceedings of the 35th International Conference on Software Engineering, 2013

Formally Verified System Initialisation.
Proceedings of the Formal Methods and Software Engineering, 2013

Bridging the Gap: Automatic Verified Abstraction of C.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Simulation modeling of a large-scale formal verification process.
Proceedings of the 2012 International Conference on Software and System Process, 2012

Large-scale formal verification in practice: A process perspective.
Proceedings of the 34th International Conference on Software Engineering, 2012

seL4 Enforces Integrity.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

seL4: formal verification of an operating-system kernel.
Commun. ACM, 2010

Towards Proving Security in the Presence of Large Untrusted Components.
Proceedings of the 5th International Workshop on Systems Software Verification, 2010

From a Proven Correct Microkernel to Trustworthy Large Systems.
Proceedings of the Formal Verification of Object-Oriented Software, 2010

The road to trustworthy systems.
Proceedings of the fifth ACM workshop on Scalable trusted computing, 2010

Mind the Gap.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

seL4: formal verification of an OS kernel.
Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

Certifying an embedded remote method invocation protocol.
Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), 2008

Formally Proved Anti-tearing Properties of Embedded C Code.
Proceedings of the Leveraging Applications of Formal Methods, 2006

Formal Verification of Security Properties of Smart Card Embedded Source Code.
Proceedings of the FM 2005: Formal Methods, 2005

Using Coq to Verify Java Card Applet Isolation Properties.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003