A System-Level Implementation of a Verified Fibonacci Heap as Priority Queue - A System-Level Verification of a Forest of Trees

Sammanfattning

This thesis presents the functional correctness of the insert, meld, and extract minimum operation of the Fibonacci heap in the system-level programming languagePancake. The verification is carried out with the interactive theorem prover hol4and Pancake’s associated separation logic framework. Our approach is defined froma structural design of the Fibonacci heap and a separation of the verification taskover multiple levels. These verification levels start at the logical reasoning aboutthe Fibonacci heap and end in correctness properties stated in terms of Pancake’soperational semantics. We target the Pancake language because it is supported bya verified compiler in hol4.