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 37 of 37 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.00059752575 |
| 132 | Optimization of Nested SQL Queries Revisited | 1987 | SIGMOD | 0.00030241193 |
| 272 | An Overview of Query Optimization in Relational Systems | 1998 | PODS | 0.00022509573 |
| 292 | LINQ: Reconciling Objects, Relations and XML in the .NET Framework | 2006 | SIGMOD | 0.00021947834 |
| 518 | Query by Output | 2009 | SIGMOD | 0.00016944862 |
| 1,032 | Cost-Based Optimization for Magic: Algebra and Implementation | 1996 | SIGMOD | 0.00012401489 |
| 1,275 | The Containment Problem for Real Conjunctive Queries with Inequalities | 2006 | PODS | 0.00011242154 |
Previous
Page 1 / 1
Next
Semantically Similar Papers
| # | Overall Rank | Paper | Year | Venue |
|---|---|---|---|---|
| 1 | 10,129 | ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation | 2025 | VLDB |
| 2 | 4,847 | Explaining Wrong Queries Using Small Examples | 2019 | SIGMOD |
| 3 | 12,782 | Equivalence of SQL Queries In Presence of Embedded Dependencies | 2009 | PODS |
| 4 | 2,961 | Proving Query Equivalence Using Linear Integer Arithmetic | 2023 | SIGMOD |
| 5 | 1,680 | Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries | 2018 | VLDB |
| 6 | 5,460 | ConQuer: A System for Efficient Querying Over Inconsistent Databases | 2005 | VLDB |
| 7 | 3,297 | Automated Verification of Query Equivalence Using Satisfiability Modulo Theories | 2019 | VLDB |
| 8 | 11,644 | Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries | 2024 | VLDB |
| 9 | 4,102 | QED: A Powerful Query Equivalence Decider for SQL | 2024 | VLDB |
| 10 | 3,202 | Demonstration of the Cosette Automated SQL Prover | 2017 | SIGMOD |