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: 5362
Venue: SIGMOD
Year: 2017
Pagerank: 7.1008151e-05
Overall Rank: 3,432 | 76.13%
DOI: 10.1145/3035918.3058728

Incoming Non-self Citations Over Time

Authors

Incoming Citations (Sorted by Pagerank)

Showing 11 of 11 citing papers.

Rank	Citing Paper	Year	Venue	Pagerank
716	Query-based Workload Forecasting for Self-Driving Database Management Systems	2018	SIGMOD	0.00017723171
2,099	Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries	2018	VLDB	9.5479391e-05
2,237	Procedural Extensions of SQL: Understanding their usage in the wild	2021	VLDB	9.2212748e-05
3,901	Automated Verification of Query Equivalence Using Satisfiability Modulo Theories	2019	VLDB	6.6499845e-05
4,388	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD	6.2303078e-05
5,243	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB	5.6071695e-05
7,726	Semantic Conformance Testing of Relational DBMS	2025	VLDB	4.6667388e-05
8,645	Predicate Pushdown for Data Science Pipelines	2023	SIGMOD	4.4772518e-05
10,778	GRewriter: Practical Query Rewriting with Automatic Rule Set Expansion in GaussDB	2025	VLDB	4.1945683e-05
11,120	Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries	2024	VLDB	4.1945683e-05
11,300	Towards Auto-Generated Data Systems	2023	VLDB	4.1945683e-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
31	Provenance Semirings	2007	PODS	0.0007857786
130	Optimization of Nested SQL Queries Revisited	1987	SIGMOD	0.00044031247
1,057	Cosette: An Automated Prover for SQL	2017	CIDR	0.0001439886
1,313	Cost-Based Optimization for Magic: Algebra and Implementation	1996	SIGMOD	0.0001263831
1,423	Magic is Relevant	1990	SIGMOD	0.00012054867

Semantically Similar Papers

Overall Rank	Paper	Year	Venue	Pagerank
10,762	ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation	2025	VLDB	4.1945683e-05
3,901	Automated Verification of Query Equivalence Using Satisfiability Modulo Theories	2019	VLDB	6.6499845e-05
4,388	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD	6.2303078e-05
11,290	Demo of QueryBooster: Supporting Middleware-Based SQL Query Rewriting as a Service	2023	VLDB	4.1945683e-05
5,243	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB	5.6071695e-05
4,980	Interactive Query Synthesis from Input-Output Examples	2017	SIGMOD	5.7873101e-05
5,389	ConQuer : A System for Efficient Querying Over Inconsistent Databases	2005	VLDB	5.5368328e-05
5,733	Explaining Wrong Queries Using Small Examples	2019	SIGMOD	5.3483446e-05
11,120	Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries	2024	VLDB	4.1945683e-05
1,057	Cosette: An Automated Prover for SQL	2017	CIDR	0.0001439886