Verification of Query Optimization Algorithms

Lukas Stevens 🌐 and Bernhard Stöckl 📧

October 4, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This formalization includes a general framework for query optimization consisting of the definitions of selectivities, query graphs, join trees, and cost functions. Furthermore, it implements the join ordering algorithm IKKBZ using these definitions. It verifies the correctness of these definitions and proves that IKKBZ produces an optimal solution within a restricted solution space.


BSD License


Session Query_Optimization

Depends on