Verified analysis of random binary tree structures

DOI10.1007/S10817-020-09545-0MaRDI QIDQ5919010zbMATH OpenOpenAlexFDO

Authors Manuel Eberl, Max W. Haslbeck, Tobias Nipkow

Publication date 2 November 2020

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-020-09545-0

zbMATH Keywords

quicksortinteractive theorem provingIsabellebinary search treesrandomised algorithmsrandomised data structures

Mathematics Subject Classification ID

Randomized algorithms (68W20) Analysis of algorithms (68W40) Data structures (68P05) Searching and sorting (68P10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Verified analysis of random binary tree structures
• Verified Root-Balanced Trees
• Verified tail bounds for randomized programs
• Random binary trees: from the average case analysis to the asymptotics of distributions
• Verified analysis of list update algorithms

Cites work

• scientific article; zbMATH DE number 3764843 (Why is no real title available?)
• scientific article; zbMATH DE number 1052006 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 4115969 (Why is no real title available?)
• A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
• A unifying look at data structures
• A verified compiler for probability density functions
• Algorithmen und Datenstrukturen
• Amortized complexity verified
• Automated recurrence analysis for almost-linear expected-runtime bounds
• Automatic functional correctness proofs for functional search trees
• Concrete semantics. With Isabelle/HOL
• CryptHOL: game-based proofs in higher-order logic
• Formal certification of code-based cryptographic proofs
• Formalising Semantics for Expected Running Time of Probabilistic Programs
• Introduction to algorithms
• Isabelle/HOL. A proof assistant for higher-order logic
• Markov chains and Markov decision processes in Isabelle/HOL
• Probabilistic functions and cryptographic oracles in higher order logic
• Probabilistic recurrence relations
• Proofs of randomized algorithms in Coq
• Quicksort
• Randomized binary search trees
• Randomized search trees
• The analysis of Quicksort programs
• The height of a random binary search tree
• Three chapters of measure theory in Isabelle/HOL
• Verified Root-Balanced Trees
• Verified analysis of random binary tree structures
• Verified tail bounds for randomized programs
• Weakest precondition reasoning for expected run-times of probabilistic programs

Cited in

(8)

• Combining higher-order logic with set theory formalizations
• Verifying randomised social choice
• Verified analysis of random binary tree structures
• Loop verification with invariants and contracts
• Derandomization with pseudorandomness
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Probabilistic analysis of vantage point trees
• Parameter estimation in topological analysis of binary tree structures

Describes a project that uses

Uses Software

• Probabilistic_Prime_Tests
• Monad normalisation
• Density Compiler
• Random BSTs
• Root Balanced Tree
• Treaps
• QuickSort Cost
• Archive Formal Proofs
• Amortized Complexity
• CryptHOL
• Ergodic theory
• Quicksort
• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: Verified analysis of random binary tree structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5919010)