{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:12:50Z","timestamp":1755997970651},"publisher-location":"Cham","reference-count":58,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319912707"},{"type":"electronic","value":"9783319912714"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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-319-91271-4_8","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T10:32:55Z","timestamp":1525689175000},"page":"105-120","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Systematic Generation of Non-equivalent Expressions for Relational Algebra"],"prefix":"10.1007","author":[{"given":"Kaiyuan","family":"Wang","sequence":"first","affiliation":[]},{"given":"Allison","family":"Sullivan","sequence":"additional","affiliation":[]},{"given":"Manos","family":"Koukoutos","sequence":"additional","affiliation":[]},{"given":"Darko","family":"Marinov","sequence":"additional","affiliation":[]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,8]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"934","DOI":"10.1007\/978-3-642-39799-8_67","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 934\u2013950. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_67"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-662-54577-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2017","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 319\u2013336. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F.S., Jackson, D.: Modular verification of code with SAT. In: ISSTA (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: POPL (2017)","DOI":"10.1145\/3009837.3009851"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: PLDI (2015)","DOI":"10.1145\/2737924.2737977"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.G.L., Aguirre, N.M.: DynAlloy: upgrading Alloy with actions. In: ICSE (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Galenson, J., Reames, P., Bodik, R., Hartmann, B., Sen, K.: CodeHint: dynamic and interactive synthesis of code snippets. In: ICSE (2014)","DOI":"10.1145\/2568225.2568250"},{"key":"8_CR9","first-page":"1283","volume":"39","author":"JP Galeotti","year":"2013","unstructured":"Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. TSE 39, 1283\u20131307 (2013)","journal-title":"TSE"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-19835-9_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Divya Gopinath","year":"2011","unstructured":"Gopinath, D., Malik, M.Z., Khurshid, S.: Specification-based program repair using SAT. In: TACAS (2011)"},{"issue":"11","key":"8_CR11","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/2736282","volume":"58","author":"S Gulwani","year":"2015","unstructured":"Gulwani, S., Hern\u00e1ndez-Orallo, J., Kitzelmann, E., Muggleton, S.H., Schmid, U., Zorn, B.: Inductive programming meets the real world. CACM 58(11), 90\u201399 (2015)","journal-title":"CACM"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-22110-1_33","volume-title":"Computer Aided Verification","author":"T Gvero","year":"2011","unstructured":"Gvero, T., Kuncak, V., Piskac, R.: Interactive synthesis of code snippets. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 418\u2013423. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_33"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-319-46520-3_29","volume-title":"Automated Technology for Verification and Analysis","author":"J Hua","year":"2016","unstructured":"Hua, J., Khurshid, S.: A sketching-based approach for debugging using test cases. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 463\u2013478. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_29"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Hua, J., Khurshid, S.: EdSketch: execution-driven sketching for Java. In: SPIN (2017)","DOI":"10.1145\/3092282.3092285"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Hua, J., Zhang, M., Wang, K., Khurshid, S.: Towards practical program repair with on-demand candidate generation. In: ICSE (2018)","DOI":"10.1145\/3180155.3180245"},{"key":"8_CR16","first-page":"256","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. TSE 11, 256\u2013290 (2002)","journal-title":"TSE"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/3-540-45500-0_25","volume-title":"Theoretical Aspects of Computer Software","author":"D Jackson","year":"2001","unstructured":"Jackson, D., Fekete, A.: Lightweight analysis of object interactions. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 492\u2013513. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45500-0_25"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA (2000)","DOI":"10.1145\/347324.383378"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Jeon, J., Qiu, X., Foster, J.S., Solar-Lezama, A.: JSketch: sketching for Java. In: FSE (2015)","DOI":"10.1145\/2786805.2803189"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226\u2013238. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_23"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Kang, E., Milicevic, A., Jackson, D.: Multi-representational security analysis. In: FSE (2016)","DOI":"10.1145\/2950290.2950356"},{"issue":"10","key":"8_CR22","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1145\/2544173.2509555","volume":"48","author":"Etienne Kneuss","year":"2013","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"100","DOI":"10.4204\/EPTCS.229.9","volume":"229","author":"Manos Koukoutos","year":"2016","unstructured":"Koukoutos, M., Kneuss, E., Kuncak, V.: An update on deductive synthesis and repair in the leon tool. In: SYNT Workshop (2016)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Long, F., Rinard, M.: Staged program repair with condition synthesis. In: FSE (2015)","DOI":"10.1145\/2786805.2786811"},{"key":"8_CR25","volume-title":"Theory of Relational Databases","author":"D Maier","year":"1983","unstructured":"Maier, D.: Theory of Relational Databases. Computer Science Press, Rockville (1983)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-662-43652-3_31","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"FA Maldonado-Lopez","year":"2014","unstructured":"Maldonado-Lopez, F.A., Chavarriaga, J., Donoso, Y.: Detecting network policy conflicts using alloy. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 314\u2013317. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_31"},{"issue":"6","key":"8_CR27","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/1064978.1065018","volume":"40","author":"David Mandelin","year":"2005","unstructured":"Mandelin, D., Xu, L., Bod\u00edk, R., Kimelman, D.: Jungloid mining: helping to navigate the API jungle. In: PLDI (2005)","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"8_CR28","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"Z Manna","year":"1971","unstructured":"Manna, Z., Waldinger, R.: Toward automatic program synthesis. CACM 14(3), 151\u2013165 (1971)","journal-title":"CACM"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-24485-8_44","volume-title":"Model Driven Engineering Languages and Systems","author":"Shahar Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: class diagrams analysis using Alloy revisited. In: MODELS (2011)"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-22655-7_12","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"S Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CDDiff: semantic differencing for class diagrams. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 230\u2013254. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22655-7_12"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: ASE (2001)","DOI":"10.1109\/ASE.2001.989787"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Nelson, T., Danas, N., Dougherty, D.J., Krishnamurthi, S.: The power of \u201cwhy\u201d and \u201cwhy not\u201d: enriching scenario exploration with provenance. In: FSE (2017)","DOI":"10.1145\/3106237.3106272"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"8_CR34","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: LISA (2010)"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Pei, Y., Furia, C.A., Nordio, M., Meyer, B.: Automated program repair in an integrated development environment. In: ICSE (2015)","DOI":"10.1109\/ICSE.2015.222"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Perelman, D., Gulwani, S., Grossman, D., Provost, P.: Test-driven synthesis. In: PLDI (2014)","DOI":"10.1145\/2594291.2594297"},{"issue":"6","key":"8_CR37","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1145\/2980983.2908093","volume":"51","author":"Nadia Polikarpova","year":"2016","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: PLDI (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Polozov, O., Gulwani, S.: FlashMeta: a framework for inductive program synthesis. In: OOPSLA (2015)","DOI":"10.1145\/2814270.2814310"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-45669-4_4","volume-title":"Object Modeling with the OCL","author":"M Richters","year":"2002","unstructured":"Richters, M., Gogolla, M.: OCL: syntax, semantics, and tools. In: Clark, T., Warmer, J. (eds.) Object Modeling with the OCL. LNCS, vol. 2263, pp. 42\u201368. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45669-4_4"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-319-48989-6_36","volume-title":"FM 2016: Formal Methods","author":"B-C Rothenberg","year":"2016","unstructured":"Rothenberg, B.-C., Grumberg, O.: Sound and complete mutation-based program repair. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 593\u2013611. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_36"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Ruchansky, N., Proserpio, D.: A (not) NICE way to verify the Openflow switch specification: formal modelling of the Openflow switch using Alloy. In: SIGCOMM (2013)","DOI":"10.1145\/2486001.2491711"},{"key":"8_CR42","volume-title":"Unified Modeling Language Reference Manual","author":"J Rumbaugh","year":"2004","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Education, London (2004)","edition":"2"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-319-21401-6_30","volume-title":"Automated Deduction - CADE-25","author":"S Saghafi","year":"2015","unstructured":"Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 434\u2013449. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_30"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: ASE (2003)","DOI":"10.1109\/ASE.2003.1240298"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: FSE (2011)","DOI":"10.1145\/2025113.2025153"},{"issue":"11","key":"8_CR46","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1145\/1168918.1168907","volume":"41","author":"Armando Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR47","unstructured":"Sullivan, A.: Automated testing and sketching of Alloy models. Ph.D. thesis, University of Texas at Austin (2017)"},{"key":"8_CR48","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Wang, K., Khurshid, S.: AUnit: a test automation tool for Alloy. In: ICST (2018)","DOI":"10.1109\/ICST.2018.00047"},{"key":"8_CR49","unstructured":"Sullivan, A., Wang, K., Khurshid, S., Marinov, D.: Evaluating state modeling techniques in alloy. In: SQAMIA (2017)"},{"key":"8_CR50","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: ICST (2017)","DOI":"10.1109\/ICST.2017.31"},{"key":"8_CR51","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Zaeem, R.N., Khurshid, S., Marinov, D.: Towards a test automation framework for alloy. In: SPIN (2014)","DOI":"10.1145\/2632362.2632369"},{"key":"8_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-68237-0_23","volume-title":"FM 2008: Formal Methods","author":"E Torlak","year":"2008","unstructured":"Torlak, E., Chang, F.S.-H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 326\u2013341. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_23"},{"key":"8_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"},{"issue":"6","key":"8_CR54","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1145\/2666356.2594334","volume":"49","author":"Vu Le","year":"2014","unstructured":"Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: PLDI, vol. 49, no. 6, pp. 216\u2013226 (2014)","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: MuAlloy: a mutation testing framework for alloy. In: ICSE (2018)","DOI":"10.1145\/3183440.3183488"},{"key":"8_CR56","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Marinov, D., Khurshid, S.: Solver-based sketching Alloy models using test valuations. In: ABZ (2018)","DOI":"10.1007\/978-3-319-91271-4_9"},{"key":"8_CR57","doi-asserted-by":"crossref","unstructured":"Weimer, W., Nguyen, T., Le Goues, C., Forrest, S.: Automatically finding patches using genetic programming. In: ICSE (2009)","DOI":"10.1109\/ICSE.2009.5070536"},{"key":"8_CR58","doi-asserted-by":"crossref","unstructured":"Yang, Z., Hua, J., Wang, K., Khurshid, S.: Test execution driven synthesis of API sequences with conditionals and loops. In: ICST (2018)","DOI":"10.1109\/ICST.2018.00025"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91271-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,17]],"date-time":"2019-10-17T12:51:13Z","timestamp":1571316673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91271-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912707","9783319912714"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91271-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}