{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T14:48:21Z","timestamp":1725547701217},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642118104"},{"type":"electronic","value":"9783642118111"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11811-1_13","type":"book-chapter","created":{"date-parts":[[2010,2,19]],"date-time":"2010-02-19T11:57:22Z","timestamp":1266580642000},"page":"160-173","source":"Crossref","is-referenced-by-count":7,"title":["Alloy+HotCore: A Fast Approximation to Unsat Core"],"prefix":"10.1007","author":[{"given":"Nicol\u00e1s","family":"D\u2019Ippolito","sequence":"first","affiliation":[]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[]},{"given":"Juan P.","family":"Galeotti","sequence":"additional","affiliation":[]},{"given":"Esteban","family":"Lanzarotti","sequence":"additional","affiliation":[]},{"given":"Sergio","family":"Mera","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Software abstractions: logic, language, and analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software abstractions: logic, language, and analysis. MIT Press, Cambridge (2006)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-68237-0_23","volume-title":"FM 2008: Formal Methods","author":"E. Torlak","year":"2008","unstructured":"Torlak, E., Chang, F., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 326\u2013341. Springer, Heidelberg (2008)"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/800157.805047","volume-title":"STOC 1971","author":"S.A. Cook","year":"1971","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: STOC 1971, pp. 151\u2013158. ACM, New York (1971)"},{"issue":"2","key":"13_CR5","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-007-9074-1","volume":"39","author":"C. Sinz","year":"2007","unstructured":"Sinz, C.: Visualizing sat instances and runs of the dpll algorithm. Journal of Automated Reasoning\u00a039(2), 219\u2013243 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR6","unstructured":"Selman, B., Levesque, H., Mitchell, D.: A new method for solving hard satisfiability problems. In: Procs. of the 10th Conf. on Artificial Intelligence, pp. 440\u2013446 (1992)"},{"key":"13_CR7","unstructured":"Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. DIMACS Series in Discrete Mathematics and Theoretical Computer Science (1993)"},{"key":"13_CR8","unstructured":"Mazure, B., Sa\u00efs, L., Gr\u00e9goire, \u00c9.: A powerful heuristic to locate inconsistent kernels in knowledge-based systems. In: IPMU 1996, pp. 1265\u20131269 (1996)"},{"key":"13_CR9","unstructured":"Gr\u00e9goire, E., Mazure, B., Piette, C.: Boosting a complete technique to find mss and mus thanks to a local search oracle. In: Proceedings of IJCAI, pp. 2300\u20132305 (2007)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.M. Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013515. Springer, Heidelberg (2004)"},{"key":"13_CR11","unstructured":"Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating the small scope hypothesis (2002), http:\/\/sdg.csail.mit.edu\/pubs\/2002\/SSH.pdf"},{"issue":"7","key":"13_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"13_CR13","first-page":"220","volume-title":"1996 IEEE\/ACM international conference on Computer-aided design","author":"J.P.M. Silva","year":"1997","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP \u2013 A new search algorithm for satisfiability. In: 1996 IEEE\/ACM international conference on Computer-aided design, pp. 220\u2013227. IEEE Computer Society, Washington (1997)"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"13_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-48159-1_5","volume-title":"Progress in Artificial Intelligence","author":"J. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol.\u00a01695, pp. 62\u201374. Springer, Heidelberg (1999)"},{"issue":"12","key":"13_CR16","doi-asserted-by":"publisher","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E. Goldberg","year":"2007","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. Discrete Applied Mathematics\u00a0155(12), 1549\u20131561 (2007)","journal-title":"Discrete Applied Mathematics"},{"key":"13_CR17","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In: Proceedings of SAT, vol. 3 (2003)"},{"key":"13_CR18","first-page":"162","volume":"9","author":"R. Bruni","year":"2001","unstructured":"Bruni, R., Sassano, A.: Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. ENDM\u00a09, 162\u2013173 (2001)","journal-title":"ENDM"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"13_CR20","unstructured":"Galeotti, J.: Distributed sat-based analysis of object oriented code. In: Proceedings of Symposium on Automatic Program Verification (APV 2009), Rio Cuarto, Argentina, ETH Zurich (February 2009)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11811-1_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:44:13Z","timestamp":1606185853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11811-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642118104","9783642118111"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11811-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}