Anastasiya Kravchuk-Kirilyuk will present her MSE talk "The B+-tree Index as a Verified Software Unit" on May 7th, 2020 at 1:30 pm via Zoom.

Zoom Link:

Everyone is invited to attend her talk.  Please see below for talk abstract.

Ordered indexes are used in relational databases to allow for a faster retrieval of records. An ordered index can be implemented using a variety of data structures, and the query planner can later decide which implementation to use for optimal performance. This means the implementation details of an ordered index need not be exposed to the user. In this work, we define an API that any instance of an ordered index should implement. Then, we show that a particular instance of an ordered index, the B+-tree with cursors, satisfies this general interface. Finally, we present the B+-tree index instance as a Verified Software Unit, a VST-verified module with explicitly defined sets of imported and exported functions. That is, a B+-tree implementation verified for functional correctness to a B+-tree specification in previous work, is formally proved to be functionally correct w.r.t. the abstract specification of an ordered index. We verify our code using the Coq proof assistant, the Verified Software Toolchain (VST), and CompCert.