Dumitrache, Elena Marcela (2025) Formal Verification of Leftist and Skew Heaps in Rocq. Bachelor's Thesis, Computing Science.
|
Text
bCS2025DumitracheEM.pdf Download (1MB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf Restricted to Registered users only Download (180kB) |
Abstract
Leftist and Skew Heaps are data structures that provide efficient insertion, deletion, and merging operations, and are widely used in scheduling algorithms, graph algorithms, and real-time systems. Despite their theoretical efficiency and practical relevance, subtle implementation errors can compromise their reliability. Remarkably, these data structures had not, until now, been subject to formal verification within the Rocq proof assistant. This thesis addresses exactly that gap by formally verifying Leftist and Skew Heaps using Rocq, a tool for constructing machine-checked mathematical proofs. The work provides rigorous definitions of both heap types in Rocq, specifies their core operations, and proves that these operations preserve key properties such as heap order, structural invariants, and the integrity of the multiset of elements through permutation proofs. By establishing machine-checked guarantees for each operation, this research contributes to building a strong and reliable foundation for software systems where correctness is critical.
| 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: | 25 Jul 2025 06:27 |
| Last Modified: | 25 Jul 2025 06:27 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/36519 |
Actions (login required)
 |
View Item |