{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:59:31Z","timestamp":1725728371212},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385353"},{"type":"electronic","value":"9783642385360"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38536-0_33","type":"book-chapter","created":{"date-parts":[[2013,6,2]],"date-time":"2013-06-02T21:03:04Z","timestamp":1370206984000},"page":"378-390","source":"Crossref","is-referenced-by-count":8,"title":["More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Fr\u00f6hlich","sequence":"first","affiliation":[]},{"given":"Gergely","family":"Kov\u00e1sznai","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","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.\u00a0SMT 2012, pp. 44\u201355 (2012)"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Cyrluk, D., M\u00f6ller, O., Rue\u00df, H.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 60\u201371. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_9"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proc.\u00a0DAC 1998, pp. 522\u2013527 (1998)","DOI":"10.21236\/ADA400400"},{"key":"33_CR4","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. Bj\u00f8rner","year":"1998","unstructured":"Bj\u00f8rner, N., 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":"33_CR5","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: Proc.\u00a0ICCAD 2009, pp. 13\u201320. IEEE (2009)","DOI":"10.1145\/1687399.1687403"},{"key":"33_CR6","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":"33_CR7","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Proc. SMT 2010, Edinburgh, UK (2010)"},{"key":"33_CR8","first-page":"33","volume-title":"Proc. BPR 2008","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. BPR 2008, pp. 33\u201338. ACM, New York (2008)"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/10722167_16","volume-title":"Computer Aided Verification","author":"A. Ayari","year":"2000","unstructured":"Ayari, A., Basin, D.A., Klaedtke, F.: Decision procedures for inductive boolean functions based on alternating automata. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 170\u2013186. Springer, Heidelberg (2000)"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-642-31365-3_39","volume-title":"Automated Reasoning","author":"A. Spielmann","year":"2012","unstructured":"Spielmann, A., Kuncak, V.: Synthesis for unbounded bit-vector arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 499\u2013513. Springer, Heidelberg (2012)"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"33_CR12","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. In: Proc. FMCAD 2010, pp. 239\u2013246. IEEE (2010)"},{"key":"33_CR13","unstructured":"Wintersteiger, C.M.: Termination Analysis for Bit-Vector Programs. PhD thesis, ETH Zurich, Switzerland (2011)"},{"key":"33_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-12002-2_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Cook","year":"2010","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 236\u2013250. Springer, Heidelberg (2010)"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Spielmann, A., Kuncak, V.: On synthesis for unbounded bit-vector arithmetic. Technical report, EPFL, Lausanne, Switzerland (February 2012)","DOI":"10.1007\/978-3-642-31365-3_39"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Johannsen, P.: Reducing bitvector satisfiability problems to scale down design sizes for RTL property checking. In: Proc.\u00a0HLDVT 2001, 123\u2013128 (2001)","DOI":"10.1109\/HLDVT.2001.972818"},{"key":"33_CR17","unstructured":"Johannsen, P.: Speeding Up Hardware Verification by Automated Data Path Scaling. PhD thesis, CAU Kiel, Germany (2002)"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: Proc.\u00a0FOCS 1979, pp. 348\u2013363 (1979)","DOI":"10.1109\/SFCS.1979.25"},{"issue":"2","key":"33_CR19","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M.R. Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT\u00a07(2), 156\u2013173 (2005)","journal-title":"STTT"},{"key":"33_CR20","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 4A: Combinatorial Algorithms. Addison-Wesley (2011)"},{"key":"33_CR21","unstructured":"Donini, F.M., Liberatore, P., Massacci, F., Schaerf, M.: Solving QBF with SMV. In: Proc.\u00a0KR 2002, pp. 578\u2013589 (2002)"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Davis, M., Matijasevich, Y., Robinson, J.: Hilbert\u2019s tenth problem: Diophantine equations: positive aspects of a negative solution. In: Proc.\u00a0Sympos. Pure Mathematics, vol.\u00a028, pp. 323\u2013378 (1976)","DOI":"10.1090\/pspum\/028.2\/0432534"},{"key":"33_CR23","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: Proc. POS 2012 (2012)"},{"key":"33_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"33_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-14186-7_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 158\u2013171. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Computer Science \u2013 Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38536-0_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,14]],"date-time":"2019-07-14T07:43:03Z","timestamp":1563090183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38536-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385353","9783642385360"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38536-0_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}