{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T12:36:38Z","timestamp":1789994198927,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662545768","type":"print"},{"value":"9783662545775","type":"electronic"}],"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-662-54577-5_15","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T10:48:06Z","timestamp":1490870886000},"page":"264-280","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Counterexample-Guided Model Synthesis"],"prefix":"10.1007","author":[{"given":"Mathias","family":"Preiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-93900-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 120\u2013135. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-93900-9_13"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-12002-2_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2010","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 236\u2013250. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-12002-2_19"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17\u201323 January 2010, pp. 313\u2013326. ACM (2010)","DOI":"10.1145\/1706299.1706337"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: 6th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2006, San Jose, California, USA, 12\u201316 November 2006, Proceedings, pp. 117\u2013124. IEEE Computer Society (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"issue":"2","key":"15_CR5","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s00224-015-9653-1","volume":"59","author":"G Kov\u00e1sznai","year":"2016","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: Complexity of fixed-size bit-vector logics. Theory Comput. Syst. 59(2), 323\u2013376 (2016)","journal-title":"Theory Comput. Syst."},{"key":"15_CR6","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). doi:10.1007\/978-3-642-22110-1_14"},{"key":"15_CR7","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","year":"2008","unstructured":"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_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-08867-9_49"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 198\u2013216. Springer, Cham (2015). doi:10.1007\/978-3-319-21668-3_12"},{"key":"15_CR10","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., 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). doi:10.1007\/978-3-642-02658-4_25"},{"key":"15_CR11","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. In: Bloem, R., Sharygina, N. (eds.) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, 20\u201323 October, pp. 239\u2013246. IEEE (2010)"},{"key":"15_CR12","unstructured":"Dutertre, B.: Solving exists\/forall problems in Yices. In: Workshop on Satisfiability Modulo Theories (2015)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-40970-2_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Jon\u00e1\u0161","year":"2016","unstructured":"Jon\u00e1\u0161, M., Strej\u010dek, J.: Solving quantified bit-vector formulas using binary decision diagrams. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 267\u2013283. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-40970-2_17"},{"key":"15_CR14","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: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"15_CR15","volume-title":"Handbook of Automated Reasoning","year":"2001","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 2s. Elsevier and MIT Press, Cambridge (2001)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In Boehm, H., Flanagan, C., eds.: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, 16\u201319 June 2013, pp. 287\u2013296. ACM (2013)","DOI":"10.1145\/2499370.2462174"},{"issue":"3","key":"15_CR17","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"15_CR18","unstructured":"Goultiaeva, A., Bacchus, F.: Exploiting QBF duality on a circuit representation. In: Fox, M., Poole, D. (eds.) Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, 11\u201315 July 2010. AAAI Press (2010)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Turbo-charging lemmas on demand with don\u2019t care reasoning. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 179\u2013186. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987611"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. J. Satisfiability Boolean Model. Comput. 9, 53\u201358 (2014) (2015, published)","DOI":"10.3233\/SAT190101"},{"key":"15_CR21","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/978-3-662-48899-7_42","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Fedyukovich","year":"2015","unstructured":"Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Automated discovery of simulation between programs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 606\u2013621. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-48899-7_42"},{"issue":"3","key":"15_CR23","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/s10703-016-0260-9","volume":"49","author":"AK John","year":"2016","unstructured":"John, A.K., Chakraborty, S.: A layered algorithm for quantifier elimination from linear modular constraints. Formal Methods Syst. Des. 49(3), 272\u2013323 (2016)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR24","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A., (eds.) 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015. EPiC Series in Computing, Suva, Fiji, 24\u201328 November 2015, vol. 35, pp. 15\u201327. EasyChair (2015)"},{"key":"15_CR25","unstructured":"Farzan, A., Kincaid, Z.: Linear arithmetic satisfiability via strategy improvement. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9\u201315 July 2016, pp. 735\u2013743. IJCAI\/AAAI Press (2016)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54577-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:33:55Z","timestamp":1618972435000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54577-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545768","9783662545775"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54577-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","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 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","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"}]}}