{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:23Z","timestamp":1776333383199,"version":"3.51.2"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,6,8]],"date-time":"2012-06-08T00:00:00Z","timestamp":1339113600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,2]]},"DOI":"10.1007\/s10703-012-0156-2","type":"journal-article","created":{"date-parts":[[2012,6,7]],"date-time":"2012-06-07T10:52:49Z","timestamp":1339066369000},"page":"3-23","source":"Crossref","is-referenced-by-count":45,"title":["Efficiently solving quantified bit-vector formulas"],"prefix":"10.1007","volume":"42","author":[{"given":"Christoph M.","family":"Wintersteiger","sequence":"first","affiliation":[]},{"given":"Youssef","family":"Hamadi","sequence":"additional","affiliation":[]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,6,8]]},"reference":[{"key":"156_CR1","unstructured":"Barrett C, Stump A, Tinelli C (2010) The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org"},{"key":"156_CR2","series-title":"LNCS","volume-title":"Proceedings of CAV","author":"C Barrett","year":"2007","unstructured":"Barrett C, Tinelli C (2007) CVC3. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin"},{"key":"156_CR3","series-title":"LNCS","volume-title":"Proceedings of LPAR","author":"M Benedetti","year":"2005","unstructured":"Benedetti M (2005) Evaluating QBFs via symbolic skolemization. In: Proceedings of LPAR. LNCS, vol\u00a03452. Springer, Berlin"},{"key":"156_CR4","series-title":"LNCS","volume-title":"Proceedings of SAT","author":"A Biere","year":"2005","unstructured":"Biere A (2005) Resolve and expand. In: Proceedings of SAT. LNCS, vol 3542. Springer, Berlin"},{"key":"156_CR5","series-title":"LNCS","volume-title":"Proceedings of TACAS","author":"R Brummayer","year":"2009","unstructured":"Brummayer R, Biere A (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: Proceedings of TACAS. LNCS, vol 5505. Springer, Berlin"},{"key":"156_CR6","series-title":"LNCS","volume-title":"Proceedings of CAV","author":"R Bruttomesso","year":"2008","unstructured":"Bruttomesso R, Cimatti A, Franz\u00e9n A, Griggio A, Sebastiani R (2008) The MathSAT 4 SMT solver. In: Proceedings of CAV. LNCS, vol 5123. Springer, Berlin"},{"key":"156_CR7","series-title":"LNCS","volume-title":"Proceedings of international symposium on logic based program synthesis and transformation","author":"M Col\u00f3n","year":"2005","unstructured":"Col\u00f3n M (2005) Schema-guided synthesis of imperative programs by constraint solving. In: Proceedings of international symposium on logic based program synthesis and transformation. LNCS, vol 3573. Springer, Berlin"},{"key":"156_CR8","series-title":"LNCS","volume-title":"Proceedings of TACAS","author":"B Cook","year":"2010","unstructured":"Cook B, Kroening D, R\u00fcmmer P, Wintersteiger CM (2010) Ranking function synthesis for bit-vector relations. In: Proceedings of TACAS. LNCS, vol 6015. Springer, Berlin"},{"key":"156_CR9","doi-asserted-by":"crossref","unstructured":"Egly U, Seidl M, Woltran S (2009) A solver for QBFs in negation normal form. Constraints 14(1)","DOI":"10.1007\/s10601-008-9055-y"},{"key":"156_CR10","series-title":"LNCS","volume-title":"Proceedings of CAV","author":"V Ganesh","year":"2007","unstructured":"Ganesh V, Dill DL (2007) A decision procedure for bit-vectors and arrays. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin"},{"key":"156_CR11","series-title":"LNCS","volume-title":"Proceedings of CAV","author":"Y Ge","year":"2009","unstructured":"Ge Y, de Moura L (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Proceedings of CAV. LNCS, vol 5643. Springer, Berlin"},{"key":"156_CR12","series-title":"LNCS","volume-title":"Proceedings of FMCAD","author":"E Giunchiglia","year":"2004","unstructured":"Giunchiglia E, Narizzano M, Tacchella A (2004) QuBE++: an efficient QBF solver. In: Proceedings of FMCAD. LNCS, vol 3312. Springer, Berlin"},{"key":"156_CR13","series-title":"LNCS","volume-title":"Proceedings of SAT","author":"A Goultiaeva","year":"2009","unstructured":"Goultiaeva A, Iverson V, Bacchus F (2009) Beyond CNF: a circuit-based QBF solver. In: Proceedings of SAT. LNCS, vol 5584. Springer, Berlin"},{"key":"156_CR14","series-title":"LNCS","volume-title":"Proceedings of VMCAI","author":"S Gulwani","year":"2009","unstructured":"Gulwani S, Srivastava S, Venkatesan R (2009) Constraint-based invariant inference over predicate abstraction. In: Proceedings of VMCAI. LNCS, vol 5403. Springer, Berlin"},{"key":"156_CR15","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of practical logic and automated reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press, Cambridge"},{"key":"156_CR16","doi-asserted-by":"crossref","unstructured":"Jain H, Kroening D, Sharygina N, Clarke EM (2008) Word-level predicate-abstraction and refinement techniques for verifying RTL verilog. IEEE Trans CAD Int Circuits Syst 27(2)","DOI":"10.1109\/TCAD.2007.907270"},{"key":"156_CR17","volume-title":"Proceedings of ICSE","author":"S Jha","year":"2010","unstructured":"Jha S, Gulwani S, Seshia S, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of ICSE. ACM, New York"},{"key":"156_CR18","volume-title":"Proceedings of FMCAD","author":"B Jobstmann","year":"2006","unstructured":"Jobstmann B, Bloem R (2006) Optimizations for LTL synthesis. In: Proceedings of FMCAD. IEEE, New York"},{"key":"156_CR19","volume-title":"Proceedings of conference on computational problems in abstract algebra","author":"DE Knuth","year":"1970","unstructured":"Knuth DE, Bendix PB (1970) Simple word problems in universal algebra. In: Proceedings of conference on computational problems in abstract algebra. Pergamon, New York"},{"key":"156_CR20","doi-asserted-by":"crossref","unstructured":"Lewis HR (1980) Complexity results for classes of quantificational formulas. J Comput Syst Sci 21(3)","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"156_CR21","series-title":"LNCS","volume-title":"Proceedings of SAT","author":"F Lonsing","year":"2010","unstructured":"Lonsing F, Biere A (2010) Integrating dependency schemes in search-based QBF solvers. In: Proceedings of SAT. LNCS, vol 6175. Springer, Berlin"},{"key":"156_CR22","series-title":"LNCS","volume-title":"Proceedings of CAV","author":"P Manolios","year":"2007","unstructured":"Manolios P, Srinivasan SK, Vroon D (2007) BAT: the bit-level analysis tool. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin"},{"key":"156_CR23","series-title":"LNCS","volume-title":"Proceedings of CADE","author":"L Moura de","year":"2007","unstructured":"de Moura L, Bj\u00f8rner N (2007) Efficient E-matching for SMT solvers. In: Proceedings of CADE. LNCS, vol 4603. Springer, Berlin"},{"key":"156_CR24","series-title":"LNCS","volume-title":"Proceedings of TACAS","author":"L Moura de","year":"2008","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: Proceedings of TACAS. LNCS, vol\u00a04963. Springer, Berlin"},{"key":"156_CR25","volume-title":"Proceedings of POPL","author":"A Pnueli","year":"1989","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of POPL. ACM, New York"},{"key":"156_CR26","series-title":"LNCS","volume-title":"Proceedings of VMCAI","author":"A Podelski","year":"2004","unstructured":"Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: Proceedings of VMCAI. LNCS, vol 2937. Springer, Berlin"},{"key":"156_CR27","volume-title":"Proceedings of PLDI","author":"A Solar-Lezama","year":"2008","unstructured":"Solar-Lezama A, Jones CG, Bod\u00edk R (2008) Sketching concurrent data structures. In: Proceedings of PLDI. ACM, New York"},{"key":"156_CR28","volume-title":"Proceedings of PLDI","author":"S Srivastava","year":"2009","unstructured":"Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: Proceedings of PLDI. ACM, New York"},{"key":"156_CR29","volume-title":"Proceedings of POPL","author":"S Srivastava","year":"2010","unstructured":"Srivastava S, Gulwani S, Foster JS (2010) From program verification to program synthesis. In: Proceedings of POPL. ACM, New York"},{"key":"156_CR30","series-title":"LNCS","volume-title":"Proceedings of SAT","author":"S Staber","year":"2007","unstructured":"Staber S, Bloem R (2007) Fault localization and correction with QBF. In: Proceedings of SAT. LNCS, vol 4501. Springer, Berlin"},{"key":"156_CR31","volume-title":"Report of a conference on high speed automatic calculating machines","author":"A Turing","year":"1949","unstructured":"Turing A (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines"},{"key":"156_CR32","volume-title":"Proceedings of the international conference on VLSI of system-on-chip","author":"R Wille","year":"2007","unstructured":"Wille R, Fey G, Gro\u00dfe D, Eggersgl\u00fc\u00dfS, Drechsler R (2007) Sword: a SAT like prover using word level information. In: Proceedings of the international conference on VLSI of system-on-chip. IEEE, New York"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0156-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0156-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0156-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,29]],"date-time":"2019-06-29T10:30:06Z","timestamp":1561804206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0156-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,8]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["156"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0156-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,8]]}}}