Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

DOI10.1007/s10817-017-9431-7zbMath1468.68120OpenAlexW2757243080MaRDI QIDQ670699

François Pottier, Arthur Charguéraud

Publication date: 20 March 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01652785/file/credits_jar.pdf

zbMATH Keywords

verificationseparation logicunion-findtime credits

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) 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 (10)

Local Reasoning for Global Graph Properties ⋮ 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 ⋮ Denotational semantics as a foundation for cost recurrence extraction for functional languages ⋮ Unnamed Item ⋮ Unnamed Item ⋮ For a few dollars more. Verified fine-grained algorithm analysis down to LLVM ⋮ Amortized complexity verified ⋮ Simpler proofs with decentralized invariants ⋮ Two decades of automatic amortized resource analysis

Uses Software

• Coq
• OCaml
• Ynot
• VACID-0
• ACE
• Grail
• Camelot
• Bedrock
• Separation Logic
• Amortized Complexity
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A program logic for resources
• A Coq Library for Internal Verification of Running-Times
• Iris
• Effective interactive proofs for higher-order imperative programs
• Static prediction of heap space usage for first-order functional programs
• Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
• Amortized Complexity Verified
• Higher-order ghost state
• Verified Characteristic Formulae for CakeML
• The Essence of Higher-Order Concurrent Separation Logic
• Certifying and Reasoning on Cost Annotations of Functional Programs
• Lightweight semiformal time complexity analysis for purely functional data structures
• Certified Complexity (CerCo)
• Hoare type theory, polymorphism and separation
• Amortised Resource Analysis with Separation Logic
• Amortized Resource Analysis with Polynomial Potential
• Amortized Computational Complexity
• Worst-case Analysis of Set Union Algorithms
• Mechanical program analysis
• Efficiency of a Good But Not Linear Set Union Algorithm
• List processing in real time on a serial computer
• Purely Functional Data Structures
• A tutorial on the universality and expressiveness of fold
• Union-Find with Constant Time Deletions
• Program verification through characteristic formulae
• Characteristic formulae for the verification of imperative programs
• Ynot
• Resource bound certification
• Quantitative Reasoning for Proving Lock-Freedom
• Top-Down Analysis of Path Compression
• An improved equivalence algorithm
• Contract-based resource verification for higher-order functions with memoization
• Towards automatic resource bound analysis for OCaml
• Multivariate amortized resource analysis
• A type system with usage aspects
• Set Merging Algorithms
• Abstract Predicates and Mutable ADTs in Hoare Type Theory
• Algorithms

This page was built for publication: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits