University of Twente Student Theses


Formal verification of a red-black tree data structure

Nguyen, ir. H.M. (2019) Formal verification of a red-black tree data structure.

[img] PDF
Abstract:Nowadays, although software has been integrated deeply into our society, software errors are still common. Because the failure of software can have devastating effects, being certain that a program does what it is meant to do is crucial. This thesis conducts a case study in deductive verification, which is a sub-area of formal verification. The case study involves a company in the Netherlands and their industrial red-black tree code. This thesis is intended to be an experience report to show how formal verification can be used to help proving the correctness of a program. Ultimately, we want to be able to verify the industrial red-black tree code. However, in this thesis, we only cover the verification of a standard red-black tree code. The main section presents how specifications of a red-black tree can be developed, and the obstacles that are met during the development. Finally, we conclude with the comparisons with the results of other authors and possible future work.
Item Type:Essay (Master)
BetterBe, Enschede, Netherlands
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page