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

Andronick, June

doi:10.4230/LIPIcs.ITP.2019.1

Document

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

Author June Andronick

Part of: Volume: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Interactive Theorem Proving (ITP)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2019-09-05

PDF

File

PDF

LIPIcs.ITP.2019.1.pdf

Filesize: 157 kB
1 pages

Document Identifiers

DOI: 10.4230/LIPIcs.ITP.2019.1
URN: urn:nbn:de:0030-drops-110567

Subject Classification

ACM Subject Classification

Software and its engineering → Formal software verification
Software and its engineering → Software evolution
Software and its engineering → Operating systems

Keywords

Proof maintentance
proof evolution
seL4
Isabelle/HOL

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

In the last ten years, we have been porting, maintaining, and evolving the world’s largest proof base, the formal proof in Isabelle/HOL of the seL4 microkernel. But actually, there is no such thing as "the seL4 proof"; there are a number of proofs (functional correctness, binary translation validation, integrity and confidentiality proofs, etc) about a number of instances of seL4 (depending on the hardware platform it runs on, the features it includes, the extensions it supports). We will give an overview of the current state of these proofs, and, importantly, the challenges we face in keeping to maintain, evolve and extend them, and the processes we have put in place to manage their dependence on the evolving implementation.

Cite As Get BibTex

June Andronick. A Million Lines of Proof About a Moving Target (Invited Talk). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.1

Author Details

June Andronick

CSIRO's Data61, Sydney, Australia
UNSW, Sydney, Australia

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail