Automatic functional correctness proofs for functional search trees

DOI10.1007/978-3-319-43144-4_19MaRDI QIDQ2829265zbMATH OpenOpenAlexFDO

Authors 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

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)

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

Cites work

• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 3518272 (Why is no real title available?)
• scientific article; zbMATH DE number 3999266 (Why is no real title available?)
• scientific article; zbMATH DE number 839552 (Why is no real title available?)
• 1-2 Brother Trees or AVL Trees Revisited
• A tutorial on specifying data structures in Maude
• Amortized complexity verified
• Balanced trees with removals: An exercise in rewriting and proof
• Concrete semantics. With Isabelle/HOL
• Data refinement in Isabelle/HOL
• Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Programming Languages and Systems
• Programming with Equations
• Proof of correctness of data representations
• Purely Functional 1-2 Brother Trees
• Purely Functional Data Structures
• Red-black trees with types
• Self-adjusting binary search trees
• Symmetric binary B-trees: Data structure and maintenance algorithms

Cited in

(11)

• An assertional proof of red-black trees using Dafny
• Verifying Balanced Trees
• Functional data structures and algorithms. A proof assistant approach
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• How to keep your neighbours in order
• Verified analysis of random binary tree structures
• scientific article; zbMATH DE number 7649954 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

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

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)