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

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

Mathematics Subject Classification ID

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

• 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