DBDoctor: LLM-Aided SMT Refutation of SQL Query Equivalence
Pending peer review from Preparing for CAV-2026, 2025
Abstract
DBDoctor uses LLMs to propose counterexamples and rewrite queries into SMT-friendly forms, dramatically reducing the rate of “unsupported” query pairs from 100% to 1% and successfully refuting 47% of previously unverifiable cases.
Recommended citation: Lesner, J., Zhao, F., & Yan, X. (2025). Preparing for CAV-2026.
Download Paper