Search Results

Documents authored by Andronick, June

Document
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2022
LIPIcs, Volume 237, ITP 2022, Complete Volume

Authors: June Andronick and Leonardo de Moura

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
LIPIcs, Volume 237, ITP 2022, Complete Volume
Cite as

June Andronick and Leonardo de Moura. LIPIcs, Volume 237, ITP 2022, Complete Volume. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1-602, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{andronick_et_al:LIPIcs.ITP.2022,
  title =	{{LIPIcs, Volume 237, ITP 2022, Complete Volume}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{1--602},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022},
  URN =		{urn:nbn:de:0030-drops-167080},
  doi =		{10.4230/LIPIcs.ITP.2022},
  annote =	{Keywords: LIPIcs, Volume 237, ITP 2022, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2022.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: June Andronick and Leonardo de Moura

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

June Andronick and Leonardo de Moura. Front Matter, Table of Contents, Preface, Conference Organization. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 0:i-0:x, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{andronick_et_al:LIPIcs.ITP.2022.0,
  author =	{Andronick, June and de Moura, Leonardo},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.0},
  URN =		{urn:nbn:de:0030-drops-167097},
  doi =		{10.4230/LIPIcs.ITP.2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2019.1
A Million Lines of Proof About a Moving Target (Invited Talk)

Authors: June Andronick

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

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

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)

Copy BibTex To Clipboard

@InProceedings{andronick:LIPIcs.ITP.2019.1,
  author =	{Andronick, June},
  title =	{{A Million Lines of Proof About a Moving Target}},
  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 =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.1},
  URN =		{urn:nbn:de:0030-drops-110567},
  doi =		{10.4230/LIPIcs.ITP.2019.1},
  annote =	{Keywords: Proof maintentance, proof evolution, seL4, Isabelle/HOL}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact