License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.1
URN: urn:nbn:de:0030-drops-110567
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11056/
Go to the corresponding LIPIcs Volume Portal

Andronick, June

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

pdf-format:
LIPIcs-ITP-2019-1.pdf (0.2 MB)

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.

BibTeX - Entry

@InProceedings{andronick:LIPIcs:2019:11056,
  author =	{June Andronick},
  title =	{{A Million Lines of Proof About a Moving Target (Invited Talk)}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11056},
  URN =		{urn:nbn:de:0030-drops-110567},
  doi =		{10.4230/LIPIcs.ITP.2019.1},
  annote =	{Keywords: Proof maintentance, proof evolution, seL4, Isabelle/HOL}
}

Keywords: Proof maintentance, proof evolution, seL4, Isabelle/HOL
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI