Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

DOI10.1007/978-3-319-22102-1_9zbMath1465.68172OpenAlexW1424217719MaRDI 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

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (11)

Verified Root-Balanced Trees ⋮ The Negligible and Yet Subtle Cost of Pattern Matching ⋮ Amortized Complexity Verified ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Verified Characteristic Formulae for CakeML ⋮ 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 ⋮ Refinement to imperative HOL ⋮ A Coq Library for Internal Verification of Running-Times ⋮ Relational cost analysis in a functional-imperative setting

Uses Software

• Coq
• OCaml
• CFML
• ACE

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

This page was built for publication: Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation