An assertional proof of red-black trees using Dafny

DOI10.1007/S10817-019-09534-YMaRDI QIDQ1984797zbMATH OpenOpenAlexFDO

Authors Ricardo Peña

Publication date 7 April 2020

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

Full work available at URL https://doi.org/10.1007/s10817-019-09534-y

zbMATH Keywords

balanced treesdata structuresverification platforms

Mathematics Subject Classification ID

Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Automatic functional correctness proofs for functional search trees
• Verifying Balanced Trees
• Verified Root-Balanced Trees
• Red-black trees with types
• Recursive proofs for inductive tree data-structures

Cites work

• An assertional proof of the stability and correctness of Natural Mergesort
• Automatic functional correctness proofs for functional search trees
• Balanced search trees made simple
• Balanced trees with removals: An exercise in rewriting and proof
• Dafny: an automatic program verifier for functional correctness
• scientific article; zbMATH DE number 517385 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Introduction to algorithms
• Isabelle/HOL. A proof assistant for higher-order logic
• Organization and maintenance of large ordered indexes
• Programming Languages and Systems
• Red-black trees in a functional setting
• Symmetric binary B-trees: Data structure and maintenance algorithms

Cited in

(1)

• Red-black trees with types

Describes a project that uses

Uses Software

• Coq
• Dafny
• Isabelle/HOL
• LARCH
• Why3
• z3

This page was built for publication: An assertional proof of red-black trees using Dafny

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