Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
From MaRDI portal
Publication:670699
DOI10.1007/S10817-017-9431-7zbMATH Open1468.68120OpenAlexW2757243080MaRDI QIDQ670699FDOQ670699
Authors: Arthur Charguéraud, François Pottier 
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
Recommendations
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Amortized complexity verified
- Amortised resource analysis with separation logic
- Amortized complexity verified
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Program verification through characteristic formulae
- Ynot: dependent types for imperative programs
- Amortized complexity verified
- Title not available (Why is that?)
- Introduction to algorithms.
- Efficiency of a Good But Not Linear Set Union Algorithm
- Characteristic formulae for the verification of imperative programs
- Multivariate amortized resource analysis
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Effective interactive proofs for higher-order imperative programs
- Hoare type theory, polymorphism and separation
- Worst-case Analysis of Set Union Algorithms
- A tutorial on the universality and expressiveness of fold
- Title not available (Why is that?)
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Union-find with constant time deletions
- Purely Functional Data Structures
- Amortized Computational Complexity
- Mechanical program analysis
- An improved equivalence algorithm
- Set Merging Algorithms
- List processing in real time on a serial computer
- Title not available (Why is that?)
- Title not available (Why is that?)
- A program logic for resources
- A type system for bounded space and functional in-place update
- A Coq library for internal verification of running-times
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Static prediction of heap space usage for first-order functional programs
- 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)
- Amortised resource analysis with separation logic
- Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs
- Resource bound certification
- Quantitative reasoning for proving lock-freedom
- Top-Down Analysis of Path Compression
- Contract-based resource verification for higher-order functions with memoization
- Towards automatic resource bound analysis for OCaml
- A type system with usage aspects
- Abstract Predicates and Mutable ADTs in Hoare Type Theory
- Algorithms
Cited In (15)
- Title not available (Why is that?)
- Denotational semantics as a foundation for cost recurrence extraction for functional languages
- 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
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
- Local reasoning for global graph properties
- Two decades of automatic amortized resource analysis
- Simpler proofs with decentralized invariants
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- Relation-algebraic verification of disjoint-set forests
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Verifying asymptotic time complexity of imperative programs in Isabelle
- Amortized complexity verified
- Title not available (Why is that?)
Uses Software
This page was built for publication: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q670699)
