{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:20:41Z","timestamp":1740122441393,"version":"3.37.3"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,12,12]],"date-time":"2018-12-12T00:00:00Z","timestamp":1544572800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,12,12]],"date-time":"2018-12-12T00:00:00Z","timestamp":1544572800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1423623"],"award-info":[{"award-number":["CCF-1423623"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s10515-018-0249-2","type":"journal-article","created":{"date-parts":[[2018,12,12]],"date-time":"2018-12-12T06:42:40Z","timestamp":1544596960000},"page":"379-416","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Inductive verification of data model invariants in web applications using first-order logic"],"prefix":"10.1007","volume":"26","author":[{"given":"Ivan","family":"Boci\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0742-8101","authenticated-orcid":false,"given":"Nicol\u00e1s","family":"Rosner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,12,12]]},"reference":[{"issue":"1","key":"249_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hahnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Softw. Syst. Model. 4(1), 32\u201354 (2005)","journal-title":"Softw. Syst. Model."},{"key":"249_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201914), pp. 282\u2013293. ACM, New York (2014)","DOI":"10.1145\/2594291.2594317"},{"key":"249_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Proceedings of the 4th International Symposium on Formal Methods for Components and Objects (FMCO 2005), pp. 364\u2013387 (2005)","DOI":"10.1007\/11804192_17"},{"key":"249_CR4","unstructured":"Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with isabelle\u2014superposition with hard sorts and configurable simplification. In: Interactive Theorem Proving\u2014Third International Conference (ITP 2012), Princeton, NJ, USA, August 13\u201315, 2012. Proceedings, pp. 345\u2013360 (2012)"},{"key":"249_CR5","unstructured":"Bocic, I.: Data model verification via theorem proving. PhD thesis, University of California, Santa Barbara, Sept. 2016"},{"key":"249_CR6","unstructured":"Bocic, I., Bultan, T.: Inductive verification of data model invariants for web applications. In: 36th International Conference on Software Engineering (ICSE 2014), Hyderabad, India\u2014May 31\u2013June 07, 2014, pp. 620\u2013631 (2014)"},{"key":"249_CR7","doi-asserted-by":"crossref","unstructured":"Bocic, I., Bultan, T.: Coexecutability for efficient verification of data model updates. In: 37th International Conference on Software Engineering (ICSE 2015) (2015a)","DOI":"10.1109\/ICSE.2015.87"},{"key":"249_CR8","unstructured":"Bocic, I., Bultan, T.: Data model bugs. In: NASA Formal Methods\u20147th International Symposium, NFM 2015, Pasadena, CA, USA, April 27\u201329, 2015, Proceedings, pp. 393\u2013399 (2015b)"},{"key":"249_CR9","doi-asserted-by":"crossref","unstructured":"Bocic, I., Bultan, T.: Efficient data model verification with many-sorted logic. In: 30th IEEE\/ACM International Conference on Automated Software Engineering ASE 2015, Lincoln, Nebraska, USA, 9\u201313 Nov. (2015c)","DOI":"10.1109\/ASE.2015.48"},{"key":"249_CR10","unstructured":"Bocic, I., Bultan, T.: Symbolic model extraction for web application verification. In: Proceedings of the 39th International Conference on Software Engineering, ICSE 2017, Buenos Aires, Argentina, May 20\u201328, 2017, pp. 724\u2013734 (2017)"},{"key":"249_CR11","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity\u2014translating between many-sorted and unsorted first-order logic. In: Automated Deduction\u2014CADE-23\u201323rd International Conference on Automated Deduction, Wroclaw, Poland, July 31\u2013August 5, 2011. Proceedings, pp. 207\u2013221 (2011)"},{"key":"249_CR12","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bjrner, N.: Efficient e-matching for SMT solvers. In: Automated Deduction\u2014CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17\u201320, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pp. 183\u2013198. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"249_CR13","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings, pp. 337\u2013340 (2008)"},{"issue":"3","key":"249_CR14","first-page":"35","volume":"31","author":"A Deutsch","year":"2008","unstructured":"Deutsch, A., Vianu, V.: WAVE: automatic verification of data-driven web services. IEEE Data Eng. Bull. 31(3), 35\u201339 (2008)","journal-title":"IEEE Data Eng. Bull."},{"key":"249_CR15","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Sui, L., Vianu, V., Zhou, D.: A system for specification and verification of interactive, data-driven web applications. In: SIGMOD Conference, pp. 772\u2013774 (2006)","DOI":"10.1145\/1142473.1142584"},{"issue":"3","key":"249_CR16","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1016\/j.jcss.2006.10.006","volume":"73","author":"A Deutsch","year":"2007","unstructured":"Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. J. Comput. Syst. Sci. 73(3), 442\u2013474 (2007)","journal-title":"J. Comput. Syst. Sci."},{"key":"249_CR17","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17\u201320, 2006, Proceedings, pp. 81\u201394 (2006)"},{"key":"249_CR18","unstructured":"Karaca, E.: A collection\/list of awesome projects, sites made with Rails, Jan. 2016. \n                    https:\/\/github.com\/ekremkaraca\/awesome-rails"},{"key":"249_CR19","unstructured":"Fat Free CRM - Ruby on Rails-based open source CRM platform, Sept. 2013. \n                    http:\/\/www.fatfreecrm.com"},{"key":"249_CR20","unstructured":"Fielding, R.T.: Architectural styles and the design of network-based software architectures. PhD thesis, University of California, Irvine (2000)"},{"key":"249_CR21","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"249_CR22","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: Dynalloy: upgrading alloy with actions. In: 27th International Conference on Software Engineering (ICSE 2005), 15\u201321 May 2005, St. Louis, Missouri, USA, pp. 442\u2013451 (2005)","DOI":"10.1145\/1062455.1062535"},{"issue":"1","key":"249_CR23","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/1314493.1314497","volume":"17","author":"MF Frias","year":"2007","unstructured":"Frias, M.F., Pombo, C.L., Galeotti, J.P., Aguirre, N.: Efficient analysis of DynAlloy specifications. ACM Trans. Softw. Eng. Methodol. 17(1), 4:1\u20134:34 (2007)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"249_CR24","unstructured":"Galeotti, J.P., Frias, M.F.: Dynalloy as a formal method for the analysis of java programs. In: Software Engineering Techniques: Design for Quality, SET 2006, October 17\u201320, 2006, Warsaw, Poland, pp. 249\u2013260 (2006)"},{"issue":"2","key":"249_CR25","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"249_CR26","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. (TOSEM 2002) 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM 2002)"},{"key":"249_CR27","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)"},{"key":"249_CR28","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: Jayhorn: a framework for verifying java programs. In: Computer Aided Verification\u201428th International Conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Proceedings, Part I, pp. 352\u2013358 (2016)"},{"key":"249_CR29","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013), Saint Petersburg, Russia, July 13\u201319, 2013, pp. 1\u201335 (2013)"},{"issue":"3","key":"249_CR30","first-page":"26","volume":"1","author":"GE Krasner","year":"1988","unstructured":"Krasner, G.E., Pope, S.T.: A cookbook for using the model-view controller user interface paradigm in Smalltalk-80. J. Object Oriented Program. 1(3), 26\u201349 (1988)","journal-title":"J. Object Oriented Program."},{"issue":"12","key":"249_CR31","doi-asserted-by":"publisher","first-page":"988","DOI":"10.1109\/TSE.2006.125","volume":"32","author":"V Kuncak","year":"2006","unstructured":"Kuncak, V., Lam, P., Zee, K., Rinard, M.C.: Modular pluggable analyses for data structure consistency. IEEE Trans. Softw. Eng. 32(12), 988\u20131005 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"249_CR32","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Proceedings of the 16th International Conference on Logic Programming, Artificial Intelligence, and Reasoning (LPAR), pp. 348\u2013370 (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"249_CR33","unstructured":"Lesani, M., Millstein, T.D., Palsberg, J.: Automatic atomicity verification for clients of concurrent data structures. In: Computer Aided Verification\u201426th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. Proceedings, pp. 550\u2013567 (2014)"},{"key":"249_CR34","doi-asserted-by":"crossref","unstructured":"Near, J.P., Jackson, D.: Rubicon: bounded verification of web applications. In: Proceedings of the ACM SIGSOFT 20th International Symposium on Foundations of Software Engineering (FSE 2012), pp. 60:1\u201360:11 (2012)","DOI":"10.1145\/2393596.2393667"},{"key":"249_CR35","doi-asserted-by":"crossref","unstructured":"Nijjar, J., Bultan, T.: Bounded verification of Ruby on Rails data models. In: Proceedings of the 20th International Symposium on Software Testing and Analysis (ISSTA 2011), pp. 67\u201377 (2011)","DOI":"10.1145\/2001420.2001429"},{"key":"249_CR36","doi-asserted-by":"crossref","unstructured":"Nijjar, J., Bultan, T.: Unbounded data model verification using SMT solvers. In: Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2012), pp. 210\u2013219 (2012)","DOI":"10.1145\/2351676.2351706"},{"key":"249_CR37","doi-asserted-by":"crossref","unstructured":"Nijjar, J., Boci\u0107, I., Bultan, T.: An integrated data model verifier with property templates. In: Proceedings of the ICSE Workshop on Formal Methods in Software Engineering (FormaliSE 2013), pp. 23\u201335. IEEE (2013)","DOI":"10.1109\/FormaliSE.2013.6612274"},{"key":"249_CR38","unstructured":"Object Management Group: UML Specification. \n                    http:\/\/www.omg.org"},{"key":"249_CR39","unstructured":"Open Source Rails, Jan. 2016. \n                    http:\/\/www.opensourcerails.com"},{"issue":"2\u20133","key":"249_CR40","first-page":"79","volume":"15","author":"F Pelletier","year":"2002","unstructured":"Pelletier, F., Sutcliffe, G., Suttner, C.: The development of CASC. AI Commun. 15(2\u20133), 79\u201390 (2002)","journal-title":"AI Commun."},{"issue":"3","key":"249_CR41","doi-asserted-by":"publisher","first-page":"177","DOI":"10.2307\/2268615","volume":"19","author":"WV Quine","year":"1954","unstructured":"Quine, W.V.: Quantification and the empty domain. J. Symb. Log. 19(3), 177\u2013179 (1954)","journal-title":"J. Symb. Log."},{"key":"249_CR42","doi-asserted-by":"crossref","unstructured":"Richters, M., Gogolla, M.: Validating UML models and OCL constraints. In: Proceedings of the 3rd International Conference on Unified Modeling Language (UML 2000), LNCS 1939 (2000)","DOI":"10.1007\/3-540-40011-7_19"},{"key":"249_CR43","unstructured":"Ruby on Rails, Feb. 2013. \n                    http:\/\/rubyonrails.org"},{"key":"249_CR44","unstructured":"SimilarTech: Website technology detection and tracking, Oct. 2018. \n                    https:\/\/similartech.com\/"},{"key":"249_CR45","unstructured":"SMT-LIB, 2016. \n                    http:\/\/www.smtlib.org\/"},{"key":"249_CR46","unstructured":"Spring Framework | SpringSource.org, Feb. 2013. \n                    http:\/\/www.springsource.org"},{"key":"249_CR47","unstructured":"Stickel, M.E., Waldinger, R.J., Lowry, M.R., Pressburger, T., Underwood, I.: Deductive composition of astronomical software from subroutine libraries. In: Automated Deduction\u2014CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26\u2013July 1, 1994, Proceedings, pp. 341\u2013355 (1994)"},{"issue":"1","key":"249_CR48","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"key":"249_CR49","unstructured":"Sutcliffe, G., Suttner, C.B., Yemenis, T.: The TPTP problem library. In: Automated Deduction\u2014CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26\u2013July 1, 1994, Proceedings, pp. 252\u2013266 (1994)"},{"key":"249_CR50","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, M\u00e9rida, Venezuela, March 11\u201315, 2012. Proceedings, pp. 406\u2013419 (2012)"},{"key":"249_CR51","unstructured":"The Web framework for perfectionists with deadlines | Django, Feb. 2013. \n                    http:\/\/www.djangoproject.com"},{"key":"249_CR52","unstructured":"TPTP Syntax, Jan. 2015. \n                    http:\/\/www.cs.miami.edu\/~tptp\/TPTP\/SyntaxBNF.html"},{"key":"249_CR53","unstructured":"Tracks, Sept. 2013. \n                    http:\/\/getontracks.org"},{"key":"249_CR54","volume-title":"The Object Constraint Language: Precise Modeling with UML","author":"J Warmer","year":"1998","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Boston (1998)"},{"key":"249_CR55","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Proceedings of the 22nd International Conference on Automated Deduction (CADE 2009), LNCS 5663, pp. 140\u2013145 (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"249_CR56","unstructured":"Weidenbach, C.: SPASS input syntax version 1.5, 2016. \n                    http:\/\/www.spass-prover.org\/download\/binaries\/spass-input-syntax15.pdf"},{"key":"249_CR57","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201908), pp. 349\u2013361. ACM, New York, NY (2008)","DOI":"10.1145\/1379022.1375624"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-018-0249-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-018-0249-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-018-0249-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T08:39:14Z","timestamp":1589704754000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-018-0249-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,12]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["249"],"URL":"https:\/\/doi.org\/10.1007\/s10515-018-0249-2","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2018,12,12]]},"assertion":[{"value":"22 December 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 December 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}