@inproceedings{b69c7b3c917d4e4196624a3086cb6452,
title = "Verification of Scapegoat Trees Using Dafny",
abstract = "Self-balancing binary search trees are essential in Computer Science for their versatility and efficient management of ordered data. While a clear definition might exist for a specific kind of balanced tree, multiple implementations can exist. This diversity highlights the critical importance of verifying the correctness of a specific implementation. With this perspective, this paper shifts focus to the scapegoat tree, a type of self-balancing tree, prized for its operational simplicity. Utilizing the formal verification tool, Dafny, we undertake a rigorous examination of a scapegoat tree implementation. Through Dafny{\textquoteright}s powerful specification and verification techniques, we prove the correctness of its core operations within our chosen implementation. We also summarized our user experience with Dafny, presenting several techniques that can enhance the efficiency of the proof process.",
keywords = "Dafny, Formal Methods, Scapegoat Trees, Verification",
author = "Jiapeng Wang and Sini Chen and Huibiao Zhu",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.; 16th International Symposium on NASA Formal Methods, NFM 2024 ; Conference date: 04-06-2024 Through 06-06-2024",
year = "2024",
doi = "10.1007/978-3-031-60698-4\_7",
language = "英语",
isbn = "9783031606977",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "118--135",
editor = "Nathaniel Benz and Divya Gopinath and Nija Shi",
booktitle = "NASA Formal Methods - 16th International Symposium, NFM 2024, Proceedings",
address = "德国",
}