{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:10Z","timestamp":1740122770631,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,1,18]],"date-time":"2021-01-18T00:00:00Z","timestamp":1610928000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,18]],"date-time":"2021-01-18T00:00:00Z","timestamp":1610928000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-15-C-0113"],"award-info":[{"award-number":["FA8750-15-C-0113"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1656926"],"award-info":[{"award-number":["1656926"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"crossref","award":["FA8650-18-2-7861"],"award-info":[{"award-number":["FA8650-18-2-7861"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,7]]},"DOI":"10.1007\/s10703-020-00359-9","type":"journal-article","created":{"date-parts":[[2021,1,18]],"date-time":"2021-01-18T10:03:12Z","timestamp":1610964192000},"page":"87-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["On solving quantified bit-vector constraints using invertibility conditions"],"prefix":"10.1007","volume":"57","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":[[2021,1,18]]},"reference":[{"key":"359_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Bod\u00edk R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: Formal methods in computer-aided design, FMCAD 2013, Portland, OR, USA, pp 1\u20138","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"359_CR2","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway CL, Deters M, Hadarean L, Jovanovi\u0107 D, King T, Reynolds A, Tinelli C (2011) CVC4. In: Proceedings of the 23rd international conference on computer aided verification, CAV\u201911, pp 171\u2013177. Springer-Verlag. http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032319","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"359_CR3","unstructured":"Barrett C, Stump A, Tinelli C (2010) 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)"},{"key":"359_CR4","unstructured":"Bj\u00f8rner N, Janota M (2015) Playing with quantified satisfaction. In: 20th International conferences on logic for programming, artificial intelligence and reasoning: short presentations, LPAR 2015, Suva, Fiji, pp 15\u201327"},{"key":"359_CR5","first-page":"91","volume-title":"Machine intelligence","author":"DC Cooper","year":"1972","unstructured":"Cooper DC (1972) Theorem proving in arithmetic without multiplication. In: Meltzer B, Michie D (eds) Machine intelligence, vol 7. Edinburgh University Press, Edinburgh, pp 91\u2013100"},{"key":"359_CR6","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS\u201908\/ETAPS\u201908, pp 337\u2013340. Springer. http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"359_CR7","doi-asserted-by":"crossref","unstructured":"Dutertre B (2014) Yices 2.2. In: Proceedings of 26th international conference, computer aided verification, CAV 2014, held as part of the vienna summer of logic, VSL 2014, Vienna, Austria, pp 737\u2013744","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"359_CR8","unstructured":"Dutertre B (2015) Solving exists\/forall problems in Yices. Workshop on Satisfiability Modulo Theories"},{"key":"359_CR9","doi-asserted-by":"crossref","unstructured":"Ekici B, Mebsout A, Tinelli C, Keller C, Katz G, Reynolds A, Barrett C (2017) SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar R, Kun\u010dak V (eds) Computer aided verification, lecture notes in computer science, vol 10427, pp 126\u2013133. Springer International Publishing","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"359_CR10","doi-asserted-by":"publisher","unstructured":"Ekici B, Viswanathan A, Zohar Y, Barrett C, Tinelli C (2019) Verifying bit-vector invertibility conditions in Coq (extended abstract). In: Reis G, Barbosa H (eds) Proceedings sixth workshop on proof exchange for theorem proving, electronic proceedings in theoretical computer science, vol 301, pp 57\u201389. Open Publishing Association. https:\/\/doi.org\/10.4204\/EPTCS.301","DOI":"10.4204\/EPTCS.301"},{"key":"359_CR11","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"2001","unstructured":"Enderton HB (2001) A mathematical introduction to logic, 2nd edn. Academic Press, New York","edition":"2"},{"key":"359_CR12","doi-asserted-by":"publisher","unstructured":"Ge Y, de\u00a0Moura LM (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani A, Maler O (eds) Proceedings, lecture notes in computer science 21st international conference computer aided verification, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009, vol 5643, pp 306\u2013320. Springer. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"359_CR13","doi-asserted-by":"publisher","unstructured":"Heizmann M, Chen Y, Dietsch D, Greitschus M, Nutz A, Musa B, Sch\u00e4tzle C, Schilling C, Sch\u00fcssele F, Podelski A (2017) Ultimate automizer with an on-demand construction of floyd-hoare automata\u2014(competition contribution). In: A.\u00a0Legay, T.\u00a0Margaria (eds) Tools and algorithms for the construction and analysis of systems; Proceedings of 23rd international conference, TACAS 2017, Held as Part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Part II, Lecture Notes in Computer Science, vol 10206, pp 394\u2013398. https:\/\/doi.org\/10.1007\/978-3-662-54580-5_30","DOI":"10.1007\/978-3-662-54580-5_30"},{"key":"359_CR14","unstructured":"Hilbert D, Bernays P (1934) Grundlagen der Mathematik. Verlag von Julius Springer, Die Grundlehren der mathematischen Wissenschaften"},{"issue":"3","key":"359_CR15","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/s10703-016-0260-9","volume":"49","author":"AK John","year":"2016","unstructured":"John AK, Chakraborty S (2016) A layered algorithm for quantifier elimination from linear modular constraints. Formal Methods Syst Des 49(3):272\u2013323. https:\/\/doi.org\/10.1007\/s10703-016-0260-9","journal-title":"Formal Methods Syst Des"},{"key":"359_CR16","doi-asserted-by":"crossref","unstructured":"Jon\u00e1s M, Strejcek J (2016) Solving quantified bit-vector formulas using binary decision diagrams. In: Proceedings of 19th international conference theory and applications of satisfiability testing SAT 2016, Bordeaux, France, pp 267\u2013283","DOI":"10.1007\/978-3-319-40970-2_17"},{"key":"359_CR17","doi-asserted-by":"crossref","unstructured":"Loos R, Weispfenning V (1993) Applying linear quantifier elimination","DOI":"10.1093\/comjnl\/36.5.450"},{"key":"359_CR18","unstructured":"Manzano M (1993) Introduction to many-sorted logic. Many-sorted logic and its applications. Wiley, New York, pp 3\u201386"},{"key":"359_CR19","doi-asserted-by":"crossref","unstructured":"Niemetz A, Preiner M, Biere A (2014 (published 2015)) Boolector 2.0 system description. J Satisfiabil Boolean Model Comput 9: 53\u201358","DOI":"10.3233\/SAT190101"},{"key":"359_CR20","doi-asserted-by":"crossref","unstructured":"Niemetz A, Preiner M, Biere A (2016) Precise and complete propagation based local search for satisfiability modulo theories. In: Proceedings of 28th International conference computer aided verification, CAV 2016, Toronto, ON, Canada, Part I, pp 199\u2013217","DOI":"10.1007\/978-3-319-41528-4_11"},{"issue":"3","key":"359_CR21","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 (2017) Propagation based local search for bit-precise reasoning. Formal Methods Syst Des 51(3):608\u2013636. https:\/\/doi.org\/10.1007\/s10703-017-0295-6","journal-title":"Formal Methods Syst Des"},{"key":"359_CR22","doi-asserted-by":"publisher","unstructured":"Niemetz A, Preiner M, Reynolds A, Barrett C, Tinelli C (2018) Solving quantified bit-vectors using invertibility conditions. In: Proceedings of the 30th international conference on computer aided verification (CAV 2018), Oxford, pp 236\u2013255. https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16","DOI":"10.1007\/978-3-319-96142-2_16"},{"key":"359_CR23","doi-asserted-by":"publisher","unstructured":"Niemetz A, Preiner M, Reynolds A, Zohar Y, Barrett CW, Tinelli C (2019) Towards bit-width-independent proofs in SMT solvers. In: Fontaine P (ed) Proceedings of the 27th international conference on automated deduction (CADE-27), Lecture Notes in Computer Science, vol 11716, pp 366\u2013384. Springer. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_22","DOI":"10.1007\/978-3-030-29436-6_22"},{"issue":"6","key":"359_CR24","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"key":"359_CR25","doi-asserted-by":"crossref","unstructured":"Preiner M, Niemetz A, Biere A (2017) 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, April 22-29, 2017, Proceedings, Part I, pp 264\u2013280","DOI":"10.1007\/978-3-662-54577-5_15"},{"key":"359_CR26","doi-asserted-by":"publisher","unstructured":"Reynolds A, Barbosa H, N\u00f6tzli A, Barrett CW, Tinelli C (2019) CVC4SY: Smart and fast term enumeration for syntax-guided synthesis. In: Dillig I, Tasiran S (eds) Proceedings of the 31st international conference on computer aided verification (CAV 2019), Lecture Notes in Computer Science, vol 11562, pp 74\u201383. Springer. https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"359_CR27","doi-asserted-by":"crossref","unstructured":"Reynolds A, Deters M, Kuncak V, Tinelli C, Barrett CW (2015) Counterexample-guided quantifier instantiation for synthesis in SMT. In: Proceedings of 27th international conference computer aided verification, CAV 2015, San Francisco, CA, USA, Part II, pp 198\u2013216","DOI":"10.1007\/978-3-319-21668-3_12"},{"issue":"3","key":"359_CR28","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 (2017) Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst Des 51(3):500\u2013532. https:\/\/doi.org\/10.1007\/s10703-017-0290-y","journal-title":"Formal Methods Syst Des"},{"key":"359_CR29","doi-asserted-by":"crossref","unstructured":"Stump A, Sutcliffe G, Tinelli C (2014) Starexec: a cross-community infrastructure for logic solving. In: Demri S, Kapur D, Weidenbach C (eds) Proceedings of the 7th international joint conference on automated reasoning, lecture notes in computer science, vol 8562, pp 367\u2013373. Springer","DOI":"10.1007\/978-3-319-08587-6_28"},{"issue":"1","key":"359_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"CM Wintersteiger","year":"2013","unstructured":"Wintersteiger CM, Hamadi Y, de Moura LM (2013) Efficiently solving quantified bit-vector formulas. Formal Methods Syst Des 42(1):3\u201323","journal-title":"Formal Methods Syst Des"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00359-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00359-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00359-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,22]],"date-time":"2021-07-22T08:37:21Z","timestamp":1626943041000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00359-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,18]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,7]]}},"alternative-id":["359"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00359-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,1,18]]},"assertion":[{"value":"1 June 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 December 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 January 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}