An assertional proof of red-black trees using Dafny

DOI10.1007/s10817-019-09534-yzbMath1468.68082OpenAlexW2977551386MaRDI QIDQ1984797

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

data structuresbalanced treesverification platforms

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Balanced trees with removals: An exercise in rewriting and proof
• Isabelle/HOL. A proof assistant for higher-order logic
• Organization and maintenance of large ordered indexes
• Symmetric binary B-trees: Data structure and maintenance algorithms
• Automatic Functional Correctness Proofs for Functional Search Trees
• Dafny: An Automatic Program Verifier for Functional Correctness
• Red-black trees in a functional setting
• Balanced search trees made simple
• An Assertional Proof of the Stability and Correctness of Natural Mergesort
• Programming Languages and Systems

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