2026-08-10T11:23:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6884 2024-03-06T10:39:06Z ddc:004 open_access

Verified Analysis of List Update Algorithms Haslbeck, Maximilian P. L. Nipkow, Tobias Program Verification Algorithm Analysis Online Algorithms This paper presents a machine-verified analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The analysis is verified with help of the theorem prover Isabelle; some low-level proofs could be automated. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Maximilian P. L. Haslbeck and Tobias Nipkow 2016 Is Part Of LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2016.49 urn:nbn:de:0030-drops-68849 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.49 eng https://creativecommons.org/licenses/by/3.0/legalcode