一句话：提出首个基于 SMT 的复杂 SQL 查询有界等价性验证方法，可证明与反驳查询等价性并生成反例。
SQL 查询等价性检查在查询重写、自动评分等实际应用中十分重要，但现有技术难以推理真实查询中的排序、case 语句和丰富完整性约束等复杂特性。本文提出首个基于 SMT 的方法及其实现 VeriEQL，能够证明和反驳复杂 SQL 查询的有界等价性。其核心是一种新的逻辑编码，在符号元组上使用带未解释函数的整数理论来建模查询语义，简单而实用。作者在超过 20,000 个基准上进行了综合评估，VeriEQL 能证明或反驳的基准数量比所有最先进技术高出一个数量级以上；它还能生成反例，助力发现 MySQL 和 Apache Calcite 等系统中的严重 bug。
The task of SQL query equivalence checking is important in various real-world applications (including query rewriting and automated grading) that involve complex queries with integrity constraints; yet, state-of-the-art techniques are very limited in their capability of reasoning about complex features (e.g., those that involve sorting, case statement, rich integrity constraints, etc.) in real-life queries. To the best of our knowledge, we propose the first SMT-based approach and its implementation, VeriEQL, capable of proving and disproving bounded equivalence of complex SQL queries. VeriEQL is based on a new logical encoding that models query semantics over symbolic tuples using the theory of integers with uninterpreted functions. It is simple yet highly practical -- our comprehensive evaluation on over 20,000 benchmarks shows that VeriEQL outperforms all state-of-the-art techniques by more than one order of magnitude in terms of the number of benchmarks that can be proved or disproved. VeriEQL can also generate counterexamples that facilitate many downstream tasks (such as finding serious bugs in systems like MySQL and Apache Calcite).
@article{paperbot2545,
title = {VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints},
author = {Yang He and Pinhan Zhao and Xinyu Wang and Yuepeng Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649849}
}