| LDR | | 00000nam u2200205 4500 |
| 001 | | 000000432416 |
| 005 | | 20200224125415 |
| 008 | | 200131s2019 ||||||||||||||||| ||eng d |
| 020 | |
▼a 9781088329412 |
| 035 | |
▼a (MiAaPQ)AAI13902656 |
| 040 | |
▼a MiAaPQ
▼c MiAaPQ
▼d 247004 |
| 082 | 0 |
▼a 620 |
| 100 | 1 |
▼a Chu, Shumo. |
| 245 | 10 |
▼a Automated Reasoning of Database Queries. |
| 260 | |
▼a [S.l.]:
▼b University of Washington.,
▼c 2019. |
| 260 | 1 |
▼a Ann Arbor:
▼b ProQuest Dissertations & Theses,
▼c 2019. |
| 300 | |
▼a 138 p. |
| 500 | |
▼a Source: Dissertations Abstracts International, Volume: 81-04, Section: B. |
| 500 | |
▼a Advisor: Suciu, Dan. |
| 502 | 1 |
▼a Thesis (Ph.D.)--University of Washington, 2019. |
| 506 | |
▼a This item must not be sold to any third party vendors. |
| 506 | |
▼a This item must not be added to any third party search indexes. |
| 520 | |
▼a From booking air tickets to analyzing astronomy datasets, database queries are pervasive in people's work and life. This thesis describes Cosette, the first tool for automated reasoning the equivalences of SQL queries.The core of Cosette is a formal semantics of SQL based on semirings. This semantics covers major SQL features, including sophisticated ones such as grouping, aggregate, correlated sub- queries, and integrity constraints. Also, this semantics is denotational and only adds a few equational axioms, as the interpretation of SQL, to semirings. Then, to check the equivalences, Cosette uses this semantics to encode a pair of input SQL queries in both an interactive theorem prover and a constraint solver. In the end, Cosette will either certify their equivalences using a sound decision procedure implemented in a theorem prover that covers the known decidable fragment of SQL, or show their inequivalence by providing a counter-example. Empirical studies show that Cosette can decide the equivalence or provide counter example for a wide range of practical SQL queries collected from database literature, real-world optimizer rules and bugs, and data management class homework assignment from UW. |
| 590 | |
▼a School code: 0250. |
| 650 | 4 |
▼a Computer science. |
| 650 | 4 |
▼a Information technology. |
| 690 | |
▼a 0984 |
| 690 | |
▼a 0489 |
| 710 | 20 |
▼a University of Washington.
▼b Computer Science and Engineering. |
| 773 | 0 |
▼t Dissertations Abstracts International
▼g 81-04B. |
| 773 | |
▼t Dissertation Abstract International |
| 790 | |
▼a 0250 |
| 791 | |
▼a Ph.D. |
| 792 | |
▼a 2019 |
| 793 | |
▼a English |
| 856 | 40 |
▼u http://www.riss.kr/pdu/ddodLink.do?id=T15492391
▼n KERIS
▼z 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
| 980 | |
▼a 202002
▼f 2020 |
| 990 | |
▼a ***1008102 |
| 991 | |
▼a E-BOOK |