Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
From MaRDI portal
(Redirected from Publication:670699)
Recommendations
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Amortized complexity verified
- Amortised resource analysis with separation logic
- Amortized complexity verified
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
Cites work
- scientific article; zbMATH DE number 58315 (Why is no real title available?)
- scientific article; zbMATH DE number 3511563 (Why is no real title available?)
- scientific article; zbMATH DE number 1953273 (Why is no real title available?)
- scientific article; zbMATH DE number 2119640 (Why is no real title available?)
- A Coq library for internal verification of running-times
- A program logic for resources
- A tutorial on the universality and expressiveness of fold
- A type system for bounded space and functional in-place update
- A type system with usage aspects
- Abstract Predicates and Mutable ADTs in Hoare Type Theory
- Algorithms
- Amortised resource analysis with separation logic
- Amortized Computational Complexity
- Amortized complexity verified
- Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs
- An improved equivalence algorithm
- Certified complexity (CerCo)
- Certifying and Reasoning on Cost Annotations of Functional Programs
- Characteristic formulae for the verification of imperative programs
- Contract-based resource verification for higher-order functions with memoization
- Effective interactive proofs for higher-order imperative programs
- Efficiency of a Good But Not Linear Set Union Algorithm
- Higher-order ghost state
- Hoare type theory, polymorphism and separation
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Introduction to algorithms.
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Lightweight semiformal time complexity analysis for purely functional data structures
- List processing in real time on a serial computer
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Mechanical program analysis
- Multivariate amortized resource analysis
- Program verification through characteristic formulae
- Purely Functional Data Structures
- Quantitative reasoning for proving lock-freedom
- Resource bound certification
- Set Merging Algorithms
- Static prediction of heap space usage for first-order functional programs
- The essence of higher-order concurrent separation logic
- Top-Down Analysis of Path Compression
- Towards automatic resource bound analysis for OCaml
- Union-find with constant time deletions
- Verified characteristic formulae for CakeML
- Worst-case Analysis of Set Union Algorithms
- Ynot: dependent types for imperative programs
Cited in
(15)- scientific article; zbMATH DE number 7649967 (Why is no real title available?)
- Denotational semantics as a foundation for cost recurrence extraction for functional languages
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
- Local reasoning for global graph properties
- Simpler proofs with decentralized invariants
- Two decades of automatic amortized resource analysis
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Relation-algebraic verification of disjoint-set forests
- Verifying asymptotic time complexity of imperative programs in Isabelle
- Amortized complexity verified
- scientific article; zbMATH DE number 7649969 (Why is no real title available?)
Describes a project that uses
Uses Software
This page was built for publication: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q670699)
