{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:31:27Z","timestamp":1725798687933},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662444641"},{"type":"electronic","value":"9783662444658"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44465-8_41","type":"book-chapter","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T06:33:02Z","timestamp":1407825182000},"page":"481-492","source":"Crossref","is-referenced-by-count":5,"title":["On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic"],"prefix":"10.1007","author":[{"given":"Gergely","family":"Kov\u00e1sznai","sequence":"first","affiliation":[]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Fr\u00f6hlich","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"41_CR1","doi-asserted-by":"crossref","unstructured":"Balc\u00e1zar, J.L., Lozano, A., Tor\u00e1n, J.: The complexity of algorithmic problems on succinct instances. Computer Science, 351\u2013377 (1992)","DOI":"10.1007\/978-1-4615-3422-8_30"},{"issue":"4","key":"41_CR2","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0020-0190(96)00096-8","volume":"59","author":"B. Borchert","year":"1996","unstructured":"Borchert, B., Lozano, A.: Succinct circuit representations and leaf language classes are basically the same concept. Inf. Process. Lett.\u00a059(4), 211\u2013215 (1996)","journal-title":"Inf. Process. Lett."},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-04921-2_23","volume-title":"Language and Automata Theory and Applications","author":"B. Das","year":"2014","unstructured":"Das, B., Scharpfenecker, P., Tor\u00e1n, J.: Succinct encodings of graph isomorphism. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol.\u00a08370, pp. 285\u2013296. Springer, Heidelberg (2014)"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Feigenbaum, J., Kannan, S., Vardi, M.Y., Viswanathan, M.: Complexity of problems on graphs represented as OBDDs. Chicago Journal of Theoretical Computer Science\u00a05(5) (1999)","DOI":"10.4086\/cjtcs.1999.005"},{"issue":"3","key":"41_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0019-9958(83)80004-7","volume":"56","author":"H. Galperin","year":"1983","unstructured":"Galperin, H., Wigderson, A.: Succinct representations of graphs. Information and Control\u00a056(3), 183\u2013198 (1983)","journal-title":"Information and Control"},{"issue":"1","key":"41_CR6","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0168-0072(98)00057-8","volume":"97","author":"G. Gottlob","year":"1999","unstructured":"Gottlob, G., Leone, N., Veith, H.: Succinctness as a source of complexity in logical formalisms. Annals of Pure and Applied Logic\u00a097(1), 231\u2013260 (1999)","journal-title":"Annals of Pure and Applied Logic"},{"key":"41_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-52292-1_20","volume-title":"Graph-Theoretic Concepts in Computer Science","author":"A. Lozano","year":"1990","unstructured":"Lozano, A., Balc\u00e1zar, J.L.: The complexity of graph problems for succinctly represented graphs. In: Nagl, M. (ed.) WG 1989. LNCS, vol.\u00a0411, pp. 277\u2013286. Springer, Heidelberg (1990)"},{"issue":"3","key":"41_CR8","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0019-9958(86)80009-2","volume":"71","author":"C.H. Papadimitriou","year":"1986","unstructured":"Papadimitriou, C.H., Yannakakis, M.: A note on succinct representations of graphs. Information and Control\u00a071(3), 181\u2013185 (1986)","journal-title":"Information and Control"},{"key":"41_CR9","unstructured":"Veith, H.: Succinct representation, leaf languages, and projection reductions. In: IEEE Conference on Computational Complexity, pp. 118\u2013126 (1996)"},{"issue":"5","key":"41_CR10","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0020-0190(97)00134-8","volume":"63","author":"H. Veith","year":"1997","unstructured":"Veith, H.: Languages represented by boolean formulas. Inf. Process. Lett.\u00a063(5), 251\u2013256 (1997)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"41_CR11","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1006\/inco.1997.2696","volume":"142","author":"H. Veith","year":"1998","unstructured":"Veith, H.: Succinct representation, leaf languages, and projection reductions. Information and Computation\u00a0142(2), 207\u2013236 (1998)","journal-title":"Information and Computation"},{"issue":"3","key":"41_CR12","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00289117","volume":"23","author":"K.W. Wagner","year":"1986","unstructured":"Wagner, K.W.: The complexity of combinatorial problems with succinct input representation. Acta Informatica\u00a023(3), 325\u2013356 (1986)","journal-title":"Acta Informatica"},{"key":"41_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-38536-0_33","volume-title":"Computer Science \u2013 Theory and Applications","author":"A. Fr\u00f6hlich","year":"2013","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: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol.\u00a07913, pp. 378\u2013390. Springer, Heidelberg (2013)"},{"key":"41_CR14","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proc. DAC 1998, pp. 522\u2013527 (1998)","DOI":"10.21236\/ADA400400"},{"key":"41_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BFb0054184","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N.S. Bj\u00f8rner","year":"1998","unstructured":"Bj\u00f8rner, N.S., Pichora, M.C.: Deciding fixed and non-fixed size bit-vectors. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 376\u2013392. Springer, Heidelberg (1998)"},{"key":"41_CR16","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":"41_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-63166-6_9","volume-title":"Computer Aided Verification","author":"D. Cyrluk","year":"1997","unstructured":"Cyrluk, D., M\u00f6ller, O., Rue\u00df, H.: An efficient decision procedure for a theory of fixed-sized bitvectors with composition and extraction. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 60\u201371. Springer, Heidelberg (1997)"},{"key":"41_CR18","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":"41_CR19","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Proc. SMT 2010 (2010)"},{"key":"41_CR20","first-page":"33","volume-title":"Proc. 1st International Workshop on Bit-Precise Reasoning","author":"R. Brummayer","year":"2008","unstructured":"Brummayer, R., Biere, A., Lonsing, F.: BTOR: bit-precise modelling of word-level problems for model checking. In: Proc. 1st International Workshop on Bit-Precise Reasoning, pp. 33\u201338. ACM, New York (2008)"},{"key":"41_CR21","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: Proc. SMT 2012, pp. 44\u201355 (2012)"},{"volume-title":"Model Checking","year":"1999","author":"E.M. Clarke Jr.","key":"41_CR22","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"41_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"41_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-73368-3_35","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2007","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: BAT: The bit-level analysis tool. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 303\u2013306. Springer, Heidelberg (2007)"},{"key":"41_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31612-8_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A.R. Bradley","year":"2012","unstructured":"Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 1\u201314. Springer, Heidelberg (2012)"},{"key":"41_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"41_CR27","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.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"41_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-540-70545-1_43","volume-title":"Computer Aided Verification","author":"P. Bjesse","year":"2008","unstructured":"Bjesse, P.: A practical approach to word level model checking of industrial netlists. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 446\u2013458. Springer, Heidelberg (2008)"},{"key":"41_CR29","unstructured":"Bjorner, N., McMillan, K., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: Proc. SMT 2012, pp. 3\u201311 (2013)"},{"key":"41_CR30","unstructured":"Veith, H.: How to encode a logical structure by an OBDD. In: Proc. 13th Annual IEEE Conference on Computational Complexity, pp. 122\u2013131. IEEE (1998)"},{"issue":"4","key":"41_CR31","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1137\/0216051","volume":"16","author":"N. Immerman","year":"1987","unstructured":"Immerman, N.: Languages that capture complexity classes. SIAM Journal on Computing\u00a016(4), 760\u2013778 (1987)","journal-title":"SIAM Journal on Computing"},{"key":"41_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/BFb0028031","volume-title":"Computer Science Logic","author":"T. Schwentick","year":"1998","unstructured":"Schwentick, T.: Padding and the expressive power of existential second-order logics. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol.\u00a01414, pp. 461\u2013477. Springer, Heidelberg (1998)"},{"key":"41_CR33","doi-asserted-by":"crossref","unstructured":"Immerman, N.: Descriptive complexity. Springer (1999)","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"41_CR34","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer (2008)"},{"issue":"6","key":"41_CR35","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1093\/logcom\/1.6.861","volume":"1","author":"I.A. Stewart","year":"1991","unstructured":"Stewart, I.A.: Complete problems involving boolean labelled structures and projection transactions. Journal of Logic and Computation\u00a01(6), 861\u2013882 (1991)","journal-title":"Journal of Logic and Computation"},{"key":"41_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/3-540-56992-8_25","volume-title":"Computer Science Logic","author":"I.A. Stewart","year":"1993","unstructured":"Stewart, I.A.: On completeness for NP via projection translations. In: Martini, S., B\u00f6rger, E., Kleine B\u00fcning, H., J\u00e4ger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol.\u00a0702, pp. 353\u2013366. Springer, Heidelberg (1993)"},{"issue":"1","key":"41_CR37","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/0022-0000(92)90043-I","volume":"45","author":"I.A. Stewart","year":"1992","unstructured":"Stewart, I.A.: Using the Hamiltonian path operator to capture NP. Journal of Computer and System Sciences\u00a045(1), 127\u2013151 (1992)","journal-title":"Journal of Computer and System Sciences"},{"issue":"2","key":"41_CR38","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF01195200","volume":"27","author":"I.A. Stewart","year":"1994","unstructured":"Stewart, I.A.: On completeness for NP via projection translations. Mathematical Systems Theory\u00a027(2), 125\u2013157 (1994)","journal-title":"Mathematical Systems Theory"},{"issue":"1","key":"41_CR39","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/0304-3975(94)00175-I","volume":"145","author":"I.A. Stewart","year":"1995","unstructured":"Stewart, I.A.: Complete problems for monotone NP. Theoretical Computer Science\u00a0145(1), 147\u2013157 (1995)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44465-8_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,14]],"date-time":"2022-04-14T03:05:21Z","timestamp":1649905521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44465-8_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662444641","9783662444658"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44465-8_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}