Cosette: An Automated Prover for SQL
Summary: Cosette: automated SQL-equivalence prover that combines SMT solving and theorem proving to output machine-checked proofs or concrete counterexamples. Handles conjunctive/correlated queries, outer joins, and aggregates; validated magic-set rewrites and found real rewrite bugs, advancing provably-correct query optimization. (summarized by gpt-5-mini on Feb 09 2026)
Incoming Non-self Citations Over Time
Authors
- 1. Shumo Chu (University of Washington)
- 2. Chenglong Wang (University of Washington)
- 3. Konstantin Weitz (University of Washington)
- 4. Alvin Cheung (University of Washington)
BibTeX Citation
@inproceedings{chu_cidr17,
address = {Amsterdam, Netherlands},
series = {{CIDR} '17},
title = {{Cosette: An Automated Prover for SQL}},
booktitle = {Proceedings of the {Conference} on {Innovative} {Data} {Systems} {Research}},
author = {Chu, Shumo and Wang, Chenglong and Weitz, Konstantin and Cheung, Alvin},
year = {2017}
}Incoming Citations (Sorted by Pagerank)
Showing 34 of 34 citing papers.
Previous
Page 1 / 1
Next
Outgoing Citations (Sorted by Pagerank)
Showing 7 of 7 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 |
| 290 | An Overview of Query Optimization in Relational Systems | 1998 | PODS | 0.0002227038 |
| 292 | LINQ: Reconciling Objects, Relations and XML in the .NET Framework | 2006 | SIGMOD | 0.00022259549 |
| 517 | Query by Output | 2009 | SIGMOD | 0.00017169735 |
| 1,037 | Cost-Based Optimization for Magic: Algebra and Implementation | 1996 | SIGMOD | 0.00012494928 |
| 1,269 | The Containment Problem for Real Conjunctive Queries with Inequalities | 2006 | PODS | 0.000113935 |
Previous
Page 1 / 1
Next
Semantically Similar Papers
| # | Overall Rank | Paper | Year | Venue |
|---|---|---|---|---|
| 1 | 9,945 | ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation | 2025 | VLDB |
| 2 | 4,759 | Explaining Wrong Queries Using Small Examples | 2019 | SIGMOD |
| 3 | 12,492 | Equivalence of SQL Queries In Presence of Embedded Dependencies | 2009 | PODS |
| 4 | 3,769 | Proving Query Equivalence Using Linear Integer Arithmetic | 2023 | SIGMOD |
| 5 | 1,829 | Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries | 2018 | VLDB |
| 6 | 5,330 | ConQuer: A System for Efficient Querying Over Inconsistent Databases | 2005 | VLDB |
| 7 | 3,327 | Automated Verification of Query Equivalence Using Satisfiability Modulo Theories | 2019 | VLDB |
| 8 | 11,326 | Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries | 2024 | VLDB |
| 9 | 5,353 | QED: A Powerful Query Equivalence Decider for SQL | 2024 | VLDB |
| 10 | 3,172 | Demonstration of the Cosette Automated SQL Prover | 2017 | SIGMOD |