www.semanticscholar.org Open in urlscan Pro
2600:9000:236e:c200:6:4565:580:93a1  Public Scan

Form analysis
3 forms found in the DOM

/search

<form class="search-bar v2-search-bar" id="search-form" role="search" autocomplete="off" action="/search">
  <div class="flex-row-vcenter  input-container">
    <div class="flex-row-vcenter input-bg"><label for="q" class="search-input__label">Search 217,146,488 papers from all fields of science</label><input type="search" name="q" aria-label="Search text"
        class="legacy__input input form-input search-bar__input" value=""><button disabled="" aria-label="Submit" aria-disabled="true" data-test-id="search__form-submit" class="form-submit form-submit__icon-text">
        <div class="flex-row-vcenter"><span class="form-submit-label">Search</span><svg aria-hidden="true" width="13" height="13" alt="" class="icon-svg icon-search-small" data-test-id="icon-search-small">
            <use xlink:href="#search-small"></use>
          </svg></div>
      </button></div>
  </div>
</form>

<form id="citation-search-text-form" class="dropdown-filters__search-within-form" role="search">
  <div class="flex-container search-within"><input type="search" id="search-within-input" autocomplete="off" data-test-id="search-within-input" class="cl-text-input dropdown-filters__search-within-input" name="cite_q"
      placeholder="Search authors, publications, venues, fields of study" value=""><button aria-label="Submit" class="form-submit form-submit__icon-text" data-test-id="submit-search-within-input">
      <div class="flex-row-vcenter"><svg aria-hidden="true" width="14" height="14" alt="" class="icon-svg icon-search-small" data-test-id="icon-search-small">
          <use xlink:href="#search-small"></use>
        </svg></div>
    </button></div>
</form>

<form id="citation-search-text-form" class="dropdown-filters__search-within-form" role="search">
  <div class="flex-container search-within"><input type="search" id="search-within-input" autocomplete="off" data-test-id="search-within-input" class="cl-text-input dropdown-filters__search-within-input" name="cite_q"
      placeholder="Search authors, publications, venues, fields of study" value=""><button aria-label="Submit" class="form-submit form-submit__icon-text" data-test-id="submit-search-within-input">
      <div class="flex-row-vcenter"><svg aria-hidden="true" width="14" height="14" alt="" class="icon-svg icon-search-small" data-test-id="icon-search-small">
          <use xlink:href="#search-small"></use>
        </svg></div>
    </button></div>
</form>

Text Content

Skip to search formSkip to main contentSkip to account menu
Semantic ScholarSemantic Scholar's Logo
Search 217,146,488 papers from all fields of science
Search
Sign InCreate Free Account

 * Corpus ID: 12408033


COSETTE: AN AUTOMATED PROVER FOR SQL

