Fetching the paper…
Reading the bibliography…
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.
Optimal Implementation of Conjunctive Queries in Relational Data Bases. In Proceedings of the ACM Symposium on Theory of Computing (STOC) . ACM, 77–90
Ashok K. Chandra and Philip M. Merlin. 1977 · 1977
Earlier work this paper cites.
Equivalences among Relational Expressions
Alfred V. Aho, Yehoshua Sagiv, and Jeffrey D. Ullman. 1979 · 1979
Earlier work this paper cites.
Formal semantics of SQL queries
Mauro Negri, Giuseppe Pelagatti, and Licia Sbattella. 1991 · 1991
Earlier work this paper cites.
The cascades framework for query optimization
Goetz Graefe. 1995 · 1995
Earlier work this paper cites.
Complex query decorrelation. In Proceedings of the Twelfth International Conference on Data Engineering . IEEE, 450–458
Praveen Seshadri, Hamid Pirahesh, and TY Cliff Leung. 1996 · 1996
Earlier work this paper cites.
Translation Validation. In Proceedings of International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 1384) . 151–166
Amir Pnueli, Michael Siegel, and Eli Singerman. 1998 · 1998
Earlier work this paper cites.
Translation validation for an optimizing compiler. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) . ACM, 83–94
George C. Necula. 2000 · 2000
Earlier work this paper cites.
Simple relational correctness proofs for static analyses and program transformations. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 14–25
Nick Benton. 2004 · 2004
Earlier work this paper cites.
A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004. Proceedings 10 . Springer, 168–176
Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004 · 2004
Earlier work this paper cites.
A Verifier for Interactive, Data-Driven Web Applications. In Proceedings of the ACM SIGMOD International Conference on Management of Data . 539–550
Alin Deutsch, Monica Marcus, Liying Sui, Victor Vianu, and Dayou Zhou. 2005 · 2005
Earlier work this paper cites.
Specification and verification of data-driven Web applications
Alin Deutsch, Liying Sui, and Victor Vianu. 2007 · 2006
Earlier work this paper cites.
Z3: An Efficient SMT Solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 4963) . 337–340
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008 · 2008
Earlier work this paper cites.
CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In Proceedings of the International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science, Vol. 5014) . 35–51
Anna Zaks and Amir Pnueli. 2008 · 2008
Earlier work this paper cites.
Full predicate coverage for testing SQL database queries
Javier Tuya, María José Suárez-Cabal, and Claudio De La Riva. 2010 · 2010
Earlier work this paper cites.
Qex: Symbolic SQL query explorer. In International Conference on Logic for Programming Artificial Intelligence and Reasoning . Springer, 425–446
Margus Veanes, Nikolai Tillmann, and Jonathan de Halleux. 2010 · 2010
Earlier work this paper cites.
Relational Verification Using Product Programs. In Proceedings of the International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science, Vol. 6664) . 200–214
Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011 · 2011
Earlier work this paper cites.
Containment of Conjunctive Queries on Annotated Relations
Todd J. Green. 2011 · 2011
Earlier work this paper cites.
Generating test data for killing SQL mutants: A constraint-based approach. In 2011 IEEE 27th International Conference on Data Engineering . IEEE, 1175–1186
Shetal Shah, S Sudarshan, Suhas Kajbaje, Sandeep Patidar, Bhanu Pratap Gupta, and Devang Vira. 2011 · 2011
Cited alongside, same era.
Equality-Based Translation Validator for LLVM. In Proceedings of the International Conference on Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 6806) . 737–742
Michael Stepp, Ross Tate, and Sorin Lerner. 2011 · 2011
Cited alongside, same era.
A solver for reachability modulo theories. In Computer Aided Verification: 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings 24 . Springer, 427–443
Akash Lal, Shaz Qadeer, and Shuvendu K Lahiri. 2012 · 2012
Cited alongside, same era.
Optimizing database-backed applications with query synthesis. In ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI) . ACM, 3–14
Alvin Cheung, Armando Solar-Lezama, and Samuel Madden. 2013 · 2013
Cited alongside, same era.
Speeding up symbolic reasoning for relational queries
Chenglong Wang, Alvin Cheung, and Rastislav Bodík. 2018a · 2018
Later among the works it cites.
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2018b · 2018
Later among the works it cites.
A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs . 249–261
Véronique Benzaken and Evelyne Contejean. 2019 · 2019
Later among the works it cites.
Automated grading of sql queries. In 2019 IEEE 35th International Conference on Data Engineering (ICDE) . IEEE, 1630–1633
Bikash Chandra, Ananyo Banerjee, Udbhas Hazra, Mathew Joseph, and S Sudarshan. 2019 · 2019
Later among the works it cites.
Explaining wrong queries using small examples. In Proceedings of the 2019 International Conference on Management of Data (SIGMOD) . 503–520
Zhengjie Miao, Sudeepa Roy, and Jun Yang. 2019 · 2019
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
DataFiller – generate random data from database schema
Fabien Coelho. 2013 · 2013
Cited alongside, same era.
Model checking database applications. In Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 19 . Springer, 549–564
Milos Gligoric and Rupak Majumdar. 2013 · 2013
Cited alongside, same era.
A lightweight symbolic virtual machine for solver-aided host languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) . 530–541
Emina Torlak and Rastislav Bodík. 2014 · 2014
Cited alongside, same era.
Data generation for testing and grading SQL queries
Bikash Chandra, Bhupesh Chawda, Biplab Kar, KV Maheshwara Reddy, Shetal Shah, and S Sudarshan. 2015 · 2015
Cited alongside, same era.
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 689–700
Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015 · 2015
Cited alongside, same era.
Cartesian hoare logic for verifying k-safety properties. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) . ACM, 57–69
Marcelo Sousa and Isil Dillig. 2016 · 2016
Cited alongside, same era.
Demonstration of the cosette automated sql prover. In Proceedings of the 2017 ACM International Conference on Management of Data . 1591–1594
Shumo Chu, Daniel Li, Chenglong Wang, Alvin Cheung, and Dan Suciu. 2017a · 2017
Cited alongside, same era.
HoTTSQL: Proving query rewrites with univalent SQL semantics
Shumo Chu, Konstantin Weitz, Alvin Cheung, and Dan Suciu. 2017c · 2017
Cited alongside, same era.
Later among the works it cites.
Mixing set and bag semantics. In Proceedings of the ACM SIGPLAN International Symposium on Database Programming Languages (DBPL) . ACM, 70–73
Wilmer Ricciotti and James Cheney. 2019 · 2019
Later among the works it cites.
Synthesizing database programs for schema refactoring. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation . 286–300
Yuepeng Wang, James Dong, Rushi Shah, and Isil Dillig. 2019 · 2019
Later among the works it cites.
Automated verification of query equivalence using satisfiability modulo theories
Qi Zhou, Joy Arulraj, Shamkant Navathe, William Harris, and Dong Xu. 2019 · 2019
Later among the works it cites.
Deductive optimization of relational data storage
John K. Feser, Sam Madden, Nan Tang, and Armando Solar-Lezama. 2020 · 2020
Later among the works it cites.
Data Migration using Datalog Program Synthesis
Yuepeng Wang, Rushi Shah, Abby Criswell, Rong Pan, and Isil Dillig. 2020 · 2020
Later among the works it cites.
Comprehending nulls. In Proceedings of the International Symposium on Database Programming Languages (DBPL) . ACM, 3–6
James Cheney and Wilmer Ricciotti. 2021 · 2021
Later among the works it cites.
A Formalization of SQL with Nulls
Wilmer Ricciotti and James Cheney. 2022 · 2022
Later among the works it cites.
Qi Zhou, Joy Arulraj, Shamkant B Navathe, William Harris, and Jinpeng Wu. 2022 · 2022
Later among the works it cites.
Calcite Optimization Rules Test Suite
Calcite. 2023 · 2023
Later among the works it cites.
LeetCode website
LeetCode. 2023 · 2023
Later among the works it cites.
Artifact Evaluation VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints
Yang He, Pinhan Zhao, Xinyu Wang, and Yuepeng Wang. 2024 · 2024
Closest in time.