{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:52:11Z","timestamp":1781927531235,"version":"3.54.5"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,10,2]],"date-time":"2017-10-02T00:00:00Z","timestamp":1506902400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11408-N23"],"award-info":[{"award-number":["S11408-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10703-017-0295-6","type":"journal-article","created":{"date-parts":[[2017,10,2]],"date-time":"2017-10-02T09:33:09Z","timestamp":1506936789000},"page":"608-636","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Propagation based local search for bit-precise reasoning"],"prefix":"10.1007","volume":"51","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"}]},{"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":[[2017,10,2]]},"reference":[{"key":"295_CR1","unstructured":"Balint A, Belov A, Heule MJH, J\u00e4rvisalo M (eds) (2013) SAT competition 2013, Department of Computer Science Series of Publications B, vol B-2013-1. University of Helsinki"},{"key":"295_CR2","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1016\/j.artint.2015.01.002","volume":"223","author":"A Balint","year":"2015","unstructured":"Balint A, Belov A, J\u00e4rvisalo M, Sinz C (2015) Overview and analysis of the SAT challenge 2012 solver competition. Artif Intell 223:120\u2013155","journal-title":"Artif Intell"},{"key":"295_CR3","doi-asserted-by":"crossref","unstructured":"Balint A, Sch\u00f6ning U (2012) Choosing probability distributions for stochastic local search and the role of make versus break. In: SAT, Lecture Notes in Computer Science, vol 7317, pp 16\u201329. Springer","DOI":"10.1007\/978-3-642-31612-8_3"},{"key":"295_CR4","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV, Lecture Notes in Computer Science, vol 6806, pp 171\u2013177. Springer","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"295_CR5","unstructured":"Barrett C, Fontaine P, Tinelli C (2015) The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa. https:\/\/www.SMT-LIB.org"},{"key":"295_CR6","unstructured":"Barrett C, Stump A, Tinelli C (2010) SMT-LIB. https:\/\/www.SMT-LIB.org"},{"key":"295_CR7","unstructured":"Belov A, Heule MJH, J\u00e4rvisalo M (eds) (2014) SAT competition 2014, Department of Computer Science Series of Publications B, vol B-2014-2. University of Helsinki"},{"key":"295_CR8","unstructured":"Biere A (2016) Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In: SAT competition 2016\u2014solver and benchmark descriptions, Department of Computer Science Series of Publications B, vol B-2016-1, pp 44\u201345. University of Helsinki"},{"key":"295_CR9","doi-asserted-by":"crossref","unstructured":"Brummayer R (2009) Efficient SMT solving for bit-vectors and the extensional theory of arrays. Ph.D. thesis, Johannes Kepler University Linz","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"295_CR10","unstructured":"Bruttomesso R (2008) RTL verification: from SAT to SMT(BV). Ph.D. thesis, University of Trento"},{"key":"295_CR11","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Cimatti A, Franz\u00e9n A, Griggio A, Hanna Z, Nadel A, Palti A, Sebastiani R (2007) A lazy and layered SMT(BV) solver for hard industrial verification problems. In: CAV, Lecture Notes in Computer Science, vol 4590, pp 547\u2013560. Springer","DOI":"10.1007\/978-3-540-73368-3_54"},{"key":"295_CR12","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT solver. In: TACAS, Lecture Notes in Computer Science, vol 6015, pp 150\u2013153. Springer","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"295_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: TACAS, Lecture Notes in Computer Science, vol 7795, pp 93\u2013107. Springer","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"295_CR14","doi-asserted-by":"crossref","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS, Lecture Notes in Computer Science, vol 4963, pp 337\u2013340. Springer","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"295_CR15","doi-asserted-by":"crossref","unstructured":"de Moura LM, Jovanovic D (2013) A model-constructing satisfiability calculus. In: VMCAI, Lecture Notes in Computer Science, vol 7737, pp 1\u201312. Springer","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"295_CR16","doi-asserted-by":"crossref","unstructured":"Dutertre B (2014) Yices 2.2. In: CAV, Lecture Notes in Computer Science, vol 8559, pp 737\u2013744. Springer","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"295_CR17","unstructured":"Franzen A (2010) Efficient solving of the satisfiability modulo bit-vectors problem and some extensions to SMT. Ph.D. thesis, University of Trento"},{"key":"295_CR18","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich A, Biere A, Wintersteiger CM, Hamadi Y (2015) Stochastic local search for satisfiability modulo theories. In: Bonet B, Koenig S (eds) Proceedings of the twenty-ninth AAAI conference on artificial intelligence, Jan 25\u201330, 2015, Austin, Texas, USA, pp 1136\u20131143. AAAI Press","DOI":"10.1609\/aaai.v29i1.9372"},{"key":"295_CR19","unstructured":"Ganesh V (2007) Decision procedures for bit-vectors, arrays and integers. Ph.D. thesis, Stanford University"},{"key":"295_CR20","doi-asserted-by":"crossref","unstructured":"Ganesh V, Dill DL (2007) A decision procedure for bit-vectors and arrays. In: CAV, Lecture Notes in Computer Science, vol 4590, pp 519\u2013531. Springer","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"295_CR21","unstructured":"Godefroid P, Levin MY, Molnar DA (2008) Automated whitebox fuzz testing. In: NDSS. The Internet Society"},{"issue":"3","key":"295_CR22","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TC.1981.1675757","volume":"30","author":"P Goel","year":"1981","unstructured":"Goel P (1981) An implicit enumeration algorithm to generate tests for combinational logic circuits. IEEE Trans Comput 30(3):215\u2013222","journal-title":"IEEE Trans Comput"},{"key":"295_CR23","doi-asserted-by":"crossref","unstructured":"Griggio A, Phan Q, Sebastiani R, Tomasi S (2011) Stochastic local search for SMT: combining theory solvers with walksat. In: FroCoS, Lecture Notes in Computer Science, vol 6989, pp 163\u2013178. Springer","DOI":"10.1007\/978-3-642-24364-6_12"},{"key":"295_CR24","doi-asserted-by":"crossref","unstructured":"Hadarean L, Bansal K, Jovanovic D, Barrett C, Tinelli C (2014) A tale of two solvers: eager and lazy approaches to bit-vectors. In: CAV, Lecture Notes in Computer Science, vol 8559, pp 680\u2013695. Springer","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"295_CR25","unstructured":"Hansen TA (2012) A constraint solver and its application to machine code test generation. Ph.D. thesis, University of Melbourne"},{"key":"295_CR26","unstructured":"Hoos HH (1999) On the run-time behaviour of stochastic local search algorithms for SAT. In: AAAI\/IAAI, pp 661\u2013666. AAAI Press\/The MIT Press"},{"key":"295_CR27","doi-asserted-by":"crossref","unstructured":"Huang C, Cheng K (2000) Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. In: DAC, pp 118\u2013123","DOI":"10.1145\/337292.337333"},{"key":"295_CR28","doi-asserted-by":"crossref","unstructured":"Iyer MA (2003) Race: a word-level ATPG-based constraints solver system for smart random simulation. In: ITC, pp 299\u2013308. IEEE Computer Society","DOI":"10.1109\/TEST.2003.1270852"},{"key":"295_CR29","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107 D, Barrett C, de Moura L (2013) The design and implementation of the model constructing satisfiability calculus. In: Formal methods in computer-aided design, FMCAD 2013, Portland, OR, USA, Oct 20\u201323, 2013, pp 173\u2013180. IEEE","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"295_CR30","volume-title":"Decision procedures\u2014an algorithmic point of view. Texts in theoretical computer science. An EATCS series","author":"D Kroening","year":"2008","unstructured":"Kroening D, Strichman O (2008) Decision procedures\u2014an algorithmic point of view. Texts in theoretical computer science. An EATCS series. Springer, Heidelberg"},{"issue":"12","key":"295_CR31","doi-asserted-by":"crossref","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann A, Paruthi V, Krohm F, Ganai MK (2002) Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans CAD Integr Circuits Syst 21(12):1377\u20131394","journal-title":"IEEE Trans CAD Integr Circuits Syst"},{"key":"295_CR32","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2572-8","volume-title":"Reasoning in Boolean networks: logic synthesis and verification using testing techniques","author":"W Kunz","year":"1997","unstructured":"Kunz W, Stoffel D (1997) Reasoning in Boolean networks: logic synthesis and verification using testing techniques. Kluwer Academic Publishers, Norwell"},{"issue":"3","key":"295_CR33","first-page":"13","volume":"28","author":"Y Naveh","year":"2007","unstructured":"Naveh Y, Rimon M, Jaeger I, Katz Y, Vinov M, Marcus E, Shurek G (2007) Constraint-based random stimuli generation for hardware verification. AI Mag 28(3):13\u201330","journal-title":"AI Mag"},{"key":"295_CR34","first-page":"53","volume":"9","author":"A Niemetz","year":"2015","unstructured":"Niemetz A, Preiner M, Biere A (2015) Boolector 2.0. JSAT 9:53\u201358","journal-title":"JSAT"},{"key":"295_CR35","doi-asserted-by":"crossref","unstructured":"Niemetz A, Preiner M, Biere A (2016) Precise and complete propagation based local search for satisfiability modulo theories. In: CAV (1), Lecture Notes in Computer Science, vol 9779, pp 199\u2013217. Springer","DOI":"10.1007\/978-3-319-41528-4_11"},{"key":"295_CR36","unstructured":"Niemetz A, Preiner M, Biere A, Fr\u00f6hlich A (2015) Improving local search for bit-vector logics in SMT with path propagation. In: DIFTS@FMCAD, pp 1\u201310"},{"key":"295_CR37","unstructured":"Selman B, Kautz HA, Cohen B (1994) Noise strategies for improving local search. In: AAAI, pp 337\u2013343. AAAI Press\/The MIT Press"},{"key":"295_CR38","doi-asserted-by":"crossref","unstructured":"Tillmann N, Schulte W (2005) Parameterized unit tests. In: ESEC\/SIGSOFT FSE, pp 253\u2013262. ACM","DOI":"10.1145\/1081706.1081749"},{"key":"295_CR39","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu L, Hutter F, Hoos HH, Leyton-Brown K (2008) Satzilla: Portfolio-based algorithm selection for SAT. J Artif Intell Res (JAIR) 32:565\u2013606","journal-title":"J Artif Intell Res (JAIR)"},{"key":"295_CR40","volume-title":"Constraint-based verification","author":"J Yuan","year":"2006","unstructured":"Yuan J, Pixley C, Aziz A (2006) Constraint-based verification. Springer, Berlin"},{"key":"295_CR41","doi-asserted-by":"crossref","unstructured":"Zeljic A, Wintersteiger CM, R\u00fcmmer P (2016) Deciding bit-vector formulas with mcSAT. In: SAT, Lecture Notes in Computer Science, vol 9710, pp 249\u2013266. Springer","DOI":"10.1007\/978-3-319-40970-2_16"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0295-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0295-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0295-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,3]],"date-time":"2022-08-03T20:54:00Z","timestamp":1659560040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0295-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,2]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["295"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0295-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,2]]}}}