Demonstration of the Cosette Automated SQL Prover

Summary: Cosette is the automated prover for SQL query equivalence, combining constraint solving with interactive theorem proving to decide equivalence and counterexamples. Demonstrates magic-set rewrite, optimizer-bug counterexamples, and a UI to explore results. (summarized by gpt-5-nano on Feb 09 2026)

Paper ID: 5424
Venue: SIGMOD
Year: 2017
Pagerank: 7.6679093e-05
Overall Rank: 3,172 | 78.24%
DOI: 10.1145/3035918.3058728

Incoming Non-self Citations Over Time

Authors

1. Shumo Chu (University of Washington)
2. Daniel Li (University of Washington)
3. Chenglong Wang (University of Washington)
4. Alvin Cheung (University of Washington)
5. Dan Suciu (University of Washington)

BibTeX Citation

@inproceedings{chu_sigmod17,
        title = {{Demonstration of the Cosette Automated SQL Prover}},
        author = {Chu, Shumo and Li, Daniel and Wang, Chenglong and Cheung, Alvin and Suciu, Dan},
        series = {{SIGMOD} '17},
        booktitle = {Proceedings of the {ACM} {SIGMOD} International Conference on Management of Data},
        publisher = {Association for Computing Machinery},
        doi = {10.1145/3035918.3058728},
        url = {https://dl.acm.org/doi/10.1145/3035918.3058728},
        year = {2017}
}

Incoming Citations (Sorted by Pagerank)

Showing 11 of 11 citing papers.

Rank	Citing Paper	Year	Venue	Pagerank
461	Query-based Workload Forecasting for Self-Driving Database Management Systems	2018	SIGMOD	0.00018068441
1,829	Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries	2018	VLDB	9.6671311e-05
1,892	Procedural Extensions of SQL: Understanding their usage in the wild	2021	VLDB	9.5277793e-05
3,327	Automated Verification of Query Equivalence Using Satisfiability Modulo Theories	2019	VLDB	7.518491e-05
3,769	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD	7.1403543e-05
5,353	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB	6.2519268e-05
7,756	Semantic Conformance Testing of Relational DBMS	2025	VLDB	5.551523e-05
8,465	Predicate Pushdown for Data Science Pipelines	2023	SIGMOD	5.4194578e-05
11,007	GRewriter: Practical Query Rewriting with Automatic Rule Set Expansion in GaussDB	2025	VLDB	5.093636e-05
11,326	Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries	2024	VLDB	5.093636e-05
11,499	Towards Auto-Generated Data Systems	2023	VLDB	5.093636e-05

Outgoing Citations (Sorted by Pagerank)

Showing 5 of 5 cited papers.

Citations counted here include only citations to other VLDB/SIGMOD/CIDR/PODS papers in this database.

Rank	Cited Paper	Year	Venue	Pagerank
17	Provenance Semirings	2007	PODS	0.00059843817
129	Optimization of Nested SQL Queries Revisited	1987	SIGMOD	0.0003068101
910	Cosette: An Automated Prover for SQL	2017	CIDR	0.00013285905
1,037	Cost-Based Optimization for Magic: Algebra and Implementation	1996	SIGMOD	0.00012494928
1,410	Magic is Relevant	1990	SIGMOD	0.00010853223

Semantically Similar Papers

#	Overall Rank	Paper	Year	Venue
1	9,945	ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation	2025	VLDB
2	3,327	Automated Verification of Query Equivalence Using Satisfiability Modulo Theories	2019	VLDB
3	3,769	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD
4	11,489	Demo of QueryBooster: Supporting Middleware-Based SQL Query Rewriting as a Service	2023	VLDB
5	4,733	Interactive Query Synthesis from Input-Output Examples	2017	SIGMOD
6	5,353	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB
7	5,330	ConQuer: A System for Efficient Querying Over Inconsistent Databases	2005	VLDB
8	4,759	Explaining Wrong Queries Using Small Examples	2019	SIGMOD
9	11,326	Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries	2024	VLDB
10	910	Cosette: An Automated Prover for SQL	2017	CIDR