<div class="csl-bib-body">
<div class="csl-entry">Leutgeb, L., Moser, G., & Zuleger, F. (2022). Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In <i>Computer Aided Verification - 34th International Conference, CAV 2022</i> (pp. 70–91). https://doi.org/10.1007/978-3-031-13188-2_4</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/150227
-
dc.description.abstract
In this paper, we present the first fully-automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps and randomised meldable heaps, which so far have only (semi-)manually been analysed in the literature. Our analysis is stated as a type-and-effect system for a first-order functional programming language with support for sampling over discrete distributions, non-deterministic choice and a ticking operator. The latter allows for the specification of fine-grained cost models. We state two soundness theorems based on two different—but strongly related—typing rules of ticking, which account differently for the cost of non-terminating computations. Finally we provide a prototype implementation able to fully automatically analyse the aforementioned case studies.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
amortised cost analysis
en
dc.subject
automation
en
dc.subject
constraint solving
en
dc.subject
functional programming
en
dc.subject
probabilistic data structures
en
dc.title
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.relation.isbn
978-3-031-13188-2
-
dc.description.startpage
70
-
dc.description.endpage
91
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Computer Aided Verification - 34th International Conference, CAV 2022