Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
From MaRDI portal
Publication:2945628
DOI10.1007/978-3-319-22102-1_9zbMath1465.68172MaRDI QIDQ2945628
Arthur Charguéraud, François Pottier
Publication date: 14 September 2015
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01245872/file/credits_itp15.pdf
68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
68P05: Data structures
68V20: Formalization of mathematics in connection with theorem provers
Related Items
Relational cost analysis in a functional-imperative setting, Verified Root-Balanced Trees, The Negligible and Yet Subtle Cost of Pattern Matching, Characteristic formulae for liveness properties of non-terminating CakeML programs, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Amortized complexity verified, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Refinement to imperative HOL, A Coq Library for Internal Verification of Running-Times, Amortized Complexity Verified, Verified Characteristic Formulae for CakeML
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Effective interactive proofs for higher-order imperative programs
- Static prediction of heap space usage for first-order functional programs
- Amortized Complexity Verified
- Lightweight semiformal time complexity analysis for purely functional data structures
- Certified Complexity (CerCo)
- Amortized Resource Analysis with Polynomial Potential
- Worst-case Analysis of Set Union Algorithms
- Mechanical program analysis
- Efficiency of a Good But Not Linear Set Union Algorithm
- Union-Find with Constant Time Deletions
- Program verification through characteristic formulae
- An improved equivalence algorithm
- Semi-persistent Data Structures
- Set Merging Algorithms