Verification of Query Optimization Algorithms

Lukas Stevens 🌐 and Bernhard Stöckl 📧

October 4, 2022


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