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

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.
Complexity

Links

Repository: https://github.com/lorenzleutgeb/atlas/

Last commit date

28 April 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_5 (CAV '21)

Last publication date

15 July 2021

Related tools

uses Z3

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.