June Andronick

Affiliations:

NICTA, Australia

According to our database¹, June Andronick authored at least 34 papers between 2003 and 2022.

Collaborative distances:

Dijkstra number² of three.
Erdős number³ of four.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Bibliography

2022

The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved.

[BibT_eX]

[DOI]

June Andronick

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk).

[BibT_eX]

[DOI]

June Andronick

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2020

seL4 in Australia: from research to real-world trustworthy systems.

[BibT_eX]

[DOI]

Gernot Heiser

Gerwin Klein

June Andronick

Commun. ACM, 2020

2019

A Million Lines of Proof About a Moving Target (Invited Talk).

[BibT_eX]

[DOI]

June Andronick

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Successes in Deployed Verified Software (and Insights on Key Social Factors).

[BibT_eX]

[DOI]

June Andronick

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018

A Formal Approach to Constructing Secure Air Vehicle Software.

[BibT_eX]

[DOI]

Computer, 2018

Formally verified software in the real world.

[BibT_eX]

[DOI]

Commun. ACM, 2018

2017

Reasoning About Concurrency in High-Assurance, High-Performance Software Systems.

[BibT_eX]

[DOI]

June Andronick

Proceedings of the Automated Deduction - CADE 26, 2017

2016

COMPLX: A Verification Framework for Concurrent Imperative Programs.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2015

An empirical research agenda for understanding formal methods productivity.

[BibT_eX]

[DOI]

Inf. Softw. Technol., 2015

Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System.

[BibT_eX]

[DOI]

June Andronick

Corey Lewis

Carroll Morgan

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.

[BibT_eX]

[DOI]

Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Automated Verification of RPC Stub Code.

[BibT_eX]

[DOI]

Proceedings of the FM 2015: Formal Methods, 2015

2014

Comprehensive formal verification of an OS microkernel.

[BibT_eX]

[DOI]

ACM Trans. Comput. Syst., 2014

Don't sweat the small stuff: formal verification of C code without the pain.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Productivity for proof engineering.

[BibT_eX]

[DOI]

Proceedings of the 2014 ACM-IEEE International Symposium on Empirical Software Engineering and Measurement, 2014

2013

Towards a verified component platform.

[BibT_eX]

[DOI]

Proceedings of the Seventh Workshop on Programming Languages and Operating Systems, 2013

Formal specifications better than function points for code sizing.

[BibT_eX]

[DOI]

Proceedings of the 35th International Conference on Software Engineering, 2013

Formally Verified System Initialisation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2013

2012

Bridging the Gap: Automatic Verified Abstraction of C.

[BibT_eX]

[DOI]

David Greenaway

June Andronick

Gerwin Klein

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Simulation modeling of a large-scale formal verification process.

[BibT_eX]

[DOI]

Proceedings of the 2012 International Conference on Software and System Process, 2012

Large-scale formal verification in practice: A process perspective.

[BibT_eX]

[DOI]

Proceedings of the 34th International Conference on Software Engineering, 2012

2011

seL4 Enforces Integrity.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

seL4: formal verification of an operating-system kernel.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Towards Proving Security in the Presence of Large Untrusted Components.

[BibT_eX]

[DOI]

June Andronick

David Greenaway

Kevin Elphinstone

Proceedings of the 5th International Workshop on Systems Software Verification, 2010

From a Proven Correct Microkernel to Trustworthy Large Systems.

[BibT_eX]

[DOI]

June Andronick

Proceedings of the Formal Verification of Object-Oriented Software, 2010

The road to trustworthy systems.

[BibT_eX]

[DOI]

Proceedings of the fifth ACM workshop on Scalable trusted computing, 2010

2009

Mind the Gap.

[BibT_eX]

[DOI]

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

seL4: formal verification of an OS kernel.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

2008

Certifying an embedded remote method invocation protocol.

[BibT_eX]

[DOI]

June Andronick

Quang Huy Nguyen

Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), 2008

2006

Formally Proved Anti-tearing Properties of Embedded C Code.

[BibT_eX]

[DOI]

June Andronick

Proceedings of the Leveraging Applications of Formal Methods, 2006

2005

Formal Verification of Security Properties of Smart Card Embedded Source Code.

[BibT_eX]

[DOI]

June Andronick

Boutheina Chetali

Christine Paulin-Mohring

Proceedings of the FM 2005: Formal Methods, 2005

2003

Using Coq to Verify Java Card Applet Isolation Properties.

[BibT_eX]

[DOI]

June Andronick

Boutheina Chetali

Olivier Ly

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

June Andronick

Timeline

Legend:

Links

Online presence:

On csauthors.net:

Bibliography

Loading...