ATLAS: automated amortised complexity analysis of self-adjusting data structures

DOI10.1007/978-3-030-81688-9_5zbMath1493.68129OpenAlexW3181653342MaRDI QIDQ832253

Georg Moser, Florian Zuleger, Lorenz Leutgeb

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81688-9_5

zbMATH Keywords

functional programmingconstraint solvingautomationself-adjusting data structuresamortised cost analysis

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Data structures (68P05)

Uses Software

• z3
• TiML
• Amortized Complexity
• OptiMathSAT
• TcT

Cites Work

• Unnamed Item
• Unnamed Item
• A combination framework for complexity
• Boolean lexicographic optimization: algorithms \& applications
• Amortized complexity verified
• A systematic analysis of splaying
• Automated amortised resource analysis for term rewrite systems
• Runtime complexity analysis of logically constrained rewriting
• Non-polynomial worst-case analysis of recursive programs
• The polynomial complexity of vector addition systems with states
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Complexity and resource bound analysis of imperative programs using difference constraints
• Type-based cost analysis for lazy functional languages
• Closed-form upper bounds in static cost analysis
• An overview of Ciao and its design philosophy
• Size-Change Abstraction and Max-Plus Automata
• Static prediction of heap space usage for first-order functional programs
• A Linear Potential Function for Pairing Heaps
• Analysing the complexity of functional programs: higher-order meets first-order
• From Shapes to Amortized Complexity
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Automated Complexity Analysis Based on the Dependency Pair Method
• Amortized Computational Complexity
• Self-adjusting binary search trees
• Purely Functional Data Structures
• Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
• Amortised Resource Analysis and Typed Polynomial Interpretations
• Decidable Inequalities over Infinite Trees
• Multivariate Amortised Resource Analysis for Term Rewrite Systems
• Verifying Procedural Programs via Constrained Rewriting Induction
• Automatic Type Inference for Amortised Heap-Space Analysis
• Towards automatic resource bound analysis for OCaml
• Multivariate amortized resource analysis

This page was built for publication: ATLAS: automated amortised complexity analysis of self-adjusting data structures