{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T05:00:02Z","timestamp":1781586002376,"version":"3.54.5"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"11","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. VLDB Endow."],"published-print":{"date-parts":[[2019,7]]},"abstract":"<jats:p>Database-as-a-service offerings enable users to quickly create and deploy complex data processing pipelines. In practice, these pipelines often exhibit significant overlap of computation due to redundant execution of certain sub-queries. It is challenging for developers and database administrators to manually detect overlap across queries since they may be distributed across teams, organization roles, and geographic locations. Thus, we require automated cloud-scale tools for identifying equivalent queries to minimize computation overlap.<\/jats:p>\n          <jats:p>State-of-the-art algebraic approaches to automated verification of query equivalence suffer from two limitations. First, they are unable to model the semantics of widely-used SQL features, such as complex query predicates and three-valued logic. Second, they have a computationally intensive verification procedure. These limitations restrict their efficacy and efficiency in cloud-scale database-as-a-service offerings.<\/jats:p>\n          <jats:p>This paper makes the case for an alternate approach to determining query equivalence based on symbolic representation. The key idea is to effectively transform a wide range of SQL queries into first order logic formulae and then use satisfiability modulo theories to efficiently verify their equivalence. We have implemented this symbolic representation-based approach in EQUITAS. Our evaluation shows that EQUITAS proves the semantic equivalence of a larger set of query pairs compared to algebraic approaches and reduces the verification time by 27X. We also demonstrate that on a set of 17,461 real-world SQL queries, it automatically identifies redundant execution across 11% of the queries. Our symbolic-representation based technique is currently deployed on Alibaba's MaxCompute database-as-a-service platform.<\/jats:p>","DOI":"10.14778\/3342263.3342267","type":"journal-article","created":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T18:36:11Z","timestamp":1568831771000},"page":"1276-1288","source":"Crossref","is-referenced-by-count":34,"title":["Automated verification of query equivalence using satisfiability modulo theories"],"prefix":"10.14778","volume":"12","author":[{"given":"Qi","family":"Zhou","sequence":"first","affiliation":[{"name":"Georgia Institute of Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joy","family":"Arulraj","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shamkant","family":"Navathe","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"William","family":"Harris","sequence":"additional","affiliation":[{"name":"Galois.Inc"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dong","family":"Xu","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Alibaba MaxCompute. https:\/\/www.alibabacloud.com\/product\/maxcompute.  Alibaba MaxCompute. https:\/\/www.alibabacloud.com\/product\/maxcompute."},{"key":"e_1_2_1_2_1","unstructured":"Ant Financial Services Group. https:\/\/www.antfin.com\/.  Ant Financial Services Group. https:\/\/www.antfin.com\/."},{"key":"e_1_2_1_3_1","unstructured":"Apache Calcite project. http:\/\/calcite.apache.org\/.  Apache Calcite project. http:\/\/calcite.apache.org\/."},{"key":"e_1_2_1_4_1","unstructured":"Apache Drill project. http:\/\/drill.apache.org\/.  Apache Drill project. http:\/\/drill.apache.org\/."},{"key":"e_1_2_1_5_1","unstructured":"Apache Flink project. http:\/\/flink.apache.org\/.  Apache Flink project. http:\/\/flink.apache.org\/."},{"key":"e_1_2_1_6_1","unstructured":"Apache Hive project. http:\/\/hive.apache.org\/.  Apache Hive project. http:\/\/hive.apache.org\/."},{"key":"e_1_2_1_7_1","unstructured":"Apache Kylin project. http:\/\/kylin.apache.org\/.  Apache Kylin project. http:\/\/kylin.apache.org\/."},{"key":"e_1_2_1_8_1","unstructured":"Apache Phoenix project. http:\/\/phoenix.apache.org\/.  Apache Phoenix project. http:\/\/phoenix.apache.org\/."},{"key":"e_1_2_1_9_1","unstructured":"Azure Data Lake. https:\/\/azure.microsoft.com\/en-us\/solutions\/data-lake\/.  Azure Data Lake. https:\/\/azure.microsoft.com\/en-us\/solutions\/data-lake\/."},{"key":"e_1_2_1_10_1","unstructured":"Cosette: An automated SQL solver. https:\/\/github.com\/uwdb\/Cosette.  Cosette: An automated SQL solver. https:\/\/github.com\/uwdb\/Cosette."},{"key":"e_1_2_1_11_1","unstructured":"Google BigQuery. https:\/\/cloud.google.com\/bigquery\/.  Google BigQuery. https:\/\/cloud.google.com\/bigquery\/."},{"key":"e_1_2_1_12_1","unstructured":"Z3prover: Z3 theorem prover. https:\/\/github.com\/Z3Prover\/z3.  Z3prover: Z3 theorem prover. https:\/\/github.com\/Z3Prover\/z3."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.34"},{"key":"e_1_2_1_14_1","volume-title":"Foundations of databases: the logical level","author":"Abiteboul S.","year":"1995","unstructured":"S. Abiteboul , R. Hull , and V. Vianu . Foundations of databases: the logical level . Addison-Wesley Longman Publishing Co., Inc. , 1995 . S. Abiteboul, R. Hull, and V. Vianu. Foundations of databases: the logical level. Addison-Wesley Longman Publishing Co., Inc., 1995."},{"key":"e_1_2_1_15_1","volume-title":"VLDB","author":"Albert J.","year":"1991","unstructured":"J. Albert . Algebraic properties of bag data types . In VLDB , 1991 . J. Albert. Algebraic properties of bag data types. In VLDB, 1991."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/263661.263667"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1628"},{"key":"e_1_2_1_18_1","volume-title":"Journal of Symbolic Logic","author":"Trakhtenbrot B.A.","year":"1950","unstructured":"B.A. Trakhtenbrot . Impossibility of an algorithm for the decision problem in finite classes . In Journal of Symbolic Logic , 1950 . B.A.Trakhtenbrot. Impossibility of an algorithm for the decision problem in finite classes. In Journal of Symbolic Logic, 1950."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_8"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993566"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352590"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803397"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/153850.153856"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/645502.656110"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3058728"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.14778\/3236187.3236200"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_2_1_28_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-47922-8","volume-title":"Containment of aggregate queries","author":"Cohen S.","year":"2002","unstructured":"S. Cohen , W. Nutt , and Y. Sagiv . Containment of aggregate queries . In Lecture Notes in Computer Science , 2002 . S. Cohen, W. Nutt, and Y. Sagiv. Containment of aggregate queries. In Lecture Notes in Computer Science, 2002."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/303976.303992"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/275487.275504"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_33_1","first-page":"03","article-title":"Physical data independence, constraints, and optimization with universal plans","author":"Deutsch A.","year":"2002","unstructured":"A. Deutsch , L. Popa , and V. Tannen . Physical data independence, constraints, and optimization with universal plans . In VLDB , 03 2002 . A. Deutsch, L. Popa, and V. Tannen. Physical data independence, constraints, and optimization with universal plans. In VLDB, 03 2002.","journal-title":"VLDB"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_2_1_35_1","volume-title":"CAV","author":"Grossman S.","year":"2017","unstructured":"S. Grossman , S. Cohen , S. Itzhaky , N. Rinetzky , and M. Sagiv . Verifying equivalence of spark programs . In CAV , 2017 . S. Grossman, S. Cohen, S. Itzhaky, N. Rinetzky, and M. Sagiv. Verifying equivalence of spark programs. In CAV, 2017."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765236.1765265"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/211414.211419"},{"key":"e_1_2_1_38_1","volume-title":"ICDT","author":"Itzhaky S.","year":"2017","unstructured":"S. Itzhaky , T. Kotek , N. Rinetzky , M. Sagiv4, O. Tamir5, H. Veith , and F. Zuleger . On the automated verification of web applications with embedded sql . In ICDT , 2017 . S. Itzhaky, T. Kotek, N. Rinetzky, M. Sagiv4, O. Tamir5, H. Veith, and F. Zuleger. On the automated verification of web applications with embedded sql. In ICDT, 2017."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142363"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.14778\/3192965.3192971"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/275487.275511"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11494645_39"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/111197.111212"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/335191.335421"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1361348.1361350"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2463711"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322221"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132773"},{"key":"e_1_2_1_51_1","volume-title":"CIDR","author":"Shumo C.","year":"2017","unstructured":"C. Shumo , W. Chenglong , W. Konstantin , and C. Alvin . Cosette: An automated SQL prover . In CIDR , 2017 . C. Shumo, W. Chenglong, W. Konstantin, and C. Alvin. Cosette: An automated SQL prover. In CIDR, 2017."},{"key":"e_1_2_1_52_1","volume-title":"ICDT","author":"Tannen V.","year":"1999","unstructured":"V. Tannen and L. Popa . An equational chase for path-conjunctive queries, constraints, and views . In ICDT , 1999 . V. Tannen and L. Popa. An equational chase for path-conjunctive queries, constraints, and views. In ICDT, 1999."},{"key":"e_1_2_1_53_1","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"Tarski A.","year":"1951","unstructured":"A. Tarski . A decision method for elementary algebra and geometry . In Quantifier Elimination and Cylindrical Algebraic Decomposition , 1951 . A. Tarski. A decision method for elementary algebra and geometry. In Quantifier Elimination and Cylindrical Algebraic Decomposition, 1951."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_3"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939165"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158144"}],"container-title":["Proceedings of the VLDB Endowment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.14778\/3342263.3342267","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T09:54:12Z","timestamp":1672221252000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.14778\/3342263.3342267"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7]]},"references-count":56,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2019,7]]}},"alternative-id":["10.14778\/3342263.3342267"],"URL":"https:\/\/doi.org\/10.14778\/3342263.3342267","relation":{},"ISSN":["2150-8097"],"issn-type":[{"value":"2150-8097","type":"print"}],"subject":[],"published":{"date-parts":[[2019,7]]}}}