{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:10:50Z","timestamp":1763467850216},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_23","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"326-341","source":"Crossref","is-referenced-by-count":55,"title":["Finding Minimal Unsatisfiable Cores of Declarative Specifications"],"prefix":"10.1007","author":[{"given":"Emina","family":"Torlak","sequence":"first","affiliation":[]},{"given":"Felix Sheng-Ho","family":"Chang","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Jackson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","first-page":"528","volume":"2031","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. LCNS\u00a02031, 528 (2001)","journal-title":"LCNS"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. In: Conference on Correct Hardware Design and Verification Methods, pp. 82\u201396 (1999)","DOI":"10.1007\/3-540-48153-2_8"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: ASE 2003 (2003)","DOI":"10.1109\/ASE.2003.1240298"},{"key":"23_CR4","unstructured":"Shlyakhter, I.: Declarative Symbolic Pure Logic Model Checking. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA (2005)"},{"key":"23_CR5","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":"23_CR6","unstructured":"Chang, F.: Alloy analyzer 4.0 (2007), http:\/\/alloy.mit.edu\/alloy4\/"},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"23_CR8","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. 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":"23_CR9","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT solver. In: DATE 2002, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Mahajan, Y.S., Fu, Z., Malik, S.: zchaff2004: An efficient SAT solver. In: SAT (Selected Papers), pp. 360\u2013375 (2004)","DOI":"10.1007\/11527695_27"},{"key":"23_CR11","unstructured":"Kalman, J.A.: Automated Reasoning with Otter. Rinton Press (2001)"},{"key":"23_CR12","unstructured":"Riazanov, A.: Implementing an Efficient Theorem Prover. PhD Thesis, The University of Manchester, Manchester (2003)"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Handbook of automated reasoning, pp. 1965\u20132013 (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"23_CR14","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":"23_CR15","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: CADE-19 Workshop on Model Computation, Miami, FL (2003)"},{"key":"23_CR16","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. In: Journal of Applied Logic (2007)"},{"issue":"2","key":"23_CR17","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"23_CR18","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J.W. Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. ORSA Journal of Computing\u00a03(2), 157\u2013158 (1991)","journal-title":"ORSA Journal of Computing"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE 2003 (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/11499107_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.H. Liffiton","year":"2005","unstructured":"Liffiton, M.H., Sakallah, K.A.: On Finding All Minimally Unsatisfiable Subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 173\u2013186. Springer, Heidelberg (2005)"},{"key":"23_CR22","unstructured":"Lynce, I.: On computing minimum unsatisfiable cores. In: SAT 2004 (2004)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/11499107_40","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Mneimneh","year":"2005","unstructured":"Mneimneh, M., Lynce, I., Andraus, Z.: A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 467\u2013474. Springer, Heidelberg (2005)"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Oh, Y., Mneimneh, M., Andraus, Z., Sakallah, K., Markov, I.: Amuse: A minimally-unsatisfiable subformula extractor. In: DAC, ACM\/IEEE, pp. 518\u2013523 (2004)","DOI":"10.1145\/996566.996710"},{"key":"23_CR25","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formula. In: SAT 2003 (2003)"},{"key":"23_CR26","unstructured":"Gr\u00e9goire, E., Mazure, B., Piette, C.: Extracting MUSes. In: ECAI 2006, Trento, Italy, pp. 387\u2013391 (2006)"},{"issue":"3","key":"23_CR27","first-page":"324","volume":"12","author":"E. Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire, E., Mazure, B., Piette, C.: Local-search extraction of MUSes. Constraints Journal\u00a012(3), 324\u2013344 (2007)","journal-title":"Constraints Journal"},{"key":"23_CR28","unstructured":"Gr\u00e9goire, E., Mazure, B., Piette, C.: Boosting a complete technique to find MSS and MUS thanks to a local search oracle. In: IJCAI 2007, Hyderabad, India, vol.\u00a02, pp. 2300\u20132305 (2007)"},{"key":"23_CR29","volume-title":"ISSTA 2006","author":"G. Dennis","year":"2006","unstructured":"Dennis, G., Chang, F., Jackson, D.: Modular verification of code. In: ISSTA 2006, Portland, Maine (2006)"},{"key":"23_CR30","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1145\/1287624.1287653","volume-title":"ESEC-FSE 2007","author":"J. Dolby","year":"2007","unstructured":"Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a sat solver. In: ESEC-FSE 2007, pp. 195\u2013204. ACM, New York (2007)"},{"key":"23_CR31","unstructured":"Taghdiri, M.: Automating Modular Program Verification by Refining Specifications. PhD thesis, Massachusetts Institute of Technology (2007)"},{"key":"23_CR32","unstructured":"Yeung, V.: Declarative configuration applied to course scheduling. Master\u2019s thesis, Massachusetts Institute of Technology, Cambridge (2006)"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:43:39Z","timestamp":1620017019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_23","relation":{},"subject":[]}}