{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:34:31Z","timestamp":1725982471813},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319942049"},{"type":"electronic","value":"9783319942056"}],"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-94205-6_39","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T12:22:50Z","timestamp":1530274970000},"page":"591-608","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Datatypes with Shared Selectors"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[]},{"given":"Arjun","family":"Viswanathan","sequence":"additional","affiliation":[]},{"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"key":"39_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, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"39_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-319-21668-3_10","volume-title":"Computer Aided Verification","author":"R Alur","year":"2015","unstructured":"Alur, R., \u010cern\u00fd, P., Radhakrishna, A.: Synthesis through unification. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 163\u2013179. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_10"},{"key":"39_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.4204\/EPTCS.260.9","volume":"260","author":"Rajeev Alur","year":"2017","unstructured":"Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: SyGuS-comp 2017: results and analysis. In: Fisman, D., Jacobs, S. (eds.) Proceedings Sixth Workshop on Synthesis (SYNT). EPTCS, vol. 260, pp. 97\u2013115 (2017)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"39_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.4204\/EPTCS.260.9","volume":"260","author":"Rajeev Alur","year":"2017","unstructured":"Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: SyGuS-comp 2017: Results and analysis. CoRR, abs\/1711.11438 (2017)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"39_CR5","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":"39_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"39_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"39_CR8","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"39_CR9","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017)"},{"issue":"1\u20132","key":"39_CR10","first-page":"21","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1\u20132), 21\u201346 (2007)","journal-title":"JSAT"},{"key":"39_CR11","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"39_CR12","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, pp. 1:1\u20131:10. ACM (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"39_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_7"},{"key":"39_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107\u2013121. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_9"},{"key":"39_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-63046-5_8","volume-title":"Automated Deduction \u2013 CADE 26","author":"S Cruanes","year":"2017","unstructured":"Cruanes, S.: Satisfiability modulo bounded checking. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 114\u2013129. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_8"},{"key":"39_CR16","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 Moura de","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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"39_CR17","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1145\/1925844.1926423","volume":"46","author":"Sumit Gulwani","year":"2011","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL, pp. 317\u2013330. ACM (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"39_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-319-40229-1_2","volume-title":"Automated Reasoning","author":"S Gulwani","year":"2016","unstructured":"Gulwani, S.: Programming by examples: applications, algorithms, and ambiguity resolution. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 9\u201314. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_2"},{"issue":"1","key":"39_CR19","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/3093333.3009887","volume":"52","author":"Laura Kov\u00e1cs","year":"2017","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: POPL, pp. 260\u2013270. ACM (2017)","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"39_CR20","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1166\/asl.2012.2173","volume":"32","author":"KRM Leino","year":"2012","unstructured":"Leino, K.R.M.: Developing verified programs with Dafny. Ada Lett. 32(3), 9\u201310 (2012)","journal-title":"Ada Lett."},{"key":"39_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"3","key":"39_CR22","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10817-016-9372-6","volume":"58","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reason. 58(3), 341\u2013362 (2017)","journal-title":"J. Autom. Reason."},{"key":"39_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-319-40229-1_10","volume-title":"Automated Reasoning","author":"A Reynolds","year":"2016","unstructured":"Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 133\u2013151. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_10"},{"key":"39_CR24","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Kuncak, V., Tinelli, C., Barrett, C., Deters, M.: Refutation-based synthesis in SMT. Form. Methods Syst. Des. (2017)","DOI":"10.1007\/s10703-017-0270-2"},{"key":"39_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C.: SyGuS techniques in the core of an SMT solver. arXiv preprint arXiv:1711.10641 (2017)","DOI":"10.4204\/EPTCS.260.8"},{"key":"39_CR26","unstructured":"Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.: Datatypes with shared selectors. Technical report, The University of Iowa (2018). http:\/\/cvc4.cs.stanford.edu\/papers\/IJCAR2018-shsel\/"},{"issue":"11","key":"39_CR27","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., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"39_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T01:23:58Z","timestamp":1571534638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}