| dc.contributor.advisor |
Vujošević Janičić, Milena |
|
| dc.contributor.author |
Spasić, Mirko |
|
| dc.date.accessioned |
2021-01-14T09:12:43Z |
|
| dc.date.available |
2021-01-14T09:12:43Z |
|
| dc.date.issued |
2020 |
|
| dc.identifier.uri |
http://hdl.handle.net/123456789/5095 |
|
| dc.description.abstract |
The query containment problem is a very important computer science problem,originally defined for relational queries. With the growing popularity of theSPARQLquerylanguage, it became relevant and important in this new context, too. This thesis introducesa new approach for solving this problem, based on a reduction to satisfiability in first orderlogic. The approach covers containment underRDF SCHEMAentailment regime, and it candeal with the subsumption relation, as a weaker form of containment. The thesis provessoundness and completeness of the approach for a wide range of language constructs. It alsodescribes an implementation of the approach as an open source solverSPECS. The experi-mental evaluation on relevant benchmarks shows thatSPECSis efficient and comparing tostate-of-the-art solvers, it gives more precise results in a shorter amount of time, while suppor-ting a larger fragment ofSPARQLconstructs. An application of query language modeling canbe useful also along refactoring of database driven applications, where simultaneous changesthat include both a query and a host language code are very common. These changes canpreserve the overall equivalence, without preserving equivalence of these two parts consideredseparately. Because of the ability to guarantee the absence of differences in behavior betweentwo versions of the code, tools that automatically verify code equivalence have great benefitsfor reliable software development. With this motivation, a custom first-order logic modelingof SQL queries is developed and described in the thesis. It enables an automated approachfor reasoning about equivalence ofC/C++programs with embedded SQL. The approach is implemented within a publicly available and open source framework SQLAV. |
en_US |
| dc.description.provenance |
Submitted by Slavisha Milisavljevic (slavisha) on 2021-01-14T09:12:43Z
No. of bitstreams: 1
doktoratMirkoSpasic.pdf: 1258450 bytes, checksum: 507e39ff2774e7c5ee736e8cb793b59a (MD5) |
en |
| dc.description.provenance |
Made available in DSpace on 2021-01-14T09:12:43Z (GMT). No. of bitstreams: 1
doktoratMirkoSpasic.pdf: 1258450 bytes, checksum: 507e39ff2774e7c5ee736e8cb793b59a (MD5)
Previous issue date: 2020 |
en |
| dc.language.iso |
sr |
en_US |
| dc.publisher |
Beograd |
en_US |
| dc.title |
MODELOVANJE UPITNIH JEZIKA SA PRIMENAMA U REFAKTORISANJU I OPTIMIZACIJI KODA |
en_US |
| mf.author.birth-date |
1985-03-01 |
|
| mf.author.birth-place |
Brus |
en_US |
| mf.author.birth-country |
Srbija |
en_US |
| mf.author.residence-state |
Srbija |
en_US |
| mf.author.citizenship |
Srpsko |
en_US |
| mf.author.nationality |
Srbin |
en_US |
| mf.subject.area |
Computer Science |
en_US |
| mf.subject.keywords |
software verification,SPARQL, query containment,FOL modeling,SMT solving,SPECSsolver, embeddedSQL, code refactoring,SQLAV framew |
en_US |
| mf.subject.subarea |
oftware specification and verification |
en_US |
| mf.contributor.committee |
Mitić, Nenad |
|
| mf.contributor.committee |
Marić, Filip |
|
| mf.contributor.committee |
Gilezan, Silvija |
|
| mf.university.faculty |
Mathematical faculty |
en_US |
| mf.document.references |
206 |
en_US |
| mf.document.pages |
161 |
en_US |
| mf.document.location |
Belgrade |
en_US |
| mf.document.genealogy-project |
No |
en_US |
| mf.university |
Belgrade University |
en_US |