{"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":1776333383255,"version":"3.51.2"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662626","type":"print"},{"value":"9783319662633","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_23","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T04:05:11Z","timestamp":1502165111000},"page":"364-379","source":"Crossref","is-referenced-by-count":3,"title":["On Simplification of Formulas with Unconstrained Variables and Quantifiers"],"prefix":"10.1007","author":[{"given":"Martin","family":"Jon\u00e1\u0161","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"23_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). \nwww.SMT-LIB.org"},{"key":"23_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). \nwww.SMT-LIB.org"},{"key":"23_CR3","first-page":"825","volume":"185","author":"CW Barrett","year":"2009","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. Handb. Satisf. 185, 825\u2013885 (2009). IOS Press,","journal-title":"Handb. Satisf."},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-319-14896-0_5","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"P Bauch","year":"2014","unstructured":"Bauch, P., Havel, V., Barnat, J.: LTL model checking of LLVM bitcode with symbolic data. In: Hlin\u011bn\u00fd, P., Dvo\u0159\u00e1k, Z., Jaro\u0161, J., Kofro\u0148, J., Ko\u0159enek, J., Matula, P., Pala, K. (eds.) MEMICS 2014. LNCS, vol. 8934, pp. 47\u201359. Springer, Cham (2014). doi:\n10.1007\/978-3-319-14896-0_5"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). doi:\n10.1007\/978-3-662-46681-0_31"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-23404-5_12","volume-title":"Model Checking Software","author":"D Beyer","year":"2015","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Benchmarking and resource measurement. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 160\u2013178. Springer, Cham (2015). doi:\n10.1007\/978-3-319-23404-5_12"},{"key":"23_CR7","unstructured":"Brummayer, R.: Efficient SMT solving for bit vectors and the extensional theory of arrays. Ph.D. thesis, Johannes Kepler University of Linz (2010)"},{"key":"23_CR8","unstructured":"Bruttomesso, R.: RTL Verification: From SAT to SMT(BV). Ph.D. thesis, University of Trento (2008)"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, 29 March - 6 April 2008, pages 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"23_CR10","unstructured":"Franz\u00e9n, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Ph.D. thesis, University of Trento (2010)"},{"key":"23_CR11","unstructured":"Hadarean, L.: An Efficient and Trustworthy Theory Solver for Bit-vectors in Satisfiability Modulo Theories. Ph.D. thesis, New York University (2015)"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-40970-2_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Jon\u00e1\u0161","year":"2016","unstructured":"Jon\u00e1\u0161, M., Strej\u010dek, J.: Solving quantified bit-vector formulas using binary decision diagrams. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 267\u2013283. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40970-2_17"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Preiner, M., Niemetz, A., Biere, A.: Counterexample-guided model synthesis. In: Proceedings of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Part I, Uppsala, Sweden, 22\u201329 April 2017, pp. 264\u2013280 (2017)","DOI":"10.1007\/978-3-662-54577-5_15"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T14:50:32Z","timestamp":1502203832000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}