{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:49:08Z","timestamp":1725572948278},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_13","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"109-122","source":"Crossref","is-referenced-by-count":18,"title":["Deriving Small Unsatisfiable Cores with Dominators"],"prefix":"10.1007","author":[{"given":"Roman","family":"Gershman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maya","family":"Koifman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Amla","year":"2003","unstructured":"Amla, N., McMillan, K.: Automatic abstraction without counter examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"issue":"2","key":"13_CR2","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0166-218X(02)00399-2","volume":"130","author":"R. Bruni","year":"2003","unstructured":"Bruni, R.: Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discrete Appl. Math.\u00a0130(2), 85\u2013100 (2003)","journal-title":"Discrete Appl. Math."},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-540-30140-0_60","volume-title":"Algorithms \u2013 ESA 2004","author":"L. Georgiadis","year":"2004","unstructured":"Georgiadis, L., Werneck, R.F., Tarjan, R.E., Triantafyllis, S., August, D.I.: Finding dominators in practice. In: Albers, S., Radzik, T. (eds.) ESA 2004. LNCS, vol.\u00a03221, pp. 677\u2013688. Springer, Heidelberg (2004)"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1145\/1040305.1040316","volume-title":"POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 122\u2013131. ACM Press, New York (2005)"},{"unstructured":"Gupta, A.: Learning Abstractions for Model Checking. PhD thesis, Carnegie Mellon University (to be published, 2006)","key":"13_CR5"},{"doi-asserted-by":"crossref","unstructured":"Huang, J.: Mup: A minimal unsatisfiability prover. In: Proc. of the 10\n                    th\n                   Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 432\u2013437 (2005)","key":"13_CR6","DOI":"10.1145\/1120725.1120907"},{"unstructured":"Koifman, M.: An approach to extracting a small unsatisfiable core. M.sc. thesis, Technion - I.I.T., Israel, Haifa (to be published, 2006)","key":"13_CR7"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"issue":"1","key":"13_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T. Lengauer","year":"1979","unstructured":"Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst.\u00a01(1), 121\u2013141 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"unstructured":"Lynce, I., Marques-Silva, J.: On computing minimum unsatisfiable cores. In: Proceedings of the International Symposium on Theory and Applications of Satisfiability Testing, pp. 305\u2013310 (2004)","key":"13_CR10"},{"doi-asserted-by":"crossref","unstructured":"Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: Amuse: a minimally-unsatisfiable subformula extractor. In: DAC 2004, pp. 518\u2013523 (2004)","key":"13_CR11","DOI":"10.1145\/996566.996710"},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","volume":"37","author":"C.H. Papadimitriou","year":"1988","unstructured":"Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. J. Comput. Syst. Sci.\u00a037(1), 2\u201313 (1988)","journal-title":"J. Comput. Syst. Sci."},{"doi-asserted-by":"crossref","unstructured":"Prosser, R.: Applications of boolean matrices to the analysis of flow diagrams. In: Proceedings of the Eastern Joint Computer Conference, pp. 133\u2013138 (1959)","key":"13_CR13","DOI":"10.1145\/1460299.1460314"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44798-9_4","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Shtrichman","year":"2001","unstructured":"Shtrichman, O.: Prunning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, p. 58. Springer, Heidelberg (2001)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C., Dill, D.: CVC: a cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 500. Springer, Heidelberg (2002)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"L. Zhang","year":"2004","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formula. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:29:59Z","timestamp":1619508599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11817963_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}