Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699): Difference between revisions

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