LIPIcs.ITP.2019.1.pdf
- Filesize: 157 kB
- 1 pages
Document
A Million Lines of Proof About a Moving Target (Invited Talk)
Author
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-09-05
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
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.
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)
0PDF Downloads