Verification of B+-Trees with Interactive Theorem Proving and Shape Analysis

This page describes proofs for the correctness of the insert and delete algorithms on B+Trees. The proofs have three parts: The KIV proofs are organized in two projects. A generic library that specifies untyped heaps, explained next. Types, predicates and algorithms specific for B+-Trees are in the second project. Finally, the TVLA proofs are explained.

KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.

The Heap-Library

The Heap library project specifies generic heaps with predicative types. It defines various predicates (like reachability, tree shape etc.) fo these and proves elementary facts about them. The project contains

The B+Tree Project

Project B+Tree specifies the data types required for B+Trees, the algorithms. it contains the proofs of the main theorems as well as proofs for TVLA constraints that are specific to B+Trees. The project is organized as follows:

TVLA-Proofs for subroutines

The TVLA input files consist of

Used basic libraries:

Here you can find all our publications.

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.

[Impressum] [E-Mail]