Formal Verification of Pointer-Based Splay Trees in Iris

January 28, 2021

When real-world applications crash or start to lack in performance, they can bring tremendous costs to the involving parties. Therefore, it is important to ensure that these applications do not fail. Testing is useful in practice as it can be used to show the presence of bugs. However, it cannot be used to prove their absence. On the other hand, formal verification can be used to prove that a program fully meets a given specification. However, formal verification of real-world code, which normally manipulates mutable and non-trivial data structures, is a difficult task. In the last few years, many advances have been made in formal verification, but there are still many opportunities to verify real-world code. In this project, we explore Coq and the Iris framework to verify the functional correctness of the pointer-based implementation of Splay Trees which is used by the GNU Compiler Collection (GCC) in the Offloading and Multi Processing Runtime Library (libgomp). In the process, we also verify a functional implementation of the splay tree algorithm for a generalized ordered datatype using the interactive proof assistant Coq. To the best of our knowledge, we provide the most complete formally verified pointer-based implementation of Splay Trees.

Authors in the community:

• 

  R

  Ricardo Ciríaco da Graça

  ist193994

Supervisors of this institution:

• 

  J

  João Fernando Peixoto Ferreira

  ist428178

electrical-engineering-electronic-engineering-information-engineering - Electrical engineering, electronic engineering, information engineering

eng - English

Instituto Superior Técnico