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.
Student: Bernhard Stöckl
Supervisor: Lukas Stevens
Professor: Prof. Tobias Nipkow