{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T06:05:58Z","timestamp":1790489158049,"version":"4.1.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216676","type":"print"},{"value":"9783319216683","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_12","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"198-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":82,"title":["Counterexample-Guided Quantifier Instantiation for Synthesis in SMT"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"12_CR1","unstructured":"Alur, R., et al.: Syntax-guided synthesis. To Appear in Marktoberdrof NATO proceedings. (2014). http:\/\/sygus.seas.upenn.edu\/files\/sygus_extended.pdf . Accessed 06 February 2015"},{"key":"12_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, pp. 1\u201317. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-319-13338-6_7","volume-title":"Hardware and Software: Verification and Testing","author":"R Alur","year":"2014","unstructured":"Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75\u201391. Springer, Heidelberg (2014)"},{"key":"12_CR4","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)"},{"issue":"3","key":"12_CR5","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10817-012-9246-5","volume":"50","author":"C Barrett","year":"2013","unstructured":"Barrett, C., Deters, M., de Moura, L.M., Oliveras, A., Stump, A.: 6 years of SMT-COMP. JAR 50(3), 243\u2013277 (2013)","journal-title":"JAR"},{"key":"12_CR6","doi-asserted-by":"crossref","first-page":"21","DOI":"10.3233\/SAT190028","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. J. Satisfiability Boolean Model. Comput. 3, 21\u201346 (2007)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-14203-1_27","volume-title":"Automated Reasoning","author":"N Bj\u00f8rner","year":"2010","unstructured":"Bj\u00f8rner, N.: Linear quantifier elimination as an abstract decision procedure. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 316\u2013330. Springer, Heidelberg (2010)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Efficient e-Matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"12_CR10","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM, Technical report (2003)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"12_CR12","first-page":"219","volume-title":"IJCAI","author":"CC Green","year":"1969","unstructured":"Green, C.C.: Application of theorem proving to problem solving. In: Walker, D.E., Norton, L.M. (eds.) IJCAI, pp. 219\u2013240. William Kaufmann, San Francisco (1969)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-18275-4_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Jacobs","year":"2011","unstructured":"Jacobs, S., Kuncak, V.: Towards complete reasoning about axiomatic specifications. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 6538, pp. 278\u2013293. Springer, Heidelberg (2011)"},{"key":"12_CR14","first-page":"215","volume-title":"ICSE","author":"S Jha","year":"2010","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) ICSE, pp. 215\u2013224. ACM, New York (2010)"},{"key":"12_CR15","first-page":"407","volume-title":"OOPSLA","author":"E Kneuss","year":"2013","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: Hosking, A.L., Eugster, P.T., Lopes, C.V. (eds.) OOPSLA, pp. 407\u2013426. ACM, New York (2013)"},{"key":"12_CR16","first-page":"316","volume-title":"PLDI","author":"V Kuncak","year":"2010","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: Zorn, B.G., Aiken, A. (eds.) PLDI, pp. 316\u2013329. ACM, New York (2010)"},{"issue":"2","key":"12_CR17","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/2076450.2076472","volume":"55","author":"V Kuncak","year":"2012","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. CACM 55(2), 103\u2013111 (2012)","journal-title":"CACM"},{"issue":"5\u20136","key":"12_CR18","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10009-011-0217-7","volume":"15","author":"V Kuncak","year":"2013","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. STTT 15(5\u20136), 455\u2013474 (2013)","journal-title":"STTT"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"762","DOI":"10.1007\/978-3-319-08867-9_51","volume-title":"Computer Aided Verification","author":"R Madhavan","year":"2014","unstructured":"Madhavan, R., Kuncak, V.: Symbolic resource bound inference for functional programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 762\u2013778. Springer, Heidelberg (2014)"},{"issue":"1","key":"12_CR20","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. TOPLAS 2(1), 90\u2013121 (1980)","journal-title":"TOPLAS"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-14295-6_51","volume-title":"Computer Aided Verification","author":"D Monniaux","year":"2010","unstructured":"Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 585\u2013599. Springer, Heidelberg (2010)"},{"key":"12_CR22","unstructured":"Raghothaman, M., Udupa, A.: Language to specify syntax-guided synthesis problems. In: CoRR, abs\/1405.5590 (2014)"},{"key":"12_CR23","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: On counterexample guided quantifier instantiation for synthesis in CVC4. In: CoRR, abs\/1502.04464, 2015. http:\/\/arxiv.org\/abs\/1502.04464"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-38574-2_26","volume-title":"Automated Deduction \u2013 CADE-24","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 377\u2013391. Springer, Heidelberg (2013)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., Moura, L.D.: Finding conflicting instances of quantified formulas in SMT. In: Formal Methods in Computer-Aided Design, FMCAD (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"12_CR26","unstructured":"Reynolds, A.J.: Finite Model Finding in Satisfiability Modulo Theories. Ph.D. thesis, The University of Iowa (2013)"},{"key":"12_CR27","first-page":"661","volume-title":"OSDI","author":"L Ryzhyk","year":"2014","unstructured":"Ryzhyk, L., Walker, A., Keys, J., Legg, A., Raghunath, A., Stumm, M., Vij, M.: User-guided device driver synthesis. In: Flinn, J., Levy, H. (eds.) OSDI, pp. 661\u2013676. USENIX Association, Berkeley (2014)"},{"issue":"5\u20136","key":"12_CR28","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1145\/1168857.1168907","volume-title":"ASPLOS","author":"A 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: Shen, J.P., Martonosi, M. (eds.) ASPLOS, pp. 404\u2013415. ACM, New York (2006)"},{"issue":"5\u20136","key":"12_CR30","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. STTT 15(5\u20136), 497\u2013518 (2013)","journal-title":"STTT"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, vol. 8562, pp. 367\u2013373. Springer, Heidelberg (2014)"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: Transit: specifying protocols with concolic snippets. In: PLDI, pp. 287\u2013296. ACM (2013)","DOI":"10.1145\/2499370.2462174"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,4]],"date-time":"2020-09-04T23:43:42Z","timestamp":1599263022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}