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

Abstract

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