Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/789
DC FieldValueLanguage
dc.contributor.authorSpasić, Mirkoen_US
dc.contributor.authorVujošević Janičić, Milenaen_US
dc.date.accessioned2022-08-15T15:39:07Z-
dc.date.available2022-08-15T15:39:07Z-
dc.date.issued2021-
dc.identifier.issn09639314-
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/789-
dc.description.abstractImproving code quality without changing its functionality, e.g., by refactoring or optimization, is an everyday programming activity. Good programming practice requires that each such change should be followed by a check if the change really preserves the code behavior. If such a check is performed by testing, it can be time consuming and still cannot guarantee the absence of differences in behavior between two versions of the code. Hence, tools that could automatically verify code equivalence would be of great help. An area that we are focused on is embedded sql programming. There are a number of approaches for dealing with equivalence of either pairs of imperative code fragments or pairs of sql statements. However, in database-driven applications, simultaneous changes (changes that include both sql and a host language code) are also present and important. Such changes can preserve the overall equivalence without preserving equivalence of these two parts considered separately. In this paper, we propose an automated approach for dealing with equivalence of programs after such changes, a problem that is hardly tackled in literature. Our approach uses our custom first-order logic modeling of sql queries that corresponds to imperative semantics. The approach generates equivalence conditions that can be efficiently checked using smt solvers or first-order logic provers. We implemented the proposed approach as a framework sqlav, which is publicly available and open source.en_US
dc.relation.ispartofSoftware Quality Journalen_US
dc.subjectBounded model checkingen_US
dc.subjectEmbedded sqlen_US
dc.subjectRegression verificationen_US
dc.subjectSMT solvingen_US
dc.subjectSoftware verificationen_US
dc.titleVerification supported refactoring of embedded sqlen_US
dc.typeArticleen_US
dc.identifier.doi10.1007/s11219-020-09517-y-
dc.identifier.scopus2-s2.0-85086670462-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/85086670462-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.lastpage665en_US
dc.relation.volume29en_US
dc.relation.issue3en_US
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeArticle-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0002-9304-4007-
crisitem.author.orcid0000-0001-5396-0644-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

1
checked on Dec 20, 2024

Page view(s)

23
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.