{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T14:49:20Z","timestamp":1773931760726,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,3,11]],"date-time":"2021-03-11T00:00:00Z","timestamp":1615420800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,3,11]],"date-time":"2021-03-11T00:00:00Z","timestamp":1615420800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Science and Engineering Research Board (SERB), Department of Science and Technology, Government of India","award":["IMP\/2018\/000523"],"award-info":[{"award-number":["IMP\/2018\/000523"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["SN COMPUT. SCI."],"published-print":{"date-parts":[[2021,5]]},"DOI":"10.1007\/s42979-020-00426-2","type":"journal-article","created":{"date-parts":[[2021,3,11]],"date-time":"2021-03-11T19:02:45Z","timestamp":1615489365000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification of Database Applications Using Predicate Abstraction"],"prefix":"10.1007","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2700-4127","authenticated-orcid":false,"given":"Md Imran","family":"Alam","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raju","family":"Halder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,11]]},"reference":[{"key":"426_CR1","volume-title":"Database systems","author":"R Elmasri","year":"2011","unstructured":"Elmasri R, Navathe SB. Database systems, vol. 9. Boston, MA: Pearson Education; 2011."},{"issue":"5","key":"426_CR2","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke EM, Grumberg O, Long DE. Model checking and abstraction. TOPLAS. 1994;16(5):1512\u201342. https:\/\/doi.org\/10.1145\/186025.186051.","journal-title":"TOPLAS"},{"issue":"4","key":"426_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala R, Majumdar R. Software model checking. ACM Comput Surv. 2009;41(4):1\u201354. https:\/\/doi.org\/10.1145\/1592434.1592438.","journal-title":"ACM Comput Surv"},{"issue":"7","key":"426_CR4","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball T, Levin V, Rajamani SK. A decade of software model checking with slam. Commun ACM. 2011;54(7):68\u201376. https:\/\/doi.org\/10.1145\/1965724.1965743.","journal-title":"Commun ACM"},{"issue":"5","key":"426_CR5","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"T Ball","year":"2001","unstructured":"Ball T, Majumdar R, Millstein T, Rajamani SK. Automatic predicate abstraction of c programs. ACM SIGPLAN Notices. 2001;36(5):203\u201313. https:\/\/doi.org\/10.1145\/381694.378846.","journal-title":"ACM SIGPLAN Notices"},{"key":"426_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_45","author":"E Clarke","year":"2000","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement. Conf CAV. 2000;. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_45.","journal-title":"Conf CAV"},{"issue":"5\u20136","key":"426_CR7","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker blast. STTT. 2007;9(5\u20136):505\u201325. https:\/\/doi.org\/10.1007\/s10009-007-0044-z.","journal-title":"STTT"},{"key":"426_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_40","author":"E Clarke","year":"2005","unstructured":"Clarke E, Kroening D, Sharygina N, Yorav K. Satabs: Sat-based predicate abstraction for ansi-c. TACAS. 2005;. https:\/\/doi.org\/10.1007\/978-3-540-31980-1_40.","journal-title":"TACAS."},{"key":"426_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_45","author":"D Kroening","year":"2011","unstructured":"Kroening D, Weissenbacher G. Interpolation-based software verification with wolverine. Conf CAV. 2011;. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_45.","journal-title":"Conf CAV"},{"key":"426_CR10","volume-title":"Systems and software verification: model-checking techniques and tools","author":"B B\u00e9rard","year":"2013","unstructured":"B\u00e9rard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P. Systems and software verification: model-checking techniques and tools. New York: Springer; 2013."},{"key":"426_CR11","doi-asserted-by":"crossref","unstructured":"Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B, Frama-c. in International Conference on Software Engineering and Formal Methods. Springer, 2012;233\u2013247.","DOI":"10.1007\/978-3-642-33826-7_16"},{"issue":"10","key":"426_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR. An axiomatic basis for computer programming. Commun ACM. 1969;12(10):576\u201380.","journal-title":"Commun ACM"},{"key":"426_CR13","unstructured":"Itzhaky S, Kotek T, Rinetzky N, Sagiv M, Tamir O, Veith H, Zuleger F. On the automated verification of web applications with embedded sql. In Proc. of ICDT, 2017."},{"key":"426_CR14","doi-asserted-by":"crossref","unstructured":"Benzaken V, Schaefer X. Static management of integrity in object-oriented databases: Design and implementation. In: International Conference on Extending Database Technology. Springer, 1998;309\u2013325.","DOI":"10.1007\/BFb0100993"},{"key":"426_CR15","doi-asserted-by":"crossref","unstructured":"Christiansen H, Martinenghi D. Simplification of database integrity constraints revisited: A transformational approach. In: Int. Symposium on Logic-Based Program Synthesis and Transformation. Springer, 2003;178\u2013197.","DOI":"10.1007\/978-3-540-25938-1_16"},{"issue":"1","key":"426_CR16","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/1707801.1706329","volume":"45","author":"G Malecha","year":"2010","unstructured":"Malecha G, Morrisett G, Shinnar A, Wisnesky R. Toward a verified relational database management system. ACM Sigplan Notices. 2010;45(1):237\u201348.","journal-title":"ACM Sigplan Notices"},{"key":"426_CR17","doi-asserted-by":"crossref","unstructured":"Baltopoulos IG, Borgstr\u00f6m J, Gordon AD. Maintaining database integrity with refinement types. In: European Conference on Object-Oriented Programming. Berlin, Heidelberg: Springer, 2011;484\u2013509.","DOI":"10.1007\/978-3-642-22655-7_23"},{"key":"426_CR18","doi-asserted-by":"publisher","unstructured":"Sharygina N, Kr\u00f6ning D. Model checking with abstraction for web services. In Test and Analysis of Web Services. Springer, 2007;121\u2013145. https:\/\/doi.org\/10.1007\/978-3-540-72912-9_5.","DOI":"10.1007\/978-3-540-72912-9_5"},{"issue":"3","key":"426_CR19","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/2694428.2694430","volume":"43","author":"A Deutsch","year":"2014","unstructured":"Deutsch A, Hull R, Vianu V. Automatic verification of database-centric systems. ACM SIGMOD Record. 2014;43(3):5\u201317. https:\/\/doi.org\/10.1145\/2694428.2694430.","journal-title":"ACM SIGMOD Record"},{"key":"426_CR20","doi-asserted-by":"publisher","unstructured":"Deutsch A, Marcus M, Sui L, Vianu V, Zhou D. A verifier for interactive, data-driven web applications. In: Proceedings of the 2005 ACM SIGMOD int. conf. on Management of data. 2005. https:\/\/doi.org\/10.1145\/1066157.1066219.","DOI":"10.1145\/1066157.1066219"},{"key":"426_CR21","doi-asserted-by":"publisher","unstructured":"Diana R, Marques-Neto H, Zarate L, Song M. A symbolic model checking approach to verifying transact-sql. In In. Conf. on SMC. IEEE, 2012;1735\u20131741. https:\/\/doi.org\/10.1109\/icsmc.2012.6377988.","DOI":"10.1109\/icsmc.2012.6377988"},{"key":"426_CR22","doi-asserted-by":"publisher","unstructured":"Gligoric M, Majumdar R. Model checking database applications. In: Proceedings of TACAS. Springer, 2013;549\u2013564. https:\/\/doi.org\/10.1007\/978-3-642-36742-7_40.","DOI":"10.1007\/978-3-642-36742-7_40"},{"key":"426_CR23","unstructured":"Ullman JD. Database constraints. http:\/\/infolab.stanford.edu\/~ullman\/fcdb\/jw-notes06\/constraints.html. Accessed 20 Aug 2020."},{"key":"426_CR24","unstructured":"Project P. Github pl\/sql project. https:\/\/github.com\/topics\/plsql. Accessed 29 July 2020."},{"key":"426_CR25","doi-asserted-by":"publisher","unstructured":"Jana A, Alam MI, Halder R, A symbolic model checker for database programs. In: ICSOFT, 2018;381\u2013388. https:\/\/doi.org\/10.5220\/0006913003810388.","DOI":"10.5220\/0006913003810388"},{"key":"426_CR26","unstructured":"Parr T, The definitive ANTLR 4 reference. Pragmatic Bookshelf, 2013."},{"key":"426_CR27","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N. \u201cZ3: An efficient smt solver,\u201d in Int. conf. on TACAS. Springer, 2008;337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"426_CR28","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/j.cl.2011.10.004","volume":"38","author":"R Halder","year":"2012","unstructured":"Halder R, Cortesi A. Abstract interpretation of database query languages. Comput Lang Syst Struct. 2012;38(2):123\u201357. https:\/\/doi.org\/10.1016\/j.cl.2011.10.004.","journal-title":"Comput Lang Syst Struct"},{"issue":"5","key":"426_CR29","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1109\/tse.2018.2861707","volume":"46","author":"A Jana","year":"2018","unstructured":"Jana A, Halder R, Kalahasti A, Ganni S, Cortesi A. Extending abstract interpretation to dependency analysis of database applications. TSE. 2018;46(5):463\u201394. https:\/\/doi.org\/10.1109\/tse.2018.2861707.","journal-title":"TSE"},{"key":"426_CR30","doi-asserted-by":"publisher","unstructured":"Ball T, Rajamani SK, Bebop: A symbolic model checker for boolean programs. In Int. SPIN Workshop on Model Checking of Software. Berlin, Heidelberg: Springer, 2000;113\u2013130. https:\/\/doi.org\/10.1007\/10722468_7.","DOI":"10.1007\/10722468_7"},{"key":"426_CR31","doi-asserted-by":"publisher","unstructured":"Aycock J, Horspool N, Simple generation of static single-assignment form. In Compiler Construction, D.\u00a0A. Watt, Ed. Berlin, Germany: Springer, Berlin Heidelberg, March 25\u2013April 2 2000;110\u2013125, https:\/\/doi.org\/10.1007\/3-540-46423-9_8.","DOI":"10.1007\/3-540-46423-9_8"},{"key":"426_CR32","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/tse.1984.5010248","volume":"4","author":"M Weiser","year":"1984","unstructured":"Weiser M. Program slicing. TSE. 1984;4:352\u20137. https:\/\/doi.org\/10.1109\/tse.1984.5010248.","journal-title":"TSE"},{"key":"426_CR33","unstructured":"Ball T, Rajamani SK. \u201cGenerating abstract explanations of spurious counterexamples in c programs,\u201d Technical Report MSR-TR-2002-09, Microsoft Research, Tech. Rep., (2002)."},{"key":"426_CR34","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The formal semantics of programming languages: an introduction","author":"G Winskel","year":"1993","unstructured":"Winskel G. The formal semantics of programming languages: an introduction. New York: MIT Press; 1993."},{"issue":"3","key":"426_CR35","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/2506375","volume":"46","author":"CA Furia","year":"2014","unstructured":"Furia CA, Meyer B, Velder S. Loop invariants: analysis, classification, and examples. ACM Comput Surv (CSUR). 2014;46(3):34.","journal-title":"ACM Comput Surv (CSUR)"},{"issue":"2","key":"426_CR36","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s00165-009-0110-2","volume":"22","author":"D Kroening","year":"2010","unstructured":"Kroening D, Weissenbacher G. Verification and falsification of programs with loops using predicate abstraction. Formal Aspects Comput. 2010;22(2):105\u2013128.","journal-title":"Formal Aspects Comput"},{"key":"426_CR37","doi-asserted-by":"crossref","unstructured":"Cortesi A, Halder R. Abstract interpretation of recursive queries. In International Conference on Distributed Computing and Internet Technology. Springer, 2013;157\u2013170.","DOI":"10.1007\/978-3-642-36071-8_12"},{"issue":"8","key":"426_CR38","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1002\/(sici)1097-024x(19980710)28:8<859::aid-spe188>3.0.co;2-8","volume":"28","author":"P Briggs","year":"1998","unstructured":"Briggs P, Cooper KD, Harvey TJ, Simpson LT. Practical improvements to the construction and destruction of static single assignment form. SP&E. 1998;28(8):859\u201381. https:\/\/doi.org\/10.1002\/(sici)1097-024x(19980710)28:8<859::aid-spe188>3.0.co;2-8.","journal-title":"SP&E"},{"key":"426_CR39","doi-asserted-by":"crossref","unstructured":"Beyer D. Software verification with validation of results. In TACAS. Springer, 2017;331\u2013349.","DOI":"10.1007\/978-3-662-54580-5_20"}],"container-title":["SN Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-020-00426-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42979-020-00426-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-020-00426-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,13]],"date-time":"2021-05-13T17:17:33Z","timestamp":1620926253000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42979-020-00426-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,11]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,5]]}},"alternative-id":["426"],"URL":"https:\/\/doi.org\/10.1007\/s42979-020-00426-2","relation":{},"ISSN":["2662-995X","2661-8907"],"issn-type":[{"value":"2662-995X","type":"print"},{"value":"2661-8907","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,3,11]]},"assertion":[{"value":"29 October 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 December 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 March 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with Ethical Standards"}},{"value":"On behalf of all authors, the corresponding author states that there is no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"135"}}