From Formal Specification to Intent: A Progressive Framework for Semantically Correct SQL

Abstract

Ensuring the semantic correctness of SQL queries is a fundamental challenge in data management. As the modality of query authorship shifts from students learning in classrooms to developers debugging complex logic, and finally to non-experts prompting AI agents, the "ground truth" available to verify correctness becomes increasingly scarce. This dissertation presents a trilogy of approaches that address the problem of SQL correctness under progressively looser assumptions: moving from scenarios where a correct “reference” query is already known, to where concrete data is available for inspection, and finally to where only implicit user intent exists.First, we address the setting in which a correct reference query is available, as is typical in educational settings. We present QR-HINT, a system that guides users from their flawed query to semantic equivalence with respect to the reference query. Unlike many standard feedback mechanisms, which only determine query equivalence or provide counterexamples, QR-HINT generates provably correct, actionable, and locally optimal hints to help users correct their query, such that it becomes semantically equivalent to the reference query despite syntactic differences.Second, we relax the assumption of a known reference query. In most real-world scenarios, developers do not begin with a reference query; instead, they write queries against underlying data and can verify correctness by inspecting execution and results. For this setting, we introduce I-REX, an interactive debugger that treats declarative SQL like procedural code. By leveraging data provenance and efficient on-demand “paginated” execution, I-REX allows users to step through and teleport across the “logical” execution of a query, even if its actual execution on the underlying data uses different, highly efficient strategies to ensure scalability.Finally, we address an AI-era challenge: verifying whether an AI-generated query accurately reflects a user's implicit intent. There is no reference query or concrete database instance, and worse, they may not know the language that the query is written in. To bridge this gap, we introduce a framework for interactive verification through questions and answers with users. We model the user as an oracle interacting with "conditional instances" — symbolic representations of possible database instances — to identify whether a result should be returned by the query. We give a procedure for verifying the correctness of any self-join-free conjunctive queries. We also prove that verification for conjunctive queries with inequalities and self-joins is undecidable in general.