Verification of Query Optimization Algorithms. - Lukas Stevens; Bernhard Stöckl (Arch. Formal Proofs, 2022)