@inproceedings{Chu2017CosetteAA,
  title={Cosette: An Automated Prover for SQL},
  author={Shumo Chu and Chenglong Wang and Konstantin Weitz and Alvin Cheung},
  booktitle={Conference on Innovative Data Systems Research},
  year={2017},
  url={https://api.semanticscholar.org/CorpusID:12408033}
}

 * Shumo Chu, Chenglong Wang, +1 author Alvin Cheung
 * Published in Conference on Innovative Data… 2017
 * Computer Science

TLDR

This paper presents C OSETTE, a fully automated prover that can determine the
equivalence of SQL queries, and proves the validity of magic set rewrites, and
various real-world query rewrite errors, including the famous COUNT bug.Expand
View Paper
Save to LibrarySave
Create AlertAlert
Cite
Share
71 Citations
Highly Influential Citations
8
Background Citations
36
Methods Citations
33
View All
 * Figures
 * Topics
 * 71 Citations
 * 35 References
 * Related Papers


FIGURES FROM THIS PAPER

 * 
   figure 1
 * 
   figure 2
 * 
   figure 3
 * 
   figure 4
 * 
   figure 5


TOPICS

AI-Generated

COSETTE (opens in a new tab)Query Equivalence (opens in a new tab)Magic Set
Rewrites (opens in a new tab)XData (opens in a new tab)Mutant Query (opens in a
new tab)SQL Queries (opens in a new tab)Query (opens in a new tab)COUNT Bug
(opens in a new tab)Conjunctive Queries (opens in a new tab)Structured Query
Language (opens in a new tab)


71 CITATIONS

Date Range

Citation Type

Has PDF
Author

More Filters
More Filters
Filters
Sort by RelevanceSort by Most Influenced PapersSort by Citation CountSort by
Recency


AXIOMATIC FOUNDATIONS AND ALGORITHMS FOR DECIDING SEMANTIC EQUIVALENCES OF SQL
QUERIES

   Shumo ChuAlvin CheungDan Suciu
   Computer Science
   Proceedings of the VLDB Endowment
 * 2018

TLDR

A new formalism and implementation, U-semiring, extends SQL's semiring semantics
with unbounded summation and duplicate elimination and is used to formally
verify 68 equivalent queries and rewrite rules from both classical data
management research papers and real-world SQL engines, where many of them have
never been proven correct before.Expand
 * 39
 * Highly Influenced
   [PDF]

 * 4 Excerpts

Save



LLM-SQL-SOLVER: CAN LLMS DETERMINE SQL EQUIVALENCE?

   Fuheng ZhaoLawrence LimIshtiyaque AhmadD. AgrawalA. E. Abbadi
   Computer Science, Mathematics
   arXiv.org
 * 2023

TLDR

Using two prompting techniques, LLMs is a promising tool to help data engineers
in writing semantically equivalent SQL queries, however challenges still
persist, and is a better metric for evaluating SQL generation than the popular
execution accuracy.Expand
 * Highly Influenced
   [PDF]

 * 8 Excerpts

Save



SPEEDING UP SYMBOLIC REASONING FOR RELATIONAL QUERIES

   Chenglong WangAlvin CheungRastislav Bodík
   Computer Science
   Proc. ACM Program. Lang.
 * 2018

TLDR

This work proposes a space refinement algorithm that soundly reduces the space
of tables such applications need to consider and significantly speeds up the SQL
solver when reasoning about a large class of challenging SQL queries, such as
those with aggregations.Expand
 * 10
 * Highly Influenced
 * PDF

 * 25 Excerpts

Save



DEMONSTRATION OF THE COSETTE AUTOMATED SQL PROVER

   Shumo ChuD. LiChenglong WangAlvin CheungDan Suciu
   Computer Science
   SIGMOD Conference
 * 2017

TLDR

This demonstration showcases COSETTE, the first automated prover for determining
the equivalences of SQL queries, and showcases three representative applications
of CosETTE: proving a query rewrite rule from magic set rewrite, finding counter
examples from the infamous optimizer bug, and an interactive visualization of
automated grading results powered by COSetTE.Expand
 * 17
 * PDF

 * 2 Excerpts

Save



HOTTSQL: PROVING QUERY REWRITES WITH UNIVALENT SQL SEMANTICS

   Shumo ChuKonstantin WeitzAlvin CheungDan Suciu
   Computer Science
   ACM-SIGPLAN Symposium on Programming Language…
 * 2017

TLDR

A machine-checkable denotational semantics for SQL, the de facto language for
relational database, for rigorously validating rewrite rules and an automated
decision procedure using HoTTSQL for conjunctive queries: a well studied
decidable fragment of SQL that encompasses many real-world queries.Expand
 * 63
   [PDF]

 * 1 Excerpt

Save



WETUNE: AUTOMATIC DISCOVERY AND VERIFICATION OF QUERY REWRITE RULES

   Zhaoguo WangZ. Zhou+6 authors Jinyang Li
   Computer Science
   SIGMOD Conference
 * 2022

TLDR

This paper presents WeTune, a rule generator that automatically discovers new
rewrite rules and proposes a new SMT-based verifier to verify the equivalence of
a query pair under different enumerated constraints.Expand
 * 16
 * PDF

Save



PROVING QUERY EQUIVALENCE USING LINEAR INTEGER ARITHMETIC

   Haoran DingZhaoguo Wang+5 authors Jinyang Li
   Computer Science, Mathematics
   Proc. ACM Manag. Data
 * 2023

TLDR

A new SQL equivalence prover called SQLSolver is developed, which can handle
unbounded summations in a principled way and significantly outperforms existing
provers.Expand
 * 1 Excerpt

Save



SYNTHESIZING HIGHLY EXPRESSIVE SQL QUERIES FROM INPUT-OUTPUT EXAMPLES

   Chenglong WangAlvin CheungRastislav Bodík
   Computer Science
   ACM-SIGPLAN Symposium on Programming Language…
 * 2017

TLDR

A new scalable and efficient algorithm for synthesizing SQL queries based on I/O
examples that develops a language for abstract queries, i.e., queries with
uninstantiated operators, that can be used to express a large space of SQL
queries efficiently.Expand
 * 172
 * PDF

 * 1 Excerpt

Save



A FORMAL SEMANTICS OF SQL QUERIES, ITS VALIDATION, AND APPLICATIONS

   P. GuagliardoL. Libkin
   Computer Science
   Proceedings of the VLDB Endowment
 * 2017

TLDR

The first formal proof of the equivalence of basic SQL and relational algebra
that extends to bag semantics and nulls is given, and it is proved that
three-valued logic employed by SQL does not add expressive power, as every SQL
query can be evaluated under the usual two-valued Boolean semantics of
conditions.Expand
 * 42
 * PDF

 * 2 Excerpts

Save



CUBES: A PARALLEL SYNTHESIZER FOR SQL USING EXAMPLES

   Ricardo BrancasMiguel Terra-NevesM. VenturaVasco M. ManquinhoR. Martins
   Computer Science
   arXiv.org
 * 2022

TLDR

CUBES incorporates a new disambiguation procedure based on fuzzing techniques
that interacts with the user and increases the confidence that the returned
query matches the user intent, and can solve more instances than other
state-of-the-art SQL synthesizers.Expand
 * 1
   [PDF]

 * 2 Excerpts

Save

...
1
2
3
4
5
...



35 REFERENCES

Citation Type

Has PDF
Author

More Filters
More Filters
Filters
Sort by RelevanceSort by Most Influenced PapersSort by Citation CountSort by
Recency


THE CONTAINMENT PROBLEM FOR REAL CONJUNCTIVE QUERIES WITH INEQUALITIES

   T. S. JayramPhokion G. KolaitisErik Vee
   Computer Science, Mathematics
   ACM SIGACT-SIGMOD-SIGART Symposium on Principles…
 * 2006

TLDR

This work investigates, under bag semantics, the query-containment problem for
conjunctive queries with inequalities, and asserts that this problem is
undecidability results hold under bag-set semantics.Expand
 * 71
 * PDF

 * 1 Excerpt

Save



HOTTSQL: PROVING QUERY REWRITES WITH UNIVALENT SQL SEMANTICS

   Shumo ChuKonstantin WeitzAlvin CheungDan Suciu
   Computer Science
   ACM-SIGPLAN Symposium on Programming Language…
 * 2017

TLDR

A machine-checkable denotational semantics for SQL, the de facto language for
relational database, for rigorously validating rewrite rules and an automated
decision procedure using HoTTSQL for conjunctive queries: a well studied
decidable fragment of SQL that encompasses many real-world queries.Expand
 * 63
   [PDF]

 * 2 Excerpts

Save



EQUIVALENCES AMONG RELATIONAL EXPRESSIONS WITH THE UNION AND DIFFERENCE
OPERATORS

   Y. SagivM. Yannakakis
   Computer Science, Mathematics
   Journal of the ACM
 * 1980

TLDR

It is shown that containment of tableaux is a necessary step in testing
equivalence of queries with union and difference, and the containment problem is
shown to be NP-complete even for tableaux that correspond to expressions with
only one project and several join operators.Expand
 * 384
 * PDF

 * 2 Excerpts

Save



OPTIMIZING DATABASE-BACKED APPLICATIONS WITH QUERY SYNTHESIS

   Alvin CheungArmando Solar-LezamaS. Madden
   Computer Science
   ACM-SIGPLAN Symposium on Programming Language…
 * 2013

TLDR

This paper presents QBS, a system that automatically transforms fragments of
application logic into SQL queries, and demonstrates that this approach can
convert a variety of imperative constructs into relational specifications and
significantly improve application performance asymptotically by orders of
magnitude.Expand
 * 143
 * PDF

 * 2 Excerpts

Save



OPTIMIZATION OF NESTED SQL QUERIES REVISITED

   Richard A. GanskiH. Wong
   Computer Science
   ACM SIGMOD Conference
 * 1987

TLDR

Previous research in the area of nested query optimization which sought methods
of reducing evaluation costs is summarized, including a classification scheme
for nested queries, algorithms designed to transform each type of query to a
logically equivalent form which may then be evaluated more efficiently.Expand
 * 216
 * PDF

 * 3 Excerpts

Save



GENERATING TEST DATA FOR KILLING SQL MUTANTS: A CONSTRAINT-BASED APPROACH

   Shetal ShahS. SudarshanSuhas KajbajeS. PatidarB. P. GuptaDevang Vira
   Computer Science
   IEEE International Conference on Data Engineering
 * 2011

TLDR

This paper addresses the problem of test data generation for checking
correctness of SQL queries, based on the query mutation approach for modeling
errors, and focuses in particular on a class of join/outer-join mutations,
comparison operator mutations, and aggregation operation mutations, which are a
common cause of error.Expand
 * 41
 * PDF

 * 3 Excerpts

Save



COST-BASED OPTIMIZATION FOR MAGIC: ALGEBRA AND IMPLEMENTATION

   P. SeshadriJ. Hellerstein+5 authors S. Sudarshan
   Computer Science, Mathematics
   ACM SIGMOD Conference
 * 1996

TLDR

A practical scheme that models magic sets rewriting as a special join method
that can be added to any cost-based query optimizer, and a formal algebraic
model based on an extension of the multiset relational algebra, which cleanly
defines the search space and can be used in a rule-based optimizer.Expand
 * 108
 * PDF

 * 2 Excerpts

Save



QUERY BY OUTPUT

   Quoc Trung TranC. ChanS. Parthasarathy
   Computer Science
   SIGMOD Conference
 * 2009

TLDR

This paper presents a novel data-driven approach, called Query By Output (QBO),
which can enhance the usability of database systems and designs several
optimization techniques to reduce processing overhead and introduce a set of
criteria to rank order output queries by various notions of utility.Expand
 * 149
 * PDF

 * 1 Excerpt

Save



QEX: SYMBOLIC SQL QUERY EXPLORER

   Margus VeanesN. TillmannJ. D. Halleux
   Computer Science, Mathematics
   Logic Programming and Automated Reasoning
 * 2010

TLDR

A technique and a tool called Qex for generating input tables and parameter
values for a given parameterized SQL query and an evaluation of its performance
is provided.Expand
 * 58
 * PDF

 * 3 Excerpts

Save



FOUNDATIONS OF DATABASES

   S. AbiteboulR. HullV. Vianu
   Computer Science, Mathematics
 * 1994

TLDR

This book discusses Languages, Computability, and Complexity, and the Relational
Model, which aims to clarify the role of Semantic Data Models in the development
of Query Language Design.Expand
 * 4,463
 * PDF

Save

...
1
2
3
4
...



RELATED PAPERS

Showing 1 through 3 of 0 Related Papers


Stay Connected With Semantic Scholar
Sign Up


WHAT IS SEMANTIC SCHOLAR?

Semantic Scholar is a free, AI-powered research tool for scientific literature,
based at the Allen Institute for AI.

Learn More


ABOUT

About UsMeet the TeamPublishersBlog (opens in a new tab)AI2 Careers (opens in a
new tab)


PRODUCT

Product OverviewSemantic ReaderScholar's HubBeta ProgramRelease Notes


API

API OverviewAPI TutorialsAPI Documentation (opens in a new tab)API Gallery


RESEARCH

PublicationsResearchersResearch CareersPrototypesResources


HELP

FAQLibrariansTutorialsContact
Proudly built by AI2 (opens in a new tab)
Collaborators & Attributions •Terms of Service (opens in a new tab)•Privacy
Policy (opens in a new tab)•API License Agreement
The Allen Institute for AI (opens in a new tab)

By clicking accept or continuing to use the site, you agree to the terms
outlined in our Privacy Policy (opens in a new tab), Terms of Service (opens in
a new tab), and Dataset License (opens in a new tab)
ACCEPT & CONTINUE