Amortized complexity verified
From MaRDI portal
Publication:670702
Recommendations
- Amortized complexity verified
- scientific article; zbMATH DE number 54254
- ATLAS: automated amortised complexity analysis of self-adjusting data structures
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Type-based analysis of logarithmic amortised complexity
Cites work
- scientific article; zbMATH DE number 1617246 (Why is no real title available?)
- scientific article; zbMATH DE number 5542185 (Why is no real title available?)
- scientific article; zbMATH DE number 177794 (Why is no real title available?)
- A Coq library for internal verification of running-times
- A systematic analysis of splaying
- A verified compiler from Isabelle/HOL to CakeML
- Amortised resource analysis with separation logic
- Amortized Computational Complexity
- Amortized complexity verified
- Automated higher-order complexity analysis
- Automated resource analysis with Coq proof objects
- Automatic average-case analysis of algorithms
- Automatic functional correctness proofs for functional search trees
- Automating program analysis
- CakeML
- Code generation via higher-order rewrite systems
- Concrete semantics. With Isabelle/HOL
- Contract-based resource verification for higher-order functions with memoization
- Denotational cost semantics for functional languages with inductive types
- Implementation of Functional Languages
- Isabelle/HOL. A proof assistant for higher-order logic
- Lightweight semiformal time complexity analysis for purely functional data structures
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Mechanical program analysis
- Multivariate amortized resource analysis
- Partial Recursive Functions in Higher-Order Logic
- Purely Functional Data Structures
- Rank-pairing heaps
- Resource bound certification
- Self-Adjusting Heaps
- Self-adjusting binary search trees
- Static prediction of heap space usage for first-order functional programs
- The derivation of a tighter bound for top-down skew heaps
- The pairing heap: A new form of self-adjusting heap
- Towards automatic resource bound analysis for OCaml
- Verified Root-Balanced Trees
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
Cited in
(10)- ATLAS: automated amortised complexity analysis of self-adjusting data structures
- Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
- Amortized complexity verified
- scientific article; zbMATH DE number 54254 (Why is no real title available?)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Exponential automatic amortized resource analysis
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Amortized Computational Complexity
- Lightweight semiformal time complexity analysis for purely functional data structures
- Type-based analysis of logarithmic amortised complexity
Describes a project that uses
Uses Software
This page was built for publication: Amortized complexity verified
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q670702)
