{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T09:13:53Z","timestamp":1778663633558,"version":"3.51.4"},"reference-count":100,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,6,18]],"date-time":"2020-06-18T00:00:00Z","timestamp":1592438400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,18]],"date-time":"2020-06-18T00:00:00Z","timestamp":1592438400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Serbian Ministry of Science","award":["174021"],"award-info":[{"award-number":["174021"]}]},{"name":"COST action","award":["CA15123"],"award-info":[{"award-number":["CA15123"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1007\/s11219-020-09517-y","type":"journal-article","created":{"date-parts":[[2020,6,18]],"date-time":"2020-06-18T07:02:46Z","timestamp":1592463766000},"page":"629-665","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verification supported refactoring of embedded sql"],"prefix":"10.1007","volume":"29","author":[{"given":"Mirko","family":"Spasi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milena Vujo\u0161evi\u0107","family":"Jani\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,18]]},"reference":[{"key":"9517_CR1","unstructured":"Abiteboul, S., Hull, R., & Vianu, V. (Eds.). (1995). Foundations of databases: the logical level. Boston: Addison-Wesley."},{"key":"9517_CR2","unstructured":"Altibase. (2020). Altibase enterprise grade open source database. http:\/\/altibase.com\/."},{"key":"9517_CR3","doi-asserted-by":"publisher","unstructured":"Amtoft, T., Bandhakavi, S., & Banerjee, A. (2006). A logic for information flow in object-oriented programs. In POPL, pp. 91\u2013102. ACM. https:\/\/doi.org\/10.1145\/1111037.1111046.","DOI":"10.1145\/1111037.1111046"},{"key":"9517_CR4","doi-asserted-by":"publisher","unstructured":"Auerbach, J. S., Hirzel, M., Mandel, L., Shinnar, A., & Sim\u00e9on, J. (2017). Handling env. in a nested relational algebra with combinators and an implementation in a verified query compiler. In SIGMOD, pp. 1555\u20131569. ACM. https:\/\/doi.org\/10.1145\/3035918.3035961.","DOI":"10.1145\/3035918.3035961"},{"key":"9517_CR5","doi-asserted-by":"publisher","unstructured":"Babic, D., & Hu, A. J. (2008). Calysto: scalable and precise extended static checking. In ICSE, pp. 211\u2013220. ACM. https:\/\/doi.org\/10.1145\/1368088.1368118.","DOI":"10.1145\/1368088.1368118"},{"key":"9517_CR6","doi-asserted-by":"publisher","unstructured":"Backes, J., Person, S., Rungta, N., & Tkachuk, O. (2013). Regression verification using impact summaries. In SPIN, pp. 99\u2013116. https:\/\/doi.org\/10.1007\/978-3-642-39176-7_7.","DOI":"10.1007\/978-3-642-39176-7_7"},{"key":"9517_CR7","doi-asserted-by":"publisher","unstructured":"Barnett, M., & Leino, R. (2005). Weakest-precondition of unstructured programs. In Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 82\u201387. ACM. https:\/\/doi.org\/10.1145\/1108792.1108813.","DOI":"10.1145\/1108792.1108813"},{"key":"9517_CR8","unstructured":"Barrett, C., Sebastiani, R., Seshia, S. A., & Tinelli, C. (2009). Satisfiability modulo theories. In Handbook of satisfiability, vol. 185, pp. 825\u2013885. IOS press."},{"key":"9517_CR9","unstructured":"Barrett, C., Stump, A., & Tinelli, C. (2010). The SMT-LIB standard: Version 2.0. Tech. rep., Department of computer science, The University of Iowa. Available at www.SMT-LIB.org, retrieved September 22nd, (2019)."},{"key":"9517_CR10","doi-asserted-by":"crossref","unstructured":"Barrett, C., & Tinelli, C. (2018). Satisfiability modulo theories. In Handbook of model checking, pp. 305\u2013343. Springer.","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"9517_CR11","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u0117goire, B., Kunz, C., Lakhnech, Y., & B\u0117guelin, S. Z. (2012). Automation in computer-aided cryptography: Proofs, attacks and designs. In CPP, pp. 7\u20138. https:\/\/doi.org\/10.1007\/978-3-642-35308-6_3.","DOI":"10.1007\/978-3-642-35308-6_3"},{"key":"9517_CR12","volume-title":"Learning SQL","author":"A Beaulieu","year":"2009","unstructured":"Beaulieu, A. (2009). Learning SQL, 2nd edn. Newton: O\u2019Reilly Media, Inc.","edition":"2nd edn."},{"key":"9517_CR13","unstructured":"Ben-Gan, I. (2012). Microsoft SQL server 2012 t-SQL fundamentals. Pearson Education."},{"key":"9517_CR14","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Konstantinidis, G., Mecca, G., Motik, B., Papotti, P., Santoro, D., & Tsamoura, E. (2017). Benchmarking the chase. In PODS, pp. 37\u201352. ACM. https:\/\/doi.org\/10.1145\/3034786.3034796.","DOI":"10.1145\/3034786.3034796"},{"key":"9517_CR15","doi-asserted-by":"publisher","unstructured":"Benzaken, V., & Contejean, E. (2019). A coq mechanised formal semantics for realistic sql queries: formally reconciling sql and bag relational algebra. In CPP, pp. 249\u2013261. ACM. https:\/\/doi.org\/10.1145\/3293880.3294107.","DOI":"10.1145\/3293880.3294107"},{"key":"9517_CR16","doi-asserted-by":"publisher","unstructured":"Benzaken, V., Contejean, \u00c9. , Keller, C., & Martins, E. (2018). A Coq formalisation of SQL\u2019s execution engines. In Avigad, J., Mahboubi, A., & Interactive theorem proving (Eds.) https:\/\/doi.org\/10.1007\/978-3-319-94821-8_6 (pp. 88\u2013107): Springer.","DOI":"10.1007\/978-3-319-94821-8_6"},{"key":"9517_CR17","doi-asserted-by":"publisher","unstructured":"Bertot, Y., & Castran, P. (2010). Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions springer. https:\/\/doi.org\/10.1007\/978-3-662-07964-5.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9517_CR18","unstructured":"Blome, M., Robertson, C., Cai, S., Jones, M., Sebolt, M., & Hogenson, G. (2020). Open database connectivity (ODBC), Microsoft Docs. https:\/\/docs.microsoft.com\/en-us\/cpp\/data\/odbc\/open-database-connectivity-odbc?view=vs-2019 retrieved March 5th."},{"key":"9517_CR19","doi-asserted-by":"crossref","unstructured":"Brumm, B. (2019). Beginning oracle SQL for oracle database 18c. Springer.","DOI":"10.1007\/978-1-4842-4430-2"},{"issue":"4","key":"9517_CR20","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1109\/TSE.1985.232223","volume":"11","author":"S Ceri","year":"1985","unstructured":"Ceri, S., & Gottlob, G. (1985). Translating sql into relational algebra: optimization, semantics, and equivalence of sql queries. IEEE Transactions on Software Engineering, 11(4), 324\u2013345. https:\/\/doi.org\/10.1109\/TSE.1985.232223.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9517_CR21","doi-asserted-by":"publisher","unstructured":"Chandra, A. K., & Merlin, P. M. (1977). Optimal implementation of conjunctive queries in relational data bases. In STOC, pp. 77\u201390. ACM. https:\/\/doi.org\/10.1145\/800105.803397.","DOI":"10.1145\/800105.803397"},{"key":"9517_CR22","doi-asserted-by":"publisher","unstructured":"Chaudhuri, S., & Vardi, M. Y. (1993). Optimization of real conjunctive queries. In PODS, pp. 59\u201370. ACM. https:\/\/doi.org\/10.1145\/153850.153856.","DOI":"10.1145\/153850.153856"},{"issue":"3","key":"9517_CR23","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1016\/j.jcss.2015.11.001","volume":"82","author":"R Chirkova","year":"2016","unstructured":"Chirkova, R. (2016). Combined-semantics equivalence of conjunctive queries: decidability and tractability results. Journal of Computer and System Sciences, 82(3), 395\u2013465. https:\/\/doi.org\/10.1016\/j.jcss.2015.11.001.","journal-title":"Journal of Computer and System Sciences"},{"issue":"11","key":"9517_CR24","doi-asserted-by":"publisher","first-page":"1482","DOI":"10.14778\/3236187.3236200","volume":"11","author":"S Chu","year":"2018","unstructured":"Chu, S., Murphy, B., Roesch, J., Cheung, A., & Suciu, D. (2018). Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries. Proc. VLDB Endow., 11(11), 1482\u20131495. https:\/\/doi.org\/10.14778\/3236187.3236200.","journal-title":"Proc. VLDB Endow."},{"issue":"6","key":"9517_CR25","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1145\/3140587.3062348","volume":"52","author":"S Chu","year":"2017","unstructured":"Chu, S., Weitz, K., Cheung, A., & Suciu, D. (2017). Hottsql: Proving query rewrites with univalent sql semantics. SIGPLAN Not., 52(6), 510\u2013524. https:\/\/doi.org\/10.1145\/3140587.3062348.","journal-title":"SIGPLAN Not."},{"key":"9517_CR26","doi-asserted-by":"publisher","unstructured":"Clarke, E., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-c programs. In TACAS, pp. 168\u2013176. Springer. https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"9517_CR27","doi-asserted-by":"publisher","unstructured":"Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (Eds.). (2018). Handbook of model checking. Berlin: Springer. https:\/\/doi.org\/10.1007\/978-3-319-10575-8.","DOI":"10.1007\/978-3-319-10575-8"},{"key":"9517_CR28","doi-asserted-by":"publisher","unstructured":"Cohen, S. (2006). Equivalence of queries combining set and bag-set semantics. In PODS, pp. 70\u201379. ACM. https:\/\/doi.org\/10.1145\/1142351.1142362.","DOI":"10.1145\/1142351.1142362"},{"issue":"3","key":"9517_CR29","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1007\/s00778-008-0122-1","volume":"18","author":"S Cohen","year":"2009","unstructured":"Cohen, S. (2009). Equivalence of queries that are sensitive to multiplicities. The VLDB Journal, 18(3), 765\u2013785. https:\/\/doi.org\/10.1007\/s00778-008-0122-1.","journal-title":"The VLDB Journal"},{"key":"9517_CR30","doi-asserted-by":"publisher","unstructured":"Cohen, S., Nutt, W., & Serebrenik, A. (1999). Rewriting aggregate queries using views. In PODS, pp. 155\u2013166. ACM. https:\/\/doi.org\/10.1145\/303976.303992.","DOI":"10.1145\/303976.303992"},{"key":"9517_CR31","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1109\/ASE.2009.63","volume":"2009","author":"L Cordeiro","year":"2009","unstructured":"Cordeiro, L., Fischer, B., & Marques-Silva, J. (2009). SMT-based bounded model checking for embedded ANSI-c software. ASE, 2009, 137\u2013148. https:\/\/doi.org\/10.1109\/ASE.2009.63.","journal-title":"ASE"},{"key":"9517_CR32","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Kroening, D., & Schrammel, P. Beyer, D., Huisman, M., Kordon, F., & Steffen, B. (Eds.). (2019). Jbmc: bounded model checking for java bytecode. Cham: Springer International Publishing.","DOI":"10.1007\/978-3-030-17502-3_17"},{"key":"9517_CR33","volume-title":"Database systems: design, implementation, and management","author":"C Coronel","year":"2009","unstructured":"Coronel, C., Morris, S., & Rob, P. (2009). Database systems: design, implementation, and management, 9th edn. Boston: Course Technology Press.","edition":"9th edn."},{"key":"9517_CR34","doi-asserted-by":"publisher","unstructured":"Cousot, P., & Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of Fixpoints. In POPL, pp. 238\u2013252. ACM Press. https:\/\/doi.org\/10.1145\/512950.512973.","DOI":"10.1145\/512950.512973"},{"key":"9517_CR35","unstructured":"Date, C. J. (2003). An introduction to database systems, 8th edn., Pearson, London."},{"key":"9517_CR36","doi-asserted-by":"publisher","unstructured":"De Moura, L., & Bjorner, N. (2008). Z3: an efficient SMT solver. In TACAS, pp. 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9517_CR37","doi-asserted-by":"publisher","unstructured":"Douglas, G., & Lawrence, R. (2016). Improving sql query performance on embedded devices using pre-compilation. In SAC, pp. 961\u2013964. ACM. https:\/\/doi.org\/10.1145\/2851613.2851657.","DOI":"10.1145\/2851613.2851657"},{"key":"9517_CR38","unstructured":"Ebel, N. (2020). Manually trigger a GitHub actions workflow. https:\/\/goobar.io\/2019\/12\/07\/manually-trigger-a-github-actions-workflow\/ retrieved March 10th."},{"key":"9517_CR39","doi-asserted-by":"publisher","unstructured":"Emmi, M., Majumdar, R., & Sen, K. (2007). Dynamic test input generation for database applications. In ISSTA, pp. 151\u2013162. ACM. https:\/\/doi.org\/10.1145\/1273463.1273484.","DOI":"10.1145\/1273463.1273484"},{"key":"9517_CR40","doi-asserted-by":"publisher","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., & Ulbrich, M. (2014). Automating regression verification. In ASE, pp. 349\u2013360. ACM. https:\/\/doi.org\/10.1145\/2642937.2642987.","DOI":"10.1145\/2642937.2642987"},{"key":"9517_CR41","unstructured":"Fisher, M., Ellis, J., & Bruce, J. C. (2003). JDBC API tutorial and reference, 3rd edn., Pearson Education, London."},{"issue":"5","key":"9517_CR42","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/543552.512558","volume":"37","author":"C Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., & Stata, R. (2002). Extended static checking for java. SIGPLAN Not., 37(5), 234\u2013245. https:\/\/doi.org\/10.1145\/543552.512558.","journal-title":"SIGPLAN Not."},{"key":"9517_CR43","unstructured":"Fowler, M. (2018). Refactoring: improving the design of existing code. Addison-Wesley Professional."},{"key":"9517_CR44","unstructured":"Garbus, J. (2015). SAP ASE 16\/Sybase ASE administration. Sap Press."},{"key":"9517_CR45","doi-asserted-by":"publisher","unstructured":"Ghafoor, M. A., Mahmood, M. S., & Siddiqui, J. H. (2019). Extending symbolic execution for automated testing of stored procedures. Software Quality Journal. https:\/\/doi.org\/10.1007\/s11219-019-09453-6.","DOI":"10.1007\/s11219-019-09453-6"},{"issue":"3","key":"9517_CR46","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1002\/stvr.1472","volume":"23","author":"B Godlin","year":"2013","unstructured":"Godlin, B., & Strichman, O. (2013). Regression verification: proving the equivalence of similar programs. Softw. Test., Verif. Reliab., 23(3), 241\u2013258. https:\/\/doi.org\/10.1002\/stvr.1472.","journal-title":"Softw. Test., Verif. Reliab."},{"key":"9517_CR47","doi-asserted-by":"crossref","unstructured":"G\u00f6rg, C., & Weiundefinedgerber, P. (2005). Error detection by refactoring reconstruction. In Proceedings of the 2005 International Workshop on Mining Software Repositories, MSR \u201905. (pp. 1\u20135). New York: Association for Computing Machinery.","DOI":"10.1145\/1083142.1083148"},{"key":"9517_CR48","doi-asserted-by":"publisher","unstructured":"Grossman, S., Cohen, S., Itzhaky, S., Rinetzky, N., & Sagiv, M. (2017). Verifying equivalence of spark programs. In CAV, LNCS, pp. 282\u2013300. Springer. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_15.","DOI":"10.1007\/978-3-319-63390-9_15"},{"issue":"1","key":"9517_CR49","doi-asserted-by":"publisher","first-page":"27","DOI":"10.14778\/3151113.3151116","volume":"11","author":"P Guagliardo","year":"2017","unstructured":"Guagliardo, P., & Libkin, L. (2017). A formal semantics of sql queries, its validation, and applications. Proc. VLDB Endow., 11(1), 27\u201339. https:\/\/doi.org\/10.14778\/3151113.3151116.","journal-title":"Proc. VLDB Endow."},{"issue":"10","key":"9517_CR50","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576\u2013580. https:\/\/doi.org\/10.1145\/363235.363259.","journal-title":"Communications of the ACM"},{"key":"9517_CR51","doi-asserted-by":"publisher","unstructured":"Huang, S., & Cheng, K. (1998). Formal equivalence checking and design debugging. Kluwer Academic Publishers. https:\/\/doi.org\/10.1007\/978-1-4615-5693-0.","DOI":"10.1007\/978-1-4615-5693-0"},{"key":"9517_CR52","unstructured":"IBM. (2012). Developing embedded SQL applications. ftp:\/\/ftp.software.ibm.com\/ps\/products\/db2\/info\/vr101\/pdf\/en_US\/DB2DevEmbeddedSQL-db2a1e1010.pdf, retrieved September 22nd, 2019."},{"issue":"3","key":"9517_CR53","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/211414.211419","volume":"20","author":"Y Ioannidis","year":"1995","unstructured":"Ioannidis, Y., & Ramakrishnan, R. (1995). Containment of conjunctive queries: beyond relations as sets. ACM Transaction Database System, 20(3), 288\u2013324. https:\/\/doi.org\/10.1145\/211414.211419.","journal-title":"ACM Transaction Database System"},{"key":"9517_CR54","unstructured":"ISO. (2016). Iso\/iec 9075-1:2016. Online at: https:\/\/www.iso.org\/obp\/ui\/#iso:std:iso-iec:9075:-1:ed-5:v1:en, retrieved September 22nd, 2019."},{"key":"9517_CR55","unstructured":"ITTIA. (2016). Benefits of database for embedded system and iot device manufacturers. On-line at: http:\/\/www.ittia.com\/files\/Benefits_of_Database_for_Embedded_System_and_IoT_Device_Manufacturers.pdf, retrieved September 22nd, 2019."},{"key":"9517_CR56","doi-asserted-by":"publisher","unstructured":"Jayram, T. S., Kolaitis, P. G., & Vee, E. (2006). The containment problem for real conjunctive queries with inequalities. In PODS, pp. 80\u201389. ACM. https:\/\/doi.org\/10.1145\/1142351.1142363.","DOI":"10.1145\/1142351.1142363"},{"issue":"7","key":"9517_CR57","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1109\/TSE.2014.2318734","volume":"40","author":"M Kim","year":"2014","unstructured":"Kim, M., Zimmermann, T., & Nagappan, N. (2014). An empirical study of refactoring challenges and benefits at Microsoft. IEEE Trans. Softw. Eng., 40(7), 633\u2013649. https:\/\/doi.org\/10.1109\/TSE.2014.2318734.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"7","key":"9517_CR58","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J. C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385\u2013394. https:\/\/doi.org\/10.1145\/360248.360252.","journal-title":"Communications of the ACM"},{"key":"9517_CR59","doi-asserted-by":"publisher","unstructured":"Lattner, C., & Adve, V. (2004). LLVM: A compilation framework for lifelong program analysis & transformation. In CGO, pp. 75\u201386. IEEE Computer Society. https:\/\/doi.org\/10.1109\/CGO.2004.1281665.","DOI":"10.1109\/CGO.2004.1281665"},{"key":"9517_CR60","doi-asserted-by":"publisher","unstructured":"Mahmood, M. S., Ghafoor, M., & Siddiqui, J. H. (2016). Symbolic execution of stored procedures in database management systems. In ASE, pp. 519\u2013530. ACM. https:\/\/doi.org\/10.1145\/2970276.2970318.","DOI":"10.1145\/2970276.2970318"},{"key":"9517_CR61","doi-asserted-by":"publisher","unstructured":"Malecha, G., Morrisett, G., Shinnar, A., & Wisnesky, R. (2010). Toward a verified relational DB management system. In POPL, pp. 237\u2013248. ACM. https:\/\/doi.org\/10.1145\/1706299.1706329.","DOI":"10.1145\/1706299.1706329"},{"issue":"2","key":"9517_CR62","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1109\/TSE.2004.1265817","volume":"30","author":"T Mens","year":"2004","unstructured":"Mens, T., & Tourw\u00e9, T. (2004). A survey of software refactoring. IEEE Transactions on Software Engineering, 30(2), 126\u2013139. https:\/\/doi.org\/10.1109\/TSE.2004.1265817.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9517_CR63","doi-asserted-by":"publisher","unstructured":"Merz, F., Falke, S., & Sinz, C. (2012). LLBMC: Bounded model checking of C and C++ programs using a compiler IR. In VSTTE, LNCS, pp. 146\u2013161. Springer. https:\/\/doi.org\/10.1007\/978-3-642-27705-4_12.","DOI":"10.1007\/978-3-642-27705-4_12"},{"key":"9517_CR64","unstructured":"Microsoft. (2020). Microsoft SQL server. https:\/\/www.microsoft.com\/en-us\/sql-server\/."},{"key":"9517_CR65","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1016\/j.scico.2015.03.005","volume":"105","author":"M Marcozzi","year":"2015","unstructured":"Marcozzi, M., Vanhoof, W., & Hainaut, J.I. (2015). Relational symbolic exec. of sql code for unit testing of database programs. Science of Comp. Program., 105, 44\u201372. https:\/\/doi.org\/10.1016\/j.scico.2015.03.005.","journal-title":"Science of Comp. Program."},{"issue":"1","key":"9517_CR66","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/TSE.2011.41","volume":"38","author":"E Murphy-Hill","year":"2012","unstructured":"Murphy-Hill, E., Parnin, C., & Black, A.P. (2012). How we refactor, and how we know it. IEEE Transactions on Software Engineering, 38(1), 5\u201318. https:\/\/doi.org\/10.1109\/TSE.2011.41.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"9517_CR67","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1145\/111197.111212","volume":"16","author":"M Negri","year":"1991","unstructured":"Negri, M., Pelagatti, G., & Sbattella, L. (1991). Formal semantics of sql queries. ACM Trans Database Syst., 16(3), 513\u2013534. https:\/\/doi.org\/10.1145\/111197.111212.","journal-title":"ACM Trans Database Syst."},{"key":"9517_CR68","unstructured":"Obe, R. O., & Hsu, L. S. (2017). PostgreSQL: Up and running: a practical guide to the advanced open source database. \u201cO\u2019Reilly Media Inc.\u201d."},{"key":"9517_CR69","unstructured":"Oracle. (2020). Oracle database. https:\/\/www.oracle.com\/database\/."},{"issue":"2","key":"9517_CR70","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/2491529","volume":"23","author":"K Pan","year":"2014","unstructured":"Pan, K., Wu, X., & Xie, T. (2014). Guided test generation for database applications via synthesized database interactions. ACM Trans. Softw. Eng. Methodol., 23(2), 12:1\u201312:s27. https:\/\/doi.org\/10.1145\/2491529.","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9517_CR71","doi-asserted-by":"publisher","unstructured":"Post, H., & Sinz, C. (2009). Proving functional equivalence of two AES implementations using bounded model checking. In ICST 2009, pp. 31\u201340. https:\/\/doi.org\/10.1109\/ICST.2009.39.","DOI":"10.1109\/ICST.2009.39"},{"key":"9517_CR72","unstructured":"PostgreSQL. (2020). PostgreSQL: The world\u2019s most advanced open source relational database. https:\/\/www.postgresql.org\/."},{"key":"9517_CR73","doi-asserted-by":"crossref","unstructured":"Ramos, D. A., & Engler, D. R. (2011). Practical, low-effort equivalence verification of real code. In CAV.","DOI":"10.1007\/978-3-642-22110-1_55"},{"issue":"2-3","key":"9517_CR74","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., & Voronkov, A. (2002). The design and implementation of VAMPIRE. AI Communications, 15(2-3), 91\u2013110.","journal-title":"AI Communications"},{"key":"9517_CR75","unstructured":"Rodchenko, N., Prokopov, A., & Gaviar, A. (2019). U\u2218OS blockchain framework. https:\/\/github.com\/UOSnetwork\/uos.docs\/blob\/master\/yellow_paper\/uos_yellow_paper.eng.pdf."},{"issue":"4","key":"9517_CR76","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322217.322221","volume":"27","author":"Y Sagiv","year":"1980","unstructured":"Sagiv, Y., & Yannakakis, M. (1980). Equivalences among relational exp. with union and difference operators. Journal of the ACM, 27 (4), 633\u2013655. https:\/\/doi.org\/10.1145\/322217.322221.","journal-title":"Journal of the ACM"},{"key":"9517_CR77","doi-asserted-by":"publisher","unstructured":"Scheben, C., & Schmitt, P. H. (2014). Efficient self-composition for weakest precondition calculi. In FM, LNCS, vol. 8442, pp. 579\u2013594. Springer. https:\/\/doi.org\/10.1007\/978-3-319-06410-9_39.","DOI":"10.1007\/978-3-319-06410-9_39"},{"key":"9517_CR78","doi-asserted-by":"publisher","unstructured":"Schlaipfer, M., Rajan, K., Lal, A., & Samak, M. (2017). Optimizing big-data queries using program synthesis. In SOSP, pp. 631\u2013646. ACM. https:\/\/doi.org\/10.1145\/3132747.3132773.","DOI":"10.1145\/3132747.3132773"},{"key":"9517_CR79","unstructured":"Schmitt, D. (2019). Bug #5673: Optimizer creates strange execution plan leading to wrong results. https:\/\/www.postgresql.org\/message-id\/201009231503.o8NF3blt059661@wwwmaster.postgresql.org retrieved September 22nd."},{"key":"9517_CR80","unstructured":"Spasi\u0107, M., & Vujo\u0161evi\u0107 Jani\u010di\u0107, M. (2018). First steps towards proving functional equivalence of embedded SQL. In TYPES, pp. 78\u201379. Univ. Minho."},{"key":"9517_CR81","unstructured":"Spasi\u0107, M., & Vujo\u0161evi\u0107 Jani\u010di\u0107, M. (2020). GitHub repository: SQLC (2020). https:\/\/github.com\/mirkospasic\/sqlc retrieved March 10th."},{"key":"9517_CR82","doi-asserted-by":"publisher","unstructured":"Strichman, O., & Godlin, B. (2005). Regression verification - a practical way to verify programs. In VSTTE, LNCS, vol. 4171, pp. 496\u2013501. Springer. https:\/\/doi.org\/10.1007\/978-3-540-69149-5_54.","DOI":"10.1007\/978-3-540-69149-5_54"},{"key":"9517_CR83","unstructured":"Sulik, M. (2019). Bug #70038: Wrong select count distinct with a field included in two-column unique key (2013). https:\/\/bugs.mysql.com\/bug.php?id=70038 retrieved September 22nd."},{"key":"9517_CR84","unstructured":"Sybase, S. (2020). Relational database server. https:\/\/www.sap.com\/products\/sybase-ase.html."},{"key":"9517_CR85","doi-asserted-by":"publisher","unstructured":"Tillmann, N., & Halleux, J. (2008). Pex \u2013 white box test generation for.NET. In TAP, LNCS, vol. 4966, pp. 134\u2013153. Springer. https:\/\/doi.org\/10.1007\/978-3-540-79124-9_10.","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"9517_CR86","first-page":"569","volume":"70","author":"BA Trakhtenbrot","year":"1950","unstructured":"Trakhtenbrot, B. A. (1950). Impossibility of an algorithm for the decision problem in finite classes. Doklady Akademii Nauk SSSR, 70, 569\u2013572.","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"9517_CR87","doi-asserted-by":"publisher","unstructured":"Veanes, M., Tillmann, N., & de Halleux, J. (2010). Qex: symbolic sql query explorer. In LPAR, pp. 425\u2013446. Springer. https:\/\/doi.org\/10.1007\/978-3-642-17511-4_24.","DOI":"10.1007\/978-3-642-17511-4_24"},{"issue":"2","key":"9517_CR88","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10836-009-5140-4","volume":"26","author":"S Verdoolaege","year":"2010","unstructured":"Verdoolaege, S., Palkovic, M., Bruynooghe, M., Janssens, G., & Catthoor, F. (2010). Experience with widening based equivalence checking in realistic multimedia systems. J. Electronic Testing, 26(2), 279\u2013292. https:\/\/doi.org\/10.1007\/s10836-009-5140-4.","journal-title":"J. Electronic Testing"},{"key":"9517_CR89","first-page":"14","volume":"49","author":"M Vujo\u0161evi\u0107 Jani\u010di\u0107","year":"2014","unstructured":"Vujo\u0161evi\u0107 Jani\u010di\u0107, M. (2014). Regression verification by system LAV. InfoM \u2014 Journal of Information Technology and Multimedia System, 49, 14\u201320.","journal-title":"InfoM \u2014 Journal of Information Technology and Multimedia System"},{"key":"9517_CR90","doi-asserted-by":"publisher","unstructured":"Vujo\u0161evi\u0107 Jani\u010di\u0107, M., & Kuncak, V. (2012). Development and evaluation of LAV: an SMT-based error finding platform. In VSTTE, LNCS, pp. 98\u2013113. Springer. https:\/\/doi.org\/10.1007\/978-3-642-27705-4_9.","DOI":"10.1007\/978-3-642-27705-4_9"},{"issue":"1","key":"9517_CR91","doi-asserted-by":"publisher","first-page":"205","DOI":"10.2298\/CSIS181220019V","volume":"17","author":"M Vujo\u0161evi\u0107 Jani\u010di\u0107","year":"2020","unstructured":"Vujo\u0161evi\u0107 Jani\u010di\u0107, M., & Mari\u0107, F. (2020). Regression verification for automated evaluation of students programs. Computer Science and Information Systems, 17(1), 205\u2013228. https:\/\/doi.org\/10.2298\/CSIS181220019V.","journal-title":"Computer Science and Information Systems"},{"key":"9517_CR92","doi-asserted-by":"publisher","unstructured":"Vujo\u0161evi\u0107 Jani\u010di\u0107, M., Nikoli\u0107, M., To\u0161i\u0107, D., & Kuncak, V. (2013). Software verification and graph similarity for automated evaluation of students\u2019 assignments. Information and Softw Technology 55(6). https:\/\/doi.org\/10.1016\/j.infsof.2012.12.005.","DOI":"10.1016\/j.infsof.2012.12.005"},{"key":"9517_CR93","unstructured":"Vujo\u0161evi\u0107 Jani\u010di\u0107, M., & Spasi\u0107, M. (2020). Tools LAV and SQLAV (2020). http:\/\/argo.matf.bg.ac.rs\/?content=lav retrieved March 10th."},{"key":"9517_CR94","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158144","volume":"29","author":"Y Wang","year":"2017","unstructured":"Wang, Y., Dillig, I., Lahiri, S., & Cook, W. (2017). Verifying equivalence of database-driven apps. Proc. ACM Program Lang., 29, 1\u201356. https:\/\/doi.org\/10.1145\/3158144.","journal-title":"Proc. ACM Program Lang."},{"key":"9517_CR95","unstructured":"Web, L. (2020). Ten ways databases run your life. https:\/\/www.liquidweb.com\/blog\/ten-ways-databases-run-your-life\/."},{"key":"9517_CR96","doi-asserted-by":"publisher","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., & Wischnewski, P. (2009). SPASS Version 3.5. In CADE, pp. 140\u2013145. https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10.","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"9517_CR97","doi-asserted-by":"publisher","unstructured":"Wei\u00dfgerber, P., & Diehl, S. (2006). Are refactorings less error-prone than other changes?. In Proceedings of the 2006 International Workshop on Mining Software Repositories, pp. 112\u2013118. https:\/\/doi.org\/10.1145\/1137983.1138011.","DOI":"10.1145\/1137983.1138011"},{"key":"9517_CR98","doi-asserted-by":"publisher","unstructured":"Wei\u00dfgerber, P., & Diehl, S. (2006). Identifying refactorings from source-code changes. In Proceedings of the 21st IEEE\/ACM International Conference on Automated Software Engineering, ASE \u201906. https:\/\/doi.org\/10.1109\/ASE.2006.41 (pp. 231\u2013240). USA: IEEE Computer Society.","DOI":"10.1109\/ASE.2006.41"},{"key":"9517_CR99","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.scico.2013.10.002","volume":"92","author":"Y Welsch","year":"2014","unstructured":"Welsch, Y., & Poetzsch-heffter, A. (2014). A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries. Sci. Comput. Program., 92, 129\u2013161. https:\/\/doi.org\/10.1016\/j.scico.2013.10.002.","journal-title":"Sci. Comput. Program."},{"issue":"10","key":"9517_CR100","first-page":"1488","volume":"20","author":"P Yang","year":"2014","unstructured":"Yang, P., Jin, P., & Yue, L. (2014). Exploiting the performance-energy tradeoffs for mobile database apps. Journal of Universal Comp. Science, 20(10), 1488\u20131498.","journal-title":"Journal of Universal Comp. Science"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-020-09517-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-020-09517-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-020-09517-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T10:19:28Z","timestamp":1630491568000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-020-09517-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,18]]},"references-count":100,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["9517"],"URL":"https:\/\/doi.org\/10.1007\/s11219-020-09517-y","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"value":"0963-9314","type":"print"},{"value":"1573-1367","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,18]]},"assertion":[{"value":"18 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}