@inproceedings{c1eb17d0d45c411d90200d96b6d2423b,
title = "Verified analysis of list update algorithms",
abstract = "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.",
keywords = "Algorithm analysis, Online algorithms, Program verification",
author = "Haslbeck, {Maximilian P.L.} and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Maximilian P. L. Haslbeck and Tobias Nipkow.; 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016 ; Conference date: 13-12-2016 Through 15-12-2016",
year = "2016",
month = dec,
day = "1",
doi = "10.4230/LIPIcs.FSTTCS.2016.49",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
pages = "49.1--49.15",
editor = "Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen and Saket Saurabh",
booktitle = "36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016",
}