Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Verification of Query Optimizat...


view this post on Zulip Email Gateway (Oct 05 2022 at 17:48):

From: Gerwin Klein <kleing@unsw.edu.au>
Verification of Query Optimization Algorithms
by Lukas Stevens and Bernhard Stöckl

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.

https://www.isa-afp.org/entries/Query_Optimization.html

Enjoy!
Gerwin


Last updated: Apr 19 2024 at 20:15 UTC