{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:26Z","timestamp":1775873546319,"version":"3.50.1"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319912707","type":"print"},{"value":"9783319912714","type":"electronic"}],"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_9","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T14:32:55Z","timestamp":1525703575000},"page":"121-136","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Solver-Based Sketching of Alloy Models Using Test Valuations"],"prefix":"10.1007","author":[{"given":"Kaiyuan","family":"Wang","sequence":"first","affiliation":[]},{"given":"Allison","family":"Sullivan","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":"9_CR1","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":"9_CR2","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-013-0287-9","volume":"15","author":"R Bod\u00edk","year":"2013","unstructured":"Bod\u00edk, R., Jobstmann, B.: Algorithmic program synthesis: introduction. STTT 15, 397\u2013411 (2013)","journal-title":"STTT"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0743-1066(94)90029-9","volume":"19\u201320","author":"Y Deville","year":"1994","unstructured":"Deville, Y., Lau, K.K.: Logic program synthesis. J. Logic Program. 19\u201320, 321\u2013350 (1994)","journal-title":"J. Logic Program."},{"key":"9_CR4","unstructured":"Ernst, M.D.: Dynamically discovering likely program invariants. Ph.D. thesis, University of Washington Department of Computer Science and Engineering (2000)"},{"key":"9_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":"9_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":"9_CR7","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":"9_CR8","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":"9_CR9","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":"9_CR10","doi-asserted-by":"crossref","unstructured":"Hua, J., Khurshid, S.: EdSketch: Execution-driven sketching for Java. In: SPIN (2017)","DOI":"10.1145\/3092282.3092285"},{"key":"9_CR11","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":"9_CR12","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":"9_CR13","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":"9_CR14","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Malik, M.Z., Uzuncaova, E.: An automated approach for writing Alloy specifications using instances. In: ISoLA (2006)","DOI":"10.1109\/ISoLA.2006.44"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-21668-3_13","volume-title":"Computer Aided Verification","author":"E Kneuss","year":"2015","unstructured":"Kneuss, E., Koukoutos, M., Kuncak, V.: Deductive program repair. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 217\u2013233. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_13"},{"issue":"10","key":"9_CR17","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":"9_CR18","doi-asserted-by":"crossref","unstructured":"Krishnamurthi, S., Fisler, K., Dougherty, D.J., Yoo, D.: Alchemy: transmuting base Alloy specifications into implementations. In: FSE (2008)","DOI":"10.1145\/1453101.1453123"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Larson, E., Kirk, A.: Generating evil test strings for regular expressions. In: ICST (2016)","DOI":"10.1109\/ICST.2016.29"},{"issue":"6","key":"9_CR21","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 (2005)","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: ICSE (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"9_CR23","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":"9_CR24","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":"9_CR25","doi-asserted-by":"crossref","unstructured":"Osera, P.M., Zdancewic, S.: Type-and-example-directed program synthesis. In: PLDI (2015)","DOI":"10.1145\/2737924.2738007"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Perelman, D., Gulwani, S., Grossman, D., Provost, P.: Test-driven synthesis. In: PLDI (2014)","DOI":"10.1145\/2594291.2594297"},{"key":"9_CR27","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":"9_CR28","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-319-21690-4_23","volume-title":"Computer Aided Verification","author":"Rishabh Singh","year":"2015","unstructured":"Singh, R., Gulwani, S.: Predicting a correct program in programming by example. In: CAV (2015)"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: FSE (2011)","DOI":"10.1145\/2025113.2025153"},{"key":"9_CR30","unstructured":"Solar-Lezama, A.: Program synthesis by sketching. Ph.D. thesis, University of California, Berkeley (2008)"},{"issue":"6","key":"9_CR31","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/1273442.1250754","volume":"42","author":"Armando Solar-Lezama","year":"2007","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Sketching stencils. In: PLDI (2007)","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: PLDI (2008)","DOI":"10.1145\/1375581.1375599"},{"issue":"11","key":"9_CR33","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":"9_CR34","unstructured":"Sullivan, A.: Automated testing and sketching of Alloy models. Ph.D. thesis, University of Texas at Austin (2017)"},{"key":"9_CR35","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":"9_CR36","unstructured":"Sullivan, A., Wang, K., Khurshid, S., Marinov, D.: Evaluating state modeling techniques in Alloy. In: SQAMIA (2017)"},{"key":"9_CR37","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":"9_CR38","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":"9_CR39","unstructured":"Alloy Team: http:\/\/alloy.mit.edu\/alloy\/documentation\/alloy4-grammar.txt"},{"key":"9_CR40","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":"9_CR41","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"},{"key":"9_CR42","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":"9_CR43","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Koukoutos, M., Marinov, D., Khurshid, S.: Systematic generation of non-equivalent expressions for relational algebra. In: ABZ (2018)","DOI":"10.1007\/978-3-319-91271-4_8"},{"key":"9_CR44","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"},{"key":"9_CR45","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/2185376.2185383","volume":"42","author":"P Zave","year":"2012","unstructured":"Zave, P.: Using lightweight modeling to understand chord. SIGCOMM Comput. Commun. Rev. 42, 49\u201357 (2012)","journal-title":"SIGCOMM Comput. Commun. Rev."}],"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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,17]],"date-time":"2019-10-17T16:51:16Z","timestamp":1571331076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91271-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912707","9783319912714"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91271-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}