{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:47:13Z","timestamp":1725857233583},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_36","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"554-561","source":"Crossref","is-referenced-by-count":4,"title":["SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]},{"given":"Marius","family":"Lindauer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"36_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/978-3-642-38916-0_3","volume-title":"Tests and Proofs","author":"C Artho","year":"2013","unstructured":"Artho, C., Biere, A., Seidl, M.: Model-based testing for verification back-ends. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 39\u201355. Springer, Heidelberg (2013)"},{"key":"36_CR2","unstructured":"Balint, A., Manthey, N.: SparrowToRiss. In: Belov et al. [3], pp. 77\u201378"},{"key":"36_CR3","unstructured":"Belov, A., Diepold, D., Heule, M., J\u00e4rvisalo, M. (eds.): Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2014-2. University of Helsinki (2014)"},{"key":"36_CR4","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Proceedings of SAT Competition 2013, pp. 51\u201352 (2013)"},{"key":"36_CR5","unstructured":"Biere, A.: Yet another local search solver and Lingeling and friends entering the SAT competition. In: Belov et al. [3], pp. 39\u201340 (2014)"},{"key":"36_CR6","unstructured":"Biere, A., Cimatti, A., Claessen, K.L., Jussila, T., McMillan, K., Somenzi, F.: Benchmarks from the 2008 hardware model checking competition (HWMCC 2008) (2008). http:\/\/fmv.jku.at\/hwmcc08\/benchmarks.html"},{"key":"36_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/978-3-642-14186-7_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"R Brummayer","year":"2010","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44\u201357. Springer, Heidelberg (2010)"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-24318-4_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"S Falkner","year":"2015","unstructured":"Falkner, S., Lindauer, M., Hutter, F.: SpySMAC: automated configuration and performance analysis of SAT solvers. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 215\u2013222. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24318-4_16"},{"key":"36_CR9","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.artint.2012.04.001","volume":"187\u2013188","author":"M Gebser","year":"2012","unstructured":"Gebser, M., Kaufmann, B., Schaub, T.: Conflict-driven answer set solving: from theory to practice. Artif. Intell. 187\u2013188, 52\u201389 (2012)","journal-title":"Artif. Intell."},{"key":"36_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-642-13520-0_23","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"F Hutter","year":"2010","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Automated configuration of mixed integer programming solvers. In: Lodi, A., Milano, M., Toth, P. (eds.) CPAIOR 2010. LNCS, vol. 6140, pp. 186\u2013202. Springer, Heidelberg (2010)"},{"key":"36_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/978-3-642-25566-3_40","volume-title":"Learning and Intelligent Optimization","author":"F Hutter","year":"2011","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507\u2013523. Springer, Heidelberg (2011)"},{"key":"36_CR12","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1613\/jair.2861","volume":"36","author":"F Hutter","year":"2009","unstructured":"Hutter, F., Hoos, H., Leyton-Brown, K., St\u00fctzle, T.: ParamILS: an automatic algorithm configuration framework. JAIR 36, 267\u2013306 (2009)","journal-title":"JAIR"},{"key":"36_CR13","unstructured":"Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H.H., Leyton-Brown, K.: The configurable SAT solver challenge. CoRR (2015). http:\/\/arxiv.org\/abs\/1505.01221"},{"key":"36_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"36_CR15","unstructured":"Manthey, N.: Riss 4.27. In: Belov et al. [3], pp. 65\u201367"},{"issue":"50","key":"36_CR16","doi-asserted-by":"crossref","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Maric","year":"2010","unstructured":"Maric, F.: Formal verification of a modern SAT solver by shallow embedding into isabelle\/hol. Theor. Comput. Sci. 411(50), 4333\u20134356 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"36_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-642-27940-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Oe","year":"2012","unstructured":"Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: a verified modern SAT solver. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 7148, pp. 363\u2013378. Springer, Heidelberg (2012)"},{"key":"36_CR18","unstructured":"Oh, C.: MiniSat HACK 999ED, MiniSat HACK 1430ED and SWDiA5BY. In: Belov et al.[3], p. 46"},{"issue":"4","key":"36_CR19","doi-asserted-by":"crossref","first-page":"139","DOI":"10.3233\/SAT190083","volume":"7","author":"O Roussel","year":"2011","unstructured":"Roussel, O.: Controlling a solver execution with the runsolver tool. J. Satisfiability Boolean Model. Comput. 7(4), 139\u2013144 (2011)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"issue":"7","key":"36_CR20","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V Silva","year":"2008","unstructured":"Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"36_CR21","unstructured":"Soos, M.: CryptoMiniSat v4. In: Belov et al. [3], p. 23"},{"key":"36_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/11499107_25","volume-title":"Theory and Applications of Satisfiability Testing","author":"E Zarpas","year":"2005","unstructured":"Zarpas, E.: Benchmarking SAT solvers for bounded model checking. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 340\u2013354. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T01:28:00Z","timestamp":1600738080000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}