License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.29
URN: urn:nbn:de:0030-drops-184044
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18404/
Go to the corresponding LIPIcs Volume Portal

Toth, Balazs ; Nipkow, Tobias

Real-Time Double-Ended Queue Verified (Proof Pearl)

pdf-format:
LIPIcs-ITP-2023-29.pdf (0.6 MB)

Abstract

We present the first verification of the real-time doubled-ended queue by Chuang and Goldberg where all operations take constant time. The main contributions are the full system invariant, the precise definition of all abstraction functions, the structure of the proof and the main lemmas.

BibTeX - Entry

@InProceedings{toth_et_al:LIPIcs.ITP.2023.29,
  author =	{Toth, Balazs and Nipkow, Tobias},
  title =	{{Real-Time Double-Ended Queue Verified (Proof Pearl)}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18404},
  URN =		{urn:nbn:de:0030-drops-184044},
  doi =		{10.4230/LIPIcs.ITP.2023.29},
  annote =	{Keywords: Double-ended queue, data structures, verification, Isabelle}
}

Keywords: Double-ended queue, data structures, verification, Isabelle
Collection: 14th International Conference on Interactive Theorem Proving (ITP 2023)
Issue Date: 2023
Date of publication: 26.07.2023

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