{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:06:40Z","timestamp":1773655600564,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030035914","type":"print"},{"value":"9783030035921","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-03592-1_14","type":"book-chapter","created":{"date-parts":[[2018,11,23]],"date-time":"2018-11-23T04:45:32Z","timestamp":1542948332000},"page":"248-266","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Relational Equivalence Proofs Between Imperative and MapReduce Algorithms"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[]},{"given":"Timo","family":"Bingmann","sequence":"additional","affiliation":[]},{"given":"Moritz","family":"Kiefer","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sanders","sequence":"additional","affiliation":[]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Weigl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,11,24]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Beckert, B., Bingmann, T., Kiefer, M., Sanders, P., Ulbrich, M., Weigl, A.: Relational Equivalence Proofs Between Imperative and MapReduce Algorithms. ArXiv e-prints, January 2018. arXiv:1801.08766","DOI":"10.1007\/978-3-030-03592-1_14"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Beckert, B., Bingmann, T., Kiefer, M., Sanders, P., Ulbrich, M., Weigl, A.: Proving equivalence between imperative and mapreduce implementations using program transformations. In: Third Workshop Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Electronic Proceedings in Theoretical Computer Science, vol. 268, pp. 185\u2013199. Open Publishing Association (2018)","DOI":"10.4204\/EPTCS.268.7"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bingmann, T., et al.: Thrill: high-performance algorithmic distributed batch data processing with C++. In: IEEE International Conference on Big Data, pp. 172\u2013183. IEEE, December 2016. preprint arXiv:1608.05634","DOI":"10.1109\/BigData.2016.7840603"},{"issue":"1\u20137","key":"14_CR5","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0169-7552(98)00110-X","volume":"30","author":"S Brin","year":"1998","unstructured":"Brin, S., Page, L.: The anatomy of a large-scale hypertextual web search engine. Comput. Netw. ISDN Syst. 30(1\u20137), 107\u2013117 (1998). https:\/\/doi.org\/10.1016\/S0169-7552(98)00110-X","journal-title":"Comput. Netw. ISDN Syst."},{"issue":"6","key":"14_CR6","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1145\/1809028.1806638","volume":"45","author":"C Chambers","year":"2010","unstructured":"Chambers, C., et al.: FlumeJava: easy, efficient data-parallel pipelines. ACM SIGPLAN Notices 45(6), 363\u2013375 (2010)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., Hong, C.D., Leng\u00e1l, O., Mu, S.C., Sinha, N., Wang, B.Y.: An Executable Sequential Specification for Spark Aggregation (2017). arXiv:1702.02439","DOI":"10.1007\/978-3-319-59647-1_31"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-662-46681-0_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-F Chen","year":"2015","unstructured":"Chen, Y.-F., Hong, C.-D., Sinha, N., Wang, B.-Y.: Commutativity of reducers. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 131\u2013146. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_9"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Y., Song, L., Wu, Z.: The Commutativity Problem of the MapReduce Framework: A Transducer-based Approach. CoRR abs\/1605.01497 (2016). arXiv:1605.01497","DOI":"10.1007\/978-3-319-41540-6_6"},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1327452.1327492","volume":"51","author":"J Dean","year":"2008","unstructured":"Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. Commun. ACM 51(1), 107\u2013113 (2008)","journal-title":"Commun. ACM"},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10703-015-0234-3","volume":"47","author":"D Elenbogen","year":"2015","unstructured":"Elenbogen, D., Katz, S., Strichman, O.: Proving mutual termination. Form. Methods Syst. Des. 47(2), 204\u2013229 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0234-3","journal-title":"Form. Methods Syst. Des."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering, pp. 349\u2013360. ASE 2014. ACM, New York, NY, USA (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: Proceedings of the 46th Annual Design Automation Conference, pp. 466\u2013471. DAC 2009. ACM, New York, NY, USA (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-319-63390-9_15","volume-title":"Computer Aided Verification","author":"S Grossman","year":"2017","unstructured":"Grossman, S., Cohen, S., Itzhaky, S., Rinetzky, N., Sagiv, M.: Verifying equivalence of spark programs. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 282\u2013300. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_15"},{"key":"14_CR15","unstructured":"Hawblitzel, C., Kawaguchi, M., Lahiri, S., Reb\u00ealo, H.: Mutual summaries: unifying program comparison techniques. In: Informal proceedings of BOOGIE 2011 workshop (2011). https:\/\/www.microsoft.com\/en-us\/research\/publication\/mutual-summaries-unifying-program-comparison-techniques\/"},{"key":"14_CR16","first-page":"22","volume":"87","author":"G Kahn","year":"1987","unstructured":"Kahn, G.: Natural semantics. STACS 87, 22\u201339 (1987)","journal-title":"STACS"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Kiefer, M., Klebanov, V., Ulbrich, M.: Relational program reasoning using compiler IR - combining static verification and dynamic analysis. J. Autom. Reason. (2017)","DOI":"10.1007\/s10817-017-9433-5"},{"key":"14_CR18","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10703-017-0293-8","volume":"52","author":"V Klebanov","year":"2017","unstructured":"Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification of pointer programs by predicate abstraction. J. Formal Methods Syst. Des. 52, 229\u2013259 (2017)","journal-title":"J. Formal Methods Syst. Des."},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2012","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712\u2013717. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_54"},{"issue":"2","key":"14_CR20","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1109\/TIT.1982.1056489","volume":"28","author":"S Lloyd","year":"1982","unstructured":"Lloyd, S.: Least squares quantization in PCM. IEEE Trans. Inf. Theor. 28(2), 129\u2013137 (1982). https:\/\/doi.org\/10.1109\/TIT.1982.1056489","journal-title":"IEEE Trans. Inf. Theor."},{"issue":"10","key":"14_CR21","doi-asserted-by":"publisher","first-page":"909","DOI":"10.1145\/2714064.2660228","volume":"49","author":"C Radoi","year":"2014","unstructured":"Radoi, C., Fink, S.J., Rabbah, R., Sridharan, M.: Translating Imperative Code to MapReduce. SIGPLAN Not. 49(10), 909\u2013927 (2014)","journal-title":"SIGPLAN Not."},{"key":"14_CR22","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project, version 8.6 (2004). http:\/\/coq.inria.fr"},{"issue":"3","key":"14_CR23","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/2362389.2362390","volume":"34","author":"S Verdoolaege","year":"2012","unstructured":"Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34(3), 11:1\u201311:35 (2012). https:\/\/doi.org\/10.1145\/2362389.2362390","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR24","volume-title":"Hadoop: The Definitive Guide","author":"T White","year":"2012","unstructured":"White, T.: Hadoop: The Definitive Guide. O\u2019Reilly Media Inc., Sebastopol (2012)"},{"key":"14_CR25","unstructured":"Zaharia, M., Chowdhury, M., Franklin, M.J., Shenker, S., Stoica, I.: Spark: cluster computing with working sets. In: Proceedings of the 2nd USENIX Conference on Hot Topics in Cloud Computing, pp. 10\u201310. HotCloud 2010, USENIX Association, Berkeley, CA, USA (2010). http:\/\/dl.acm.org\/citation.cfm?id=1863103.1863113"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-03592-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,7]],"date-time":"2022-07-07T15:05:57Z","timestamp":1657206357000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-03592-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030035914","9783030035921"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-03592-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"24 November 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/vstte18.it.uu.se\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}