PV1 ⊧ ATLASchecks or infers types by static analysis

Tool for fully-automated amortised cost analysis of self-adjusting data structures (i.e. splay trees, splay heaps and pairing heaps).

Application domain/field

• Data structures
• Self-adjusting data structures
• Amortised complexity analysis

Type of tool

Complexity analyser

Expected input

Format:

.ml file

Internals

Amortised analysis is a method for the worst-case cost/complexity analysis of data structures. In this paper they present a technique to do this amortised cost analysis of self-adjusting data-structures fully automated. In the CAV '22 paper they extended the tool to deal with probabilistic data structures such as randomised splay trees, randomised meldable heaps and randomised analysis of a binary search tree. Uses Z3