{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:03:02Z","timestamp":1767772982445,"version":"3.37.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961415"},{"type":"electronic","value":"9783319961422"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_16","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T19:55:08Z","timestamp":1532116508000},"page":"236-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Solving Quantified Bit-Vectors Using Invertibility Conditions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2600-5283","authenticated-orcid":false,"given":"Aina","family":"Niemetz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"16_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: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 1\u20138 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"16_CR2","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., et al.: 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 . http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032319"},{"key":"16_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"key":"16_CR4","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction. In: 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, 24\u201328 November 2015, pp. 15\u201327 (2015)"},{"key":"16_CR5","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 91\u2013100. Edinburgh University Press (1972)"},{"key":"16_CR6","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 . http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766"},{"key":"16_CR7","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"16_CR8","unstructured":"Dutertre, B.: Solving exists\/forall problems in yices. In: Workshop on Satisfiability Modulo Theories (2015)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-63390-9_7","volume-title":"Computer Aided Verification","author":"B Ekici","year":"2017","unstructured":"Ekici, B., et al.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 126\u2013133. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7"},{"key":"16_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., 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). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-662-54580-5_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2017","unstructured":"Heizmann, M., et al.: Ultimate automizer with an on-demand construction of Floyd-Hoare automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 394\u2013398. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_30"},{"key":"16_CR12","series-title":"Die Grundlehren der mathematischen Wissenschaften","volume-title":"Grundlagen der Mathematik","author":"D Hilbert","year":"1934","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik. Die Grundlehren der mathematischen Wissenschaften. Verlag von Julius Springer, Berlin (1934)"},{"issue":"3","key":"16_CR13","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). https:\/\/doi.org\/10.1007\/s10703-016-0260-9","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR14","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, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_17"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination (1993)","DOI":"10.1093\/comjnl\/36.5.450"},{"key":"16_CR16","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/SAT190101","volume":"9","author":"A Niemetz","year":"2014","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. J. Satisfiability Boolean Model. Comput. 9, 53\u201358 (2014). (published 2015)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-41528-4_11","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2016","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Precise and complete propagation based local search for satisfiability modulo theories. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 199\u2013217. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_11"},{"issue":"3","key":"16_CR18","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/s10703-017-0295-6","volume":"51","author":"A Niemetz","year":"2017","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3), 608\u2013636 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0295-6","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: On solving quantified bit-vectors using invertibility conditions. eprint arXiv:cs.LO\/1804.05025 (2018)","DOI":"10.1007\/978-3-319-96142-2_16"},{"issue":"6","key":"16_CR20","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Preiner, M., Niemetz, A., Biere, A.: Counterexample-guided model synthesis. In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 22\u201329 April 2017, Proceedings, Part I, pp. 264\u2013280 (2017)","DOI":"10.1007\/978-3-662-54577-5_15"},{"key":"16_CR22","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). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12"},{"issue":"3","key":"16_CR23","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51(3), 500\u2013532 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0290-y","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR24","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"},{"issue":"1","key":"16_CR25","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"CM Wintersteiger","year":"2013","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. Formal Methods Syst. Des. 42(1), 3\u201323 (2013)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,6]],"date-time":"2020-11-06T10:54:10Z","timestamp":1604660050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}