{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T18:48:54Z","timestamp":1776106134720,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141850","type":"print"},{"value":"9783642141867","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-14186-7_6","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:20:37Z","timestamp":1278627637000},"page":"44-57","source":"Crossref","is-referenced-by-count":46,"title":["Automated Testing and Debugging of SAT and QBF Solvers"],"prefix":"10.1007","author":[{"given":"Robert","family":"Brummayer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Ans\u00f3tegui, C., B\u00e9jar, R., Fern\u00e1ndez, C., Mateu, C.: Generating Hard SAT\/CSP Instances Using Expander Graphs. In: AAAI (2008)"},{"key":"6_CR2","unstructured":"Babi\u0107, D.: Exploiting Structure for Scalable Software Verification. PhD thesis, University of British Columbia, Vancouver, Canada (2008)"},{"key":"6_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: A Suite to Evaluate and Certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"6_CR4","unstructured":"Le Berre, D.: SAT4J: Bringing the Power of SAT Technology to the Java Platform, http:\/\/www.sat4j.org"},{"key":"6_CR5","unstructured":"Le Berre, D., Roussel, O., Simon, L.: SAT 2009 Competitive Events Booklet - Preliminary Version. In: SAT competition solver descriptions (September 2009), http:\/\/www.cril.univ-artois.fr\/SAT09\/solvers\/booklet.pdf"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A.: Resolve and Expand. In: SAT (Selected Papers) (2004)","DOI":"10.1007\/11527695_5"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A.: PicoSAT Essentials. JSAT\u00a04 (2008)","DOI":"10.3233\/SAT190039"},{"key":"6_CR8","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M. Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The Barcelogic SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 294\u2013298. Springer, Heidelberg (2008)"},{"key":"6_CR10","unstructured":"Bregman, D., Mitchell, D.: The SAT solver MXC, Version 0.5., SAT competition solver description (2007)"},{"key":"6_CR11","series-title":"ACM International Conference Proceedings Series","volume-title":"SMT","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Fuzzing and Delta-Debugging SMT Solvers. In: SMT. ACM International Conference Proceedings Series. ACM, New York (2009)"},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for Quantified Boolean Formulas. Inf. Comput.\u00a0117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation. J. Autom. Reasoning\u00a028 (2002)","DOI":"10.1023\/A:1015019416843"},{"key":"6_CR14","unstructured":"Chen, H., Interian, Y.: A Model for Generating Random Quantified Boolean Formulas. In: IJCAI (2005)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a Lightweight Tool for Random Testing of Haskell Programs. ICFP\u00a035(9) (2000)","DOI":"10.1145\/357766.351266"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-79719-7_5","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"N. Creignou","year":"2008","unstructured":"Creignou, N., Daud\u00e9, H., Egly, U., Rossignol, R.: New Results on the Phase Transition for Random Quantified Boolean Formulas. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 34\u201347. Springer, Heidelberg (2008)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem-Proving. ACM Commun.\u00a05 (1962)","DOI":"10.1145\/368273.368557"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"6_CR19","unstructured":"Freeman, J.W.: Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, Depart.\u00a0of Comp.\u00a0and Inf.\u00a0Science, University of Pennsylvania (1995)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-04238-6_50","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Gebser","year":"2009","unstructured":"Gebser, M., Kaufmann, B., Schaub, T.: The Conflict-Driven Answer Set Solver clasp: Progress Report. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol.\u00a05753, pp. 509\u2013514. Springer, Heidelberg (2009)"},{"key":"6_CR21","unstructured":"Van Gelder, A.: Extracting (Easily) Checkable Proofs from a Satisfiability Solver that Employs both Preorder and Postorder Resolution. In: AMAI (2002)"},{"key":"6_CR22","unstructured":"Gent, I., Walsh, T.: The SAT Phase Transition. In: ECAI (1994)"},{"key":"6_CR23","unstructured":"Gent, I., Walsh, T.: Beyond NP: the QSAT phase transition. In: AAAI\/IAAI (1999)"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-30494-4_15","volume-title":"Formal Methods in Computer-Aided Design","author":"E. Giunchiglia","year":"2004","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: An Efficient QBF Solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 201\u2013213. Springer, Heidelberg (2004)"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Jabbour, S.: ManySAT: a Parallel SAT Solver. JSAT\u00a06 (2009)","DOI":"10.3233\/SAT190070"},{"key":"6_CR26","unstructured":"Heule, M.: SmArT Solving: Tools and Techniques for Satisfiability Solvers. PhD thesis, TU Delft (2008)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Horie, S., Watanabe, O.: Hard instance generation for SAT. CoRR, cs.CC\/9809117 (1998)","DOI":"10.1007\/3-540-63890-3_4"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-02777-2_35","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"E. Hsu","year":"2009","unstructured":"Hsu, E., McIlraith, S.: VARSAT: Integrating Novel Probabilistic Interference Techniques with DPLL Search. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 377\u2013390. Springer, Heidelberg (2009)"},{"key":"6_CR29","unstructured":"Huang, J.: TINISAT in SAT Competition 2007. SAT competition solver description (2007)"},{"key":"6_CR30","unstructured":"Jain, H., Clarke, E.: SAT Solver Descriptions: CMUSAT-Base and CMUSAT. SAT competition solver description (2007)"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"T. Jussila","year":"2007","unstructured":"Jussila, T., Biere, A., Sinz, C., Kr\u00f6ning, D., Wintersteiger, C.: A First Step Towards a Unified Proof Checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 201\u2013214. Springer, Heidelberg (2007)"},{"key":"6_CR32","unstructured":"Kern, C., Khaleghi, M., Kugele, S., Schallhart, C., Tautschnig, M., Weis, A.: SAT 7 - Engineering a Modular SAT-Solver. SAT competition solver description (2007)"},{"key":"6_CR33","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, p. 160. Springer, Heidelberg (2002)"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT Solving. In: Asia and South Pacific DAC (2007)","DOI":"10.1109\/ASPDAC.2007.358108"},{"key":"6_CR35","unstructured":"Lonsing, F.: DepQBF 0.1 Source Code (2010), http:\/\/fmv.jku.at\/depqbf\/"},{"key":"6_CR36","unstructured":"Miller, B., Koski, D., Lee, C., Maganty, V., Murthy, R., Natarajan, A., Steidl, J.: Fuzz Revisited: A Re-examination of the Reliability of UNIX Utilities and Services. Technical Report CS-TR-1995-1268, University of Wisconsin, Madison (1995)"},{"key":"6_CR37","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1145\/1134285.1134307","volume-title":"ICSE","author":"G. Misherghi","year":"2006","unstructured":"Misherghi, G., Su, Z.: HDD: Hierarchical Delta Debugging. In: ICSE, pp. 142\u2013151. ACM, New York (2006)"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and Certifying QBFs: A Comparison of State-of-the-Art Tools. AI Commun.\u00a022 (2009)","DOI":"10.3233\/AIC-2009-0468"},{"key":"6_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-30201-8_34","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G. Pan","year":"2004","unstructured":"Pan, G., Vardi, M.: Symbolic Decision Procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 453\u2013467. Springer, Heidelberg (2004)"},{"key":"6_CR40","unstructured":"Pennock, D., Stout, Q.: Exploiting a Theory of Phase Transitions in Three-Satisfiability Problems. In: AAAI\/IAAI, vol.\u00a01 (1996)"},{"key":"6_CR41","unstructured":"Pipatsrisawat, K., Darwiche, A.: RSat 2.0: SAT Solver Description. Technical Report D\u2013153, Automated Reasoning Group, CSD, UCLA (2007)"},{"key":"6_CR42","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa (2006)"},{"key":"6_CR43","unstructured":"Samulowitz, H.: MiniQBF Solver (2010), http:\/\/miniqbf.spaces.live.com\/"},{"key":"6_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/11564751_43","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"H. Samulowitz","year":"2005","unstructured":"Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 578\u2013592. Springer, Heidelberg (2005)"},{"key":"6_CR45","volume-title":"Fuzzing - Brute Force Vulnerability Discovery","author":"M. Sutton","year":"2007","unstructured":"Sutton, M., Greene, A., Amini, P.: Fuzzing - Brute Force Vulnerability Discovery. Pearson Ed., London (2007)"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Takanen, A., Demott, J., Miller, C.: Fuzzing for Software Security Testing and Quality Assurance. Artech House (2008)","DOI":"10.1016\/S1353-4858(08)70095-3"},{"key":"6_CR47","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the Complexity of Proofs in Propositional Logics. Automation of Reasoning: Classical Papers in Computational Logic 1967-1970\u00a02 (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"6_CR48","unstructured":"Xu, K., Boussemart, F., Hemery, F., Lecoutre, C.: A Simple Model to Generate Hard Satisfiable Instances. CoRR, abs\/cs\/0509032 (2005)"},{"key":"6_CR49","doi-asserted-by":"crossref","unstructured":"Yu, Y., Malik, S.: Validating the Result of a Quantified Boolean Formula (QBF) Solver: Theory and Practice. In: Asia and South Pacific DAC (2005)","DOI":"10.1145\/1120725.1120821"},{"key":"6_CR50","volume-title":"Why Programs Fail. A Guide to Systematic Debugging","author":"A. Zeller","year":"2005","unstructured":"Zeller, A.: Why Programs Fail. A Guide to Systematic Debugging. Morgan Kaufmann, San Francisco (2005)"},{"issue":"2","key":"6_CR51","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A. Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and Isolating Failure-Inducing Input. IEEE Transactions on Software Engineering\u00a028(2), 183\u2013200 (2002)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR52","unstructured":"Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: DATE 2003 (2003)"},{"key":"6_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, p. 200. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14186-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T03:39:21Z","timestamp":1635651561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14186-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141850","9783642141867"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14186-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}