@inproceedings{d7eb00df73a741668ffbd137ed547e63,
title = "Real-Time Double-Ended Queue Verified (Proof Pearl)",
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.",
keywords = "Double-ended queue, Isabelle, data structures, verification",
author = "Balazs Toth and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Balazs Toth and Tobias Nipkow; licensed under Creative Commons License CC-BY 4.0 14th International Conference on Interactive Theorem Proving (ITP 2023); 14th International Conference on Interactive Theorem Proving, ITP 2023 ; Conference date: 31-07-2023 Through 04-08-2023",
year = "2023",
month = jul,
doi = "10.4230/LIPIcs.ITP.2023.29",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Adam Naumowicz and Rene Thiemann",
booktitle = "14th International Conference on Interactive Theorem Proving, ITP 2023",
}