{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:20Z","timestamp":1776333380532,"version":"3.51.2"},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,9,7]],"date-time":"2015-09-07T00:00:00Z","timestamp":1441584000000},"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":["Theory Comput Syst"],"published-print":{"date-parts":[[2016,8]]},"DOI":"10.1007\/s00224-015-9653-1","type":"journal-article","created":{"date-parts":[[2015,9,7]],"date-time":"2015-09-07T02:26:08Z","timestamp":1441592768000},"page":"323-376","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Complexity of Fixed-Size Bit-Vector Logics"],"prefix":"10.1007","volume":"59","author":[{"given":"Gergely","family":"Kov\u00e1sznai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Fr\u00f6hlich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,7]]},"reference":[{"key":"9653_CR1","doi-asserted-by":"crossref","unstructured":"Ayari, A., Basin, D.A., Klaedtke, F.: Decision procedures for inductive boolean functions based on alternating automata. In: CAV, volume 1855 of LNCS. Springer (2000)","DOI":"10.1007\/10722167_16"},{"key":"9653_CR2","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Chiang, H.-J.K., Jiang, J.-H.R.: Henkin quantifiers and boolean formulae. In: Proceedings of the SAT\u201912 (2012)","DOI":"10.1007\/978-3-642-31612-8_11"},{"key":"9653_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)"},{"key":"9653_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proceedings of the 35th Design Automation Conference, pp 522\u2013527 (1998)","DOI":"10.1145\/277044.277186"},{"key":"9653_CR5","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Pichora, M.C.: Deciding fixed and non-fixed size bit-vectors. In: TACAS, volume 1384 of LNCS, pages 376\u2013392. Springer (1998)","DOI":"10.1007\/BFb0054184"},{"key":"9653_CR6","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: Sat-based model checking without unrolling. In: Proceedings of the VMCAI\u201911, pp. 70\u201387 (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"9653_CR7","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI, volume 3855 of Lecture Notes in Computer Science, pp. 427\u2013442. Springer (2006)","DOI":"10.1007\/11609773_28"},{"key":"9653_CR8","unstructured":"Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: Proceedings of the FMCAD\u201911, pp. 144\u2013153 (2011)"},{"key":"9653_CR9","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Boolector, A.B.: An efficient smt solver for bit-vectors and arrays. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"9653_CR10","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A., Florian, L.: BTOR: bit-precise modelling of word-level problems for model checking. In: Proceedings of the 1st International Workshop on Bit-Precise Reasoning, pp. 33\u201338. ACM, New York (2008)","DOI":"10.1145\/1512464.1512472"},{"key":"9653_CR11","unstructured":"Bruttomesso, R.: RTL Verification: From SAT to SMT(BV). PhD thesis, University of Trento (2008)"},{"key":"9653_CR12","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT SMT solver. In: CAV, volume 5123 of LNCS, pp. 299\u2013303. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"9653_CR13","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: ICCAD, pp. 13\u201320. IEEE (2009)","DOI":"10.1145\/1687399.1687403"},{"key":"9653_CR14","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems, TACAS\u201907, pp. 358\u2013372. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71209-1_28"},{"issue":"1\/2","key":"9653_CR15","first-page":"101","volume":"8","author":"U Bubeck","year":"2012","unstructured":"Bubeck, U., B\u00fcning, H.K.: Encoding nested boolean functions as quantified boolean formulas. JSAT 8(1\/2), 101\u2013116 (2012)","journal-title":"JSAT"},{"key":"9653_CR16","volume-title":"A bitvectors library for pvs. Technical report","author":"RW Butler","year":"1996","unstructured":"Butler, R.W., Miner, P.S., Srivas, M.K., Greve, D.A., Miller, S.P.: A bitvectors library for pvs. Technical report. NASA Langley Research Center, Hampton (1996)"},{"key":"9653_CR17","doi-asserted-by":"crossref","unstructured":"Chlebus, B.S.: From domino tilings to a new model of computation. In: Symposium on Computation Theory, vol. 208 of LNCS. Springer (1984)","DOI":"10.1007\/3-540-16066-3_4"},{"key":"9653_CR18","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv version 2: An opensource tool for symbolic model checking. In: Proceedings of the CAV02 (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"9653_CR19","doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: TACAS, vol. 6015 of LNCS. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_19"},{"key":"9653_CR20","unstructured":"Cook, S., Soltys, M.: Boolean programs and quantified propositional proof systems. Bulletin of the Section of Logic (1999)"},{"key":"9653_CR21","doi-asserted-by":"crossref","unstructured":"Cyrluk, D., Oliver, M., Harald, R.: An efficient decision procedure for a theory of fixed-sized bitvectors with composition and extraction. In: Computer-Aided Verification (CAV 97), pp. 60\u201371. Springer (1997)","DOI":"10.1007\/3-540-63166-6_9"},{"key":"9653_CR22","volume-title":"Z3: an efficient smt solver","author":"L De Moura","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient smt solver. Springer, Berlin (2008)"},{"key":"9653_CR23","unstructured":"Donini, F.M., Liberatore, P., Massacci, F., Schaerf, M.: Solving QBF with SMV. In: Proceedings of the KR\u201902, pp 578\u2013589 (2002)"},{"key":"9653_CR24","doi-asserted-by":"crossref","unstructured":"Downey, R.G., Fellows, M.R.: Parameterized Complexity, p 530. Springer (1999)","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"9653_CR25","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf (2006)"},{"key":"9653_CR26","unstructured":"Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: FMCAD\u201910, pp. 137\u2013144 (2010)"},{"key":"9653_CR27","unstructured":"Franz\u00e9n, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. PhD thesis, University of Trento (2010)"},{"key":"9653_CR28","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: Proceedings of the POS\u201912 (2012)"},{"key":"9653_CR29","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: Efficiently solving bit-vector problems using model checkers. In: Proceedings of the SMT\u201913 (2013)"},{"key":"9653_CR30","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Proceedings of the CSR\u201913 (2013)","DOI":"10.1007\/978-3-642-38536-0_33"},{"key":"9653_CR31","doi-asserted-by":"crossref","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer Aided Verification (CAV \u201907). Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_52"},{"issue":"3","key":"9653_CR32","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1145\/322077.322090","volume":"25","author":"MR Garey","year":"1978","unstructured":"Garey, M.R., Johnson, D.S.: NP-completeness results: Motivation, examples, and implications. J. ACM 25(3), 499\u2013508 (1978)","journal-title":"J. ACM"},{"key":"9653_CR33","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network Distributed Security Symposium (NDSS). Internet Society (2008)"},{"key":"9653_CR34","unstructured":"Henkin, L.: Some remarks on infinitely long formulas. In: Infinistic Methods, pp. 167\u2013183. Pergamon Press (1961)"},{"key":"9653_CR35","doi-asserted-by":"crossref","unstructured":"Johannsen, P.: Reducing bitvector satisfiability problems to scale down design sizes for RTL property checking. In: Proceedings of the High-Level Design Validation and Test Workshop, vol. 2001, pp 123\u2013128 (2001)","DOI":"10.1109\/HLDVT.2001.972818"},{"key":"9653_CR36","volume-title":"Speeding Up Hardware Verification by Automated Data Path Scaling. PhD thesis","author":"P Johannsen","year":"2002","unstructured":"Johannsen, P.: Speeding Up Hardware Verification by Automated Data Path Scaling. PhD thesis. CAU Kiel, Germany (2002)"},{"key":"9653_CR37","doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z., Kinanah, M., Voronkov, A.: Verifying equivalence of memories using a first order logic theorem prover. In: FMCAD\u201909, pp. 128\u2013135 (2009)","DOI":"10.1109\/FMCAD.2009.5351132"},{"key":"9653_CR38","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Anders, M., Schwartzbach, M.I.: Mona implementation secrets. In: Proceedings of the CIAA\u201900, pp. 182\u2013194 (2000)","DOI":"10.7146\/brics.v7i40.20206"},{"key":"9653_CR39","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 4A: Combinatorial Algorithms. Addison-Wesley (2011)"},{"key":"9653_CR40","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver \u2014 an instantiation-based theorem prover for first-order logic (system description). In: Proceedings of the IJCAR\u201908, IJCAR \u201908. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"9653_CR41","doi-asserted-by":"crossref","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: Proceedings of the SMT\u201912, pp. 44\u201355 (2012)","DOI":"10.29007\/cvnz"},{"key":"9653_CR42","doi-asserted-by":"crossref","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: bv2epr: A tool for polynomially translating quantifier-free bit-vector formulas into epr. In: Proceedings of the CADE\u201913 (2013)","DOI":"10.1007\/978-3-642-38574-2_32"},{"key":"9653_CR43","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: Quantifier-free bit-vector formulas with binary encoding: Benchmark description. In: Balint, A., Belov, A., Heule, M., J\u00e4rvisalo, M. (eds.) Proceedings of the SAT Competition 2013, vol. B-2013-1 of Department of Computer Science Series of Publications B, pp. 107\u2013108. University of Helsinki (2013)"},{"key":"9653_CR44","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer (2008)"},{"issue":"3","key":"9653_CR45","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"HR Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"key":"9653_CR46","doi-asserted-by":"crossref","unstructured":"Marx, M.: Complexity of modal logic. In: Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pp. 139\u2013179. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80006-1"},{"key":"9653_CR47","doi-asserted-by":"crossref","unstructured":"Niewerth, M., Schwentick, T.: Two-variable logic and key constraints on data words. In: ICDT, pp. 138\u2013149 (2011)","DOI":"10.1145\/1938551.1938571"},{"key":"9653_CR48","unstructured":"Papadimitriou, C.H.: Computational complexity. Addison-Wesley (1994)"},{"key":"9653_CR49","doi-asserted-by":"crossref","unstructured":"Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information (2001)","DOI":"10.1016\/S0898-1221(00)00333-3"},{"key":"9653_CR50","doi-asserted-by":"crossref","unstructured":"Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: FOCS, pp. 348\u2013363. IEEE Computer Society (1979)","DOI":"10.1109\/SFCS.1979.25"},{"issue":"2","key":"9653_CR51","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT 7(2), 156\u2013173 (2005)","journal-title":"STTT"},{"issue":"2","key":"9653_CR52","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177\u2013192 (1970)","journal-title":"J. Comput. Syst. Sci."},{"key":"9653_CR53","doi-asserted-by":"crossref","unstructured":"Schuele, T., Schneider, K.: Verification of data paths using unbounded integers: automata strike back. In: Proceedings of the 2nd international Haifa verification conference on Hardware and software, verification and testing, HVC\u201906, pp. 65\u201380. Springer-Verlag, Berlin (2007)","DOI":"10.1007\/978-3-540-70889-6_5"},{"issue":"3","key":"9653_CR54","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A Prasad Sistla","year":"1985","unstructured":"Prasad Sistla, A., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"9653_CR55","doi-asserted-by":"crossref","unstructured":"Spielmann, A., Kuncak, V.: On synthesis for unbounded bit-vector arithmetic. Technical report, EPFL, Lausanne, Switzerland (2012)","DOI":"10.1007\/978-3-642-31365-3_39"},{"key":"9653_CR56","doi-asserted-by":"crossref","unstructured":"Spielmann, A., Kuncak, V.: Synthesis for unbounded bitvector arithmetic. In: International Joint Conference on Automated Reasoning (IJCAR), LNAI. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_39"},{"key":"9653_CR57","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Raymond Strong, H. (eds.) STOC, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"key":"9653_CR58","unstructured":"Warren, H.S.: Hacker\u2019s Delight. Addison-Wesley Longman (2002)"},{"key":"9653_CR59","volume-title":"Termination Analysis for Bit-Vector Programs. PhD thesis","author":"CM Wintersteiger","year":"2011","unstructured":"Wintersteiger, C.M.: Termination Analysis for Bit-Vector Programs. PhD thesis. ETH Zurich, Switzerland (2011)"},{"key":"9653_CR60","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, M.L.: Efficiently solving quantified bit-vector formulas. In: Proceedings of the FMCAD, pp. 239\u2013246. IEEE (2010)"},{"key":"9653_CR61","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to presburger arithmetic constraints (extended abstract). In: Procedings of the Static Analysis Symposium, LNCS 983, pp. 21\u201332. Springer LNCS (1995)","DOI":"10.1007\/3-540-60360-3_30"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-015-9653-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-015-9653-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-015-9653-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T13:11:54Z","timestamp":1748610714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-015-9653-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,7]]},"references-count":61,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,8]]}},"alternative-id":["9653"],"URL":"https:\/\/doi.org\/10.1007\/s00224-015-9653-1","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,7]]}}}