Visan, Cosmin Ionut (2025) Formal Verification of Pairing Heaps in Rocq. Bachelor's Thesis, Computing Science.
|
Text
bCS2025VisanCI.pdf Download (358kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf Restricted to Registered users only Download (180kB) |
Abstract
Formal verification plays a crucial role in ensuring the correctness and reliability of data structures, particularly in applications that demand rigorous correctness guarantees. This research focuses on the formal verification of pairing heaps using the Rocq proof assistant. Pairing heaps are a class of self-adjusting priority queues that provide efficient heap operations such as insertion, deletion, and merging. Despite their theoretical efficiency, their correctness has not been verified in the Rocq proof assistant. This project aims to define the structure and operations of pairing heaps in Rocq, implement their fundamental operations, and formally prove their correctness properties. The research will ensure that these implementations maintain heap order and structural invariants, providing machine-checked guarantees. The expected contributions include a formally verified implementation of pairing heaps and correctness proofs for fundamental operations. The results will enhance the reliability of pairing heaps in critical applications such as scheduling algorithms, graph algorithms, and real-time systems.
| 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:39 |
| Last Modified: | 25 Jul 2025 06:39 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/36504 |
Actions (login required)
 |
View Item |