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
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)
Uses Software
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