{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T09:03:58Z","timestamp":1774602238786,"version":"3.50.1"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["#1712060 and #1453386"],"award-info":[{"award-number":["#1712060 and #1453386"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>This paper addresses the problem of verifying equivalence between a pair of programs that operate over databases with different schemas. This problem is particularly important in the context of web applications, which typically undergo database refactoring either for performance or maintainability reasons. While web applications should have the same externally observable behavior before and after schema migration, there are no existing tools for proving equivalence of such programs. This paper takes a first step towards solving this problem by formalizing the equivalence and refinement checking problems for database-driven applications. We also propose a proof methodology based on the notion of bisimulation invariants over relational algebra with updates and describe a technique for synthesizing such bisimulation invariants. We have implemented the proposed technique in a tool called Mediator for verifying equivalence between database-driven applications written in our intermediate language and evaluate our tool on 21 benchmarks extracted from textbooks and real-world web applications. Our results show that the proposed methodology can successfully verify 20 of these benchmarks.<\/jats:p>","DOI":"10.1145\/3158144","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Verifying equivalence of database-driven applications"],"prefix":"10.1145","volume":"2","author":[{"given":"Yuepeng","family":"Wang","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"William R.","family":"Cook","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/0208017"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1628"},{"key":"e_1_2_2_3_1","volume-title":"Test-driven development of relational databases. Ieee Software 24, 3","author":"Ambler Scott W","year":"2007"},{"key":"e_1_2_2_4_1","unstructured":"Scott W Ambler and Pramod J Sadalage. 2006. Refactoring databases: Evolutionary database design. Pearson Education.  Scott W Ambler and Pramod J Sadalage. 2006. Refactoring databases: Evolutionary database design. Pearson Education."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390662"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90038-X"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057391"},{"key":"e_1_2_2_8_1","volume-title":"The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org 15","author":"Barrett Clark","year":"2010"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_3"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/800135.804424"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2731"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2903726"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803397"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348954"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_2_2_18_1","volume-title":"Proc. of CIDR.","author":"Chu Shumo","year":"2017"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211314"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/303976.303992"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-012-0302-x"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_16"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062486"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066157.1066219"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2006.10.006"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273463.1273484"},{"key":"e_1_2_2_30_1","volume-title":"Schema matching and mapping","author":"Fagin Ronald"},{"key":"e_1_2_2_31_1","unstructured":"St\u00e9phane Faroult and Pascal L\u2019Hermite. 2008. Refactoring SQL applications. O\u2019Reilly Media.  St\u00e9phane Faroult and Pascal L\u2019Hermite. 2008. Refactoring SQL applications. O\u2019Reilly Media."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_40"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630034"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1472"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514930"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_20"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1137\/0215061"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_11"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_18"},{"key":"e_1_2_2_45_1","volume-title":"Proc. of VLDB. 120\u2013133","author":"Miller Ren\u00e9e J.","year":"1993"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393667"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_2_2_48_1","unstructured":"Oracle. 2005. Oracle Schema Optimization Guide. https:\/\/docs.oracle.com\/cd\/B14099_19\/web.1012\/b15901\/tuning007.htm . (2005).  Oracle. 2005. Oracle Schema Optimization Guide. https:\/\/docs.oracle.com\/cd\/B14099_19\/web.1012\/b15901\/tuning007.htm . (2005)."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1228268.1228273"},{"key":"e_1_2_2_52_1","unstructured":"Martin Rinard. 1999. Credible Compilation. In MIT TechReport. MIT\u2013LCS\u2013TR\u2013776.  Martin Rinard. 1999. Credible Compilation. In MIT TechReport. MIT\u2013LCS\u2013TR\u2013776."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/176567.176568"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322221"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.17"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890002"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040311"},{"key":"e_1_2_2_61_1","first-page":"569","article-title":"Impossibility of an algorithm for the decision problem in finite classes","volume":"70","author":"Trakhtenbrot Boris A","year":"1950","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514896"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.090"},{"key":"e_1_2_2_64_1","volume-title":"Cook","author":"Wang Yuepeng","year":"2017"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390661"},{"key":"e_1_2_2_66_1","unstructured":"Wikimedia. 2017. Schema changes. https:\/\/wikitech.wikimedia.org\/wiki\/Schema_changes . (2017).  Wikimedia. 2017. Schema changes. https:\/\/wikitech.wikimedia.org\/wiki\/Schema_changes . (2017)."},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_35"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_2_2_70_1","first-page":"223","article-title":"VOC: A Methodology for the Translation Validation of Optimizing Compilers","volume":"9","author":"Zuck Lenore D.","year":"2003","journal-title":"J. UCS"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158144","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158144","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158144","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158144"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":70,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158144"],"URL":"https:\/\/doi.org\/10.1145\/3158144","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}