Cornea, Horia-Matei (2024) Formal Verification of 2-3 Trees in Coq. Bachelor's Thesis, Computing Science.
|
Text
2-3TreesReport.pdf Download (199kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (314kB) |
Abstract
This thesis investigates the formal verification of 2-3 trees using the Coq proof assistant. The recursive nature of 2-3 trees, combined with their foundational role in computer science, makes them an ideal subject for this study. This work focuses on maintaining invariant properties and algebraic specifications of 2-3 trees during operations such as lookup, insertion, and deletion. The insertion and lookup operations are thoroughly verified, demonstrating the preservation of sorted and balanced properties of 2-3 trees. Although proofs for the deletion operation remain incomplete, the groundwork is laid for future extensions. This research underscores the importance and challenges of formal verification in advancing reliable and robust data structures, with potential applications extending to more complex structures like B-trees.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Frumin, D. and Perez Parra, J.A. |
| Degree programme: | Computing Science |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 23 Jul 2024 10:13 |
| Last Modified: | 23 Jul 2024 10:13 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/33570 |
Actions (login required)
 |
View Item |