VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints

SQL查询等价检查任务在包含完整性约束的复杂查询的各种现实世界应用（包括查询重写和自动评分）中非常重要。然而，现有技术在处理现实生活中查询中涉及排序、case语句、丰富的完整性约束等复杂特性时的推理能力非常有限。据我们所知，我们提出了第一个基于SMT的方法及其实现VeriEQL，能够证明和证伪复杂SQL查询的有界等价性。VeriEQL基于一种新的逻辑编码，使用未解释函数的整数理论对符号元组上的查询语义进行建模。它简单而实用——我们对超过20,000个基准测试进行了全面评估，结果显示VeriEQL在能够证明或证伪的基准测试数量方面比所有现有技术都高出一个数量级以上。VeriEQL还可以生成反例，有助于许多下游任务（例如在MySQL和Apache Calcite等系统中发现严重的错误）。

论文旨在解决SQL查询等价性检查的问题，特别是针对涉及排序、Case语句、完整性约束等复杂特征的查询。这是一个新问题。

论文提出了一种基于SMT的方法和实现，名为VeriEQL，可以证明和否定复杂SQL查询的有界等价性。该方法使用整数理论和未解释函数对符号元组上的查询语义进行建模，是一种简单而高效的方法。

论文通过对20000多个基准测试的全面评估表明，VeriEQL在可以证明或否定的基准测试数量方面比所有现有技术都高出一个数量级。VeriEQL还可以生成反例，有助于许多下游任务。论文的代码和数据集已经开源。

近期的相关研究包括：1. Efficient Checking of SQL Statement Semantics via Query Decomposition；2. Verifying SQL Queries Using Query Containment；3. Automating SQL Query Optimization via Graph Convolutional Networks。