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: 5363
Venue: SIGMOD
Year: 2017
Pagerank: 7.0985442e-05
Overall Rank: 3,430 | 76.17%
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
704	Query-based Workload Forecasting for Self-Driving Database Management Systems	2018	SIGMOD	0.00017785557
2,097	Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries	2018	VLDB	9.5439744e-05
2,242	Procedural Extensions of SQL: Understanding their usage in the wild	2021	VLDB	9.2124242e-05
3,903	Automated Verification of Query Equivalence Using Satisfiability Modulo Theories	2019	VLDB	6.6439695e-05
4,385	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD	6.2247394e-05
5,245	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB	5.6017846e-05
7,724	Semantic Conformance Testing of Relational DBMS	2025	VLDB	4.6622637e-05
8,625	Predicate Pushdown for Data Science Pipelines	2023	SIGMOD	4.4784651e-05
10,784	GRewriter: Practical Query Rewriting with Automatic Rule Set Expansion in GaussDB	2025	VLDB	4.1905499e-05
11,123	Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries	2024	VLDB	4.1905499e-05
11,302	Towards Auto-Generated Data Systems	2023	VLDB	4.1905499e-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.00078516827
130	Optimization of Nested SQL Queries Revisited	1987	SIGMOD	0.00044001626
1,056	Cosette: An Automated Prover for SQL	2017	CIDR	0.00014391317
1,313	Cost-Based Optimization for Magic: Algebra and Implementation	1996	SIGMOD	0.00012629432
1,423	Magic is Relevant	1990	SIGMOD	0.00012047765

Semantically Similar Papers

Overall Rank	Paper	Year	Venue	Pagerank
10,768	ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation	2025	VLDB	4.1905499e-05
3,903	Automated Verification of Query Equivalence Using Satisfiability Modulo Theories	2019	VLDB	6.6439695e-05
4,385	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD	6.2247394e-05
11,292	Demo of QueryBooster: Supporting Middleware-Based SQL Query Rewriting as a Service	2023	VLDB	4.1905499e-05
5,245	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB	5.6017846e-05
4,982	Interactive Query Synthesis from Input-Output Examples	2017	SIGMOD	5.7817493e-05
5,394	ConQuer : A System for Efficient Querying Over Inconsistent Databases	2005	VLDB	5.5312682e-05
5,743	Explaining Wrong Queries Using Small Examples	2019	SIGMOD	5.3432106e-05
11,123	Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries	2024	VLDB	4.1905499e-05
1,056	Cosette: An Automated Prover for SQL	2017	CIDR	0.00014391317