{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:23Z","timestamp":1725573083224},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_20","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T11:45:34Z","timestamp":1292845534000},"page":"298-312","source":"Crossref","is-referenced-by-count":9,"title":["Minimizing Counterexample with Unit Core Extraction and Incremental SAT"],"prefix":"10.1007","author":[{"given":"ShengYu","family":"Shen","sequence":"first","affiliation":[]},{"given":"Ying","family":"Qin","sequence":"additional","affiliation":[]},{"given":"SiKun","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2002","unstructured":"Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstractionrefinement using ILP and machine learning. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 265\u2013279. Springer, Heidelberg (2002)"},{"key":"20_CR2","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: Using SAT based Image Computation for Reachability Analysis. technology report CMU-CS-03-151, School of Computer Science, Carnegie Mellon University (September 2003)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Kang, H.-J., Park, I.-C.: SAT-Based Unbounded Symbolic Model Checking. In: Proceeding of DAC 2003, Anaheim, California, USA, June 2-6 (2003)","DOI":"10.1145\/775832.776043"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal Assignments for Bounded Model Checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/3-540-46002-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2002","unstructured":"Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 445\u2013458. Springer, Heidelberg (2002)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic Model Checking using SAT procedures instead of BDDs. In: Proceedings of the 36th Conference on Design Automation (DAC 1999), pp. 317\u2013320 (1999)","DOI":"10.1145\/309847.309942"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: ICCAD (2001)","DOI":"10.1145\/774572.774637"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, Las Vegas, NV, pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"20_CR11","unstructured":"http:\/\/www.cbl.ncsu.edu\/CBL_Docs\/iscas89.html"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Een, N., Sorensson, N.: Temporal Induction by Incremental SAT Solving. In: Proc. of the First International Workshop on Bounded Model Checking (2003)","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in spin. In: SPIN Workshop on Model Checking of Software, pp. 92\u2013108 (2004)","DOI":"10.1007\/978-3-540-24732-6_7"},{"key":"20_CR14","unstructured":"Groce, A., Kroening, D.: Making the Most of BMC Counterexamples. In: The second international workshop on Bounded Model Checking, BMC 2004 (2004) (to appear)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-36577-X_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Glusman","year":"2003","unstructured":"Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 176\u2013191. Springer, Heidelberg (2003)"},{"key":"20_CR16","unstructured":"Zhang, L., Malik, S.: Validating sat solvers using an independent resolutionbased checker: Practical implementations and other applications. In: Proceedings of Design Automation and Test in Europe, DATE 2003 (2003)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for cnf formulas. In: Proceedings of Design Automation and Test in Europe, DATE 2003 (2003)","DOI":"10.1109\/DATE.2003.1253718"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:24:16Z","timestamp":1605741856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}