2026-08-16T14:53:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18404 2024-03-06T11:01:49Z ddc:004 open_access

Real-Time Double-Ended Queue Verified (Proof Pearl) Toth, Balazs Nipkow, Tobias Double-ended queue data structures verification Isabelle 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Balazs Toth and Tobias Nipkow 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.29 urn:nbn:de:0030-drops-184044 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.29 eng https://creativecommons.org/licenses/by/4.0/legalcode