Automatic functional correctness proofs for functional search trees

DOI10.1007/978-3-319-43144-4_19zbMATH Open1478.68065OpenAlexW2483569599MaRDI QIDQ2829265FDOQ2829265

Tobias Nipkow

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_19

Recommendations

• Verified Root-Balanced Trees
• Purely Functional 1-2 Brother Trees
• Red-black trees in a functional setting
• Recursive proofs for inductive tree data-structures
• Verifying Balanced Trees

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Isabelle/HOL
• Amortized Complexity Verified
• Title not available (Why is that?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Symmetric binary B-trees: Data structure and maintenance algorithms
• Self-adjusting binary search trees
• Proof of correctness of data representations
• Concrete Semantics
• 1-2 Brother Trees or AVL Trees Revisited
• Programming Languages and Systems
• Purely Functional Data Structures
• Title not available (Why is that?)
• Programming with Equations
• Data Refinement in Isabelle/HOL
• Title not available (Why is that?)
• Title not available (Why is that?)
• Balanced trees with removals: An exercise in rewriting and proof
• Red-black trees with types
• A tutorial on specifying data structures in Maude
• Purely Functional 1-2 Brother Trees

Cited In (9)

• An assertional proof of red-black trees using Dafny
• Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
• Verifying Balanced Trees
• Verified analysis of random binary tree structures
• Title not available (Why is that?)
• Verified Root-Balanced Trees
• A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL
• Automatic refinement to efficient data structures: a comparison of two approaches
• Amortized complexity verified

Uses Software

• ACL2
• Isabelle
• Isabelle/HOL
• HOL
• Splay Tree
• AVL trees
• Amortized Complexity
• Archive Formal Proofs

This page was built for publication: Automatic functional correctness proofs for functional search trees

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