Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/789
Title: Verification supported refactoring of embedded sql
Authors: Spasić, Mirko 
Vujošević Janičić, Milena 
Affiliations: Informatics and Computer Science 
Informatics and Computer Science 
Keywords: Bounded model checking;Embedded sql;Regression verification;SMT solving;Software verification
Issue Date: 2021
Journal: Software Quality Journal
Abstract: 
Improving 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.
URI: https://research.matf.bg.ac.rs/handle/123456789/789
ISSN: 09639314
DOI: 10.1007/s11219-020-09517-y
Appears in Collections:Research outputs

Show full 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.