{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:56:50Z","timestamp":1755838610282,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_15","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"282-300","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Verifying Equivalence of Spark Programs"],"prefix":"10.1007","author":[{"given":"Shelly","family":"Grossman","sequence":"first","affiliation":[]},{"given":"Sara","family":"Cohen","sequence":"additional","affiliation":[]},{"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala, SCALA 2013, pp. 1:1\u20131:10. ACM, New York (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Chandra, A.K., Merlin, P.M.: Optimal implementation of conjunctive queries in relational data bases. In: Proceedings of the Ninth Annual ACM Symposium on Theory of Computing, STOC 1977, pp. 77\u201390. ACM, New York (1977)","DOI":"10.1145\/800105.803397"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Vardi, M.Y.: Optimization of real conjunctive queries. In: Proceedings of the Twelfth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, PODS 1993, pp. 59\u201370. ACM, New York (1993)","DOI":"10.1145\/153850.153856"},{"issue":"2","key":"15_CR4","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(99)00220-0","volume":"239","author":"C Chekuri","year":"2000","unstructured":"Chekuri, C., Rajaraman, A.: Conjunctive query containment revisited. Theoret. Comput. Sci. 239(2), 211\u2013229 (2000)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR5","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). doi:10.1007\/978-3-662-46681-0_9"},{"key":"15_CR6","unstructured":"Chu, S., Wang, C., Weitz, K., Cheung, A.: Cosette: an automated prover for SQL. In: Online Proceedings of the 8th Biennial Conference on Innovative Data Systems Research, CIDR 2017, 8\u201311 January 2017, Chaminade, CA, USA (2017)"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1219092.1219093","volume":"54","author":"S Cohen","year":"2007","unstructured":"Cohen, S., Nutt, W., Sagiv, Y.: Deciding equivalences among conjunctive aggregate queries. J. ACM 54(2), 5 (2007)","journal-title":"J. ACM"},{"issue":"2","key":"15_CR8","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1145\/1055686.1055691","volume":"6","author":"S Cohen","year":"2005","unstructured":"Cohen, S., Sagiv, Y., Nutt, W.: Equivalences among aggregate queries with negation. ACM Trans. Comput. Logic 6(2), 328\u2013360 (2005)","journal-title":"ACM Trans. Comput. Logic"},{"key":"15_CR9","first-page":"300","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 300 (1972)","journal-title":"Mach. Intell."},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L De Moura","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-21437-0_12","volume-title":"FM 2011: Formal Methods","author":"AA El Ghazi","year":"2011","unstructured":"El Ghazi, A.A., Taghdiri, M.: Relational reasoning via SMT solving. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 133\u2013148. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-21437-0_12"},{"key":"15_CR12","unstructured":"Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. Technical report, Massachusetts Institue of Technology, Cambridge, MA, USA (1974)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Grossman, S., Cohen, S., Itzhaky, S., Rinetzky, N., Sagiv, M.: Verifying equivalence of spark programs. Technical report, Tel Aviv University, April 2017. http:\/\/www.cs.tau.ac.il\/%7Eshellygr\/pubs\/sparkeq-tr.pdf","DOI":"10.1007\/978-3-319-63390-9_15"},{"issue":"8","key":"15_CR14","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/s00236-004-0101-y","volume":"40","author":"S Grumbach","year":"2004","unstructured":"Grumbach, S., Rafanelli, M., Tininini, L.: On the equivalence and rewriting of aggregate queries. Acta Inf. 40(8), 529\u2013584 (2004)","journal-title":"Acta Inf."},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-60164-3_28","volume-title":"Category Theory and Computer Science","author":"M Hasegawa","year":"1995","unstructured":"Hasegawa, M.: Decomposing typed lambda calculus into a couple of categorical programming languages. In: Pitt, D., Rydeheard, D.E., Johnstone, P. (eds.) CTCS 1995. LNCS, vol. 953, pp. 200\u2013219. Springer, Heidelberg (1995). doi:10.1007\/3-540-60164-3_28"},{"key":"15_CR16","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":"15_CR17","volume-title":"Learning Spark: Lightning-Fast Big Data Analytics","author":"H Karau","year":"2015","unstructured":"Karau, H., Konwinski, A., Wendell, P., Zaharia, M.: Learning Spark: Lightning-Fast Big Data Analytics, 1st edn. O\u2019Reilly Media Inc., Sebastopol (2015)","edition":"1"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1145\/42267.42273","volume":"35","author":"A Klug","year":"1988","unstructured":"Klug, A.: On conjunctive queries containing inequalities. J. ACM 35(1), 146\u2013160 (1988)","journal-title":"J. ACM"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-17511-4_20"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Proceedings of the 2009 ACM Symposium on Applied Computing, SAC 2009, pp. 615\u2013622. ACM, New York (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Loncaric, C., Torlak, E., Ernst, M.D.: Fast synthesis of fast collections. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp. 355\u2013368. ACM, New York (2016)","DOI":"10.1145\/2908080.2908122"},{"key":"15_CR22","unstructured":"Presburger, M.: \u00dcber die vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervor. Comptes Rendus du I congr\u00e8s de Math\u00e9maticiens des Pays Slaves, pp. 92\u2013101 (1929)"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 159\u2013169. ACM, January 2008","DOI":"10.1145\/1379022.1375602"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 131\u2013144. ACM, January 2010","DOI":"10.1145\/1707801.1706316"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Smith, C., Albarghouthi, A.: Mapreduce program synthesis. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp. 326\u2013340. ACM, New York (2016)","DOI":"10.1145\/2908080.2908102"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 199\u2013210. ACM, New York (2010)","DOI":"10.1145\/1707801.1706325"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., Zinzindohoue, J.-K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F*. In: 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 256\u2013270. ACM, January 2016","DOI":"10.1145\/2837614.2837655"},{"key":"15_CR28","volume-title":"Advanced Analytics with Spark: Patterns for Learning from Data at Scale","author":"J Wills","year":"2015","unstructured":"Wills, J., Owen, S., Laserson, U., Ryza, S.: Advanced Analytics with Spark: Patterns for Learning from Data at Scale, 1st edn. O\u2019Reilly Media Inc., Sebastopol (2015)","edition":"1"},{"key":"15_CR29","unstructured":"Zaharia, M., Chowdhury, M., Das, T., Dave, A., Ma, J., McCauly, M., Franklin, M.J., Shenker, S., Stoica, I.: Resilient distributed datasets: a fault-tolerant abstraction for in-memory cluster computing. In: Presented as Part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pp. 15\u201328. USENIX, San Jose (2012)"},{"key":"15_CR30","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, HotCloud 2010, p. 10. USENIX Association, Berkeley (2010)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:09:59Z","timestamp":1626134999000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}