Query Optimization for Databases

Chair for Logic and Verification

Master’s thesis

The main result of this thesis is a formalisation of the IKKBZ algorithm as taught in the lecture query optimization for relational databases. The thesis includes a general framework consisting of the definitions of selectivities, query graphs, join trees, and cost functions. Furthermore, it implements the join ordering algorithm IKKBZ using these definitions. Isabelle/HOL is used to verify the correctness of these definitions and prove that IKKBZ produces an optimal solution within a restricted solution space.

PDF Download

Student: Bernhard Stöckl

Supervisor: Lukas Stevens

Professor: Prof. Tobias Nipkow