{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,31]],"date-time":"2026-10-31T20:49:13Z","timestamp":1793479753533,"version":"4.5.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961446","type":"print"},{"value":"9783319961453","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_32","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T22:25:55Z","timestamp":1532125555000},"page":"587-595","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":85,"title":["Btor2 , BtorMC and Boolector\u00a03.0"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2600-5283","authenticated-orcid":false,"given":"Aina","family":"Niemetz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clifford","family":"Wolf","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"32_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"32_CR2","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) format version 20071012. Technical report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr 69, 4040 Linz, Austria (2007)"},{"key":"32_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, p. 9. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102233","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"32_CR4","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr 69, 4040 Linz, Austria (2011)"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A., Lonsing, F.: BTOR: bit-precise modelling of word-level problems for model checking. In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT 2008\/BPR 2008, pp. 33\u201338. ACM, New York, USA (2008). http:\/\/doi.acm.org\/10.1145\/1512464.1512472","DOI":"10.1145\/1512464.1512472"},{"key":"32_CR6","first-page":"135","volume":"9","author":"G Cabodi","year":"2014","unstructured":"Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K.: Hardware model checking competition 2014: an analysis and comparison of solvers and benchmarks. J. Satisf. Boolean Model. Comput. 9, 135\u2013172 (2014). Published 2016","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"32_CR8","unstructured":"Cimatti, A., Roveri, M., Griggio, A., Irfan, A.: Verification modulo theories. http:\/\/es.fbk.eu\/projects\/vmt-lib\/"},{"key":"32_CR9","unstructured":"De Moura, L., Owre, S., Shankar, N.: The SAL language manual. Technical report CSL-01-01, Computer Science Laboratory, SRI International, Menlo Park (2003)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"32_CR11","unstructured":"Gisselquist, D.: ZipCPU. https:\/\/github.com\/ZipCPU\/zipcpu"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Ho, Y., Mishchenko, A., Brayton, R.K.: Property directed reachability with word-level abstraction. In: FMCAD, pp. 132\u2013139. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102251"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-642-22110-1_36","volume-title":"Computer Aided Verification","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Bj\u00f8rner, N., de Moura, L.: $$\\mu {Z} $$\u03bcZ - an efficient engine for fixed points with constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 457\u2013462. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_36"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Irfan, A., Cimatti, A., Griggio, A., Roveri, M., Sebastiani, R.: Verilog2SMV: a tool for word-level verification. In: DATE, pp. 1156\u20131159. IEEE (2016)","DOI":"10.3850\/9783981537079_0765"},{"issue":"1","key":"32_CR15","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.entcs.2005.07.021","volume":"144","author":"D Kroening","year":"2006","unstructured":"Kroening, D.: Computing over-approximations with bounded model checking. Electr. Notes Theor. Comput. Sci. 144(1), 79\u201392 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"32_CR16","unstructured":"Long, J., Ray, S., Sterin, B., Mishchenko, A., Brayton, R.K.: Enhancing ABC for stabilization verification of systemverilog\/VHDL models. In: Proceedings of the CEUR Workshop DIFTS@FMCAD, vol. 832. CEUR-WS.org (2011)"},{"key":"32_CR17","unstructured":"Niemetz, A., Biere, A.: ddSMT: a delta debugger for the SMT-LIB v2 format. In: Bruttomesso, R., Griggio, A. (eds.) Proceedings of the 11th International Workshop on Satisfiability Modulo Theories, SMT 2013, Affiliated with the 16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013, Helsinki, Finland, 8\u20139 July 2013, pp. 36\u201345 (2013)"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. JSAT 9, 53\u201358 (2015)","DOI":"10.3233\/SAT190101"},{"key":"32_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-41528-4_11","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2016","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Precise and complete propagation based local search for satisfiability modulo theories. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 199\u2013217. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_11"},{"key":"32_CR20","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Model-based API testing for SMT solvers. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017, Affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, 24\u201328 July 2017, p. 10 (2017)"},{"issue":"3","key":"32_CR21","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/s10703-017-0295-6","volume":"51","author":"A Niemetz","year":"2017","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3), 608\u2013636 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0295-6","journal-title":"Formal Methods Syst. Des."},{"key":"32_CR22","unstructured":"Niemetz, A., Preiner, M., Biere, A., Fr\u00f6hlich, A.: Improving local search for bit-vector logics in SMT with path propagation. In: Proceedings of the Fourth International Workshop on Design and Implementation of Formal Tools and Systems, Austin, USA, 26\u201327 September 2015, pp. 1\u201310 (2015)"},{"key":"32_CR23","unstructured":"Preiner, M., Niemetz, A., Biere, A.: Lemmas on demand for lambdas. In: Proceedings of the CEUR Workshop DIFTS@FMCAD, vol. 1130. CEUR-WS.org (2013)"},{"key":"32_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-662-54577-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Preiner","year":"2017","unstructured":"Preiner, M., Niemetz, A., Biere, A.: Counterexample-guided model synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 264\u2013280. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_15"},{"key":"32_CR25","unstructured":"SRI International\u2019s Computer Science Laboratory: Sally - a model checker for infinite-state systems. https:\/\/github.com\/SRI-CSL\/sally"},{"key":"32_CR26","unstructured":"Wolf, C.: PicoRV32. https:\/\/github.com\/cliffordwolf\/picorv32"},{"key":"32_CR27","unstructured":"Wolf, C.: PonyLink. https:\/\/github.com\/cliffordwolf\/PonyLink"},{"key":"32_CR28","unstructured":"Wolf, C.: riscv-formal. https:\/\/github.com\/cliffordwolf\/riscv-formal"},{"key":"32_CR29","unstructured":"Wolf, C.: Yosys. https:\/\/github.com\/YosysHQ\/yosys"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,6]],"date-time":"2020-11-06T11:16:24Z","timestamp":1604661384000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}