Verified Analysis of List Update Algorithms

Maximilian P.L. Haslbeck and Tobias Nipkow

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.

pdf

BibTeX:

@InProceedings{haslbeck_et_al:LIPIcs:2016:6884,
  author ={Maximilian P. L. Haslbeck and Tobias Nipkow},
  title ={{Verified Analysis of List Update Algorithms}},
  booktitle ={36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages ={49:1--49:15},
  series ={Leibniz International Proceedings in Informatics (LIPIcs)},
  year ={2016},
  volume ={65},
  editor ={Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
  publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6884},
  doi ={http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.49}
}
Online article

Isabelle theories in the Archive of Formal Proofs