{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T09:17:46Z","timestamp":1787563066111,"version":"build-2736575974"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540787389","type":"print"},{"value":"9783540787396","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78739-6_16","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T04:39:06Z","timestamp":1207111146000},"page":"193-207","source":"Crossref","is-referenced-by-count":17,"title":["Cover Algorithms and Their Combination"],"prefix":"10.1007","author":[{"given":"Sumit","family":"Gulwani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Madan","family":"Musuvathi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: 29th Annual Symposium on POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"issue":"6","key":"16_CR3","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. Transactions on Software Engg.\u00a030(6), 388\u2013402 (2004)","journal-title":"Transactions on Software Engg."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: 5th ACM Symposium on POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Gulavani","year":"2006","unstructured":"Gulavani, B., Rajamani, S.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, Springer, Heidelberg (2006)"},{"key":"16_CR7","unstructured":"Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. Technical Report MSR-TR-2006-09, Microsoft Research (January 2006)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Necula, G.C.: Global value numbering using random interpretation. In: 31st Annual ACM Symposium on POPL (January 2004)","DOI":"10.1145\/964001.964030"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-540-27864-1_17","volume-title":"Static Analysis","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 212\u2013227. Springer, Heidelberg (2004)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI, pp. 376\u2013386 (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: 31st Annual ACM Symposium on POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"issue":"6","key":"16_CR12","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1093\/logcom\/2.6.719","volume":"2","author":"A.C. Kakas","year":"1992","unstructured":"Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive logic programming. Journal of Logic and Computation\u00a02(6), 719\u2013770 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/11513988_5","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2005","unstructured":"Lahiri, S.K., Ball, T., Cook, B.: Predicate Abstraction via Symbolic Decision Procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 24\u201338. Springer, Heidelberg (2005)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Symbolic model checking: an approach to the state explosion problem. PhD thesis, Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. McMillan","year":"2004","unstructured":"McMillan, K.: An Interpolating Theorem Prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"issue":"2","key":"16_CR16","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Paul, G.: Ai approaches to abduction, 35\u201398 (2000)","DOI":"10.1007\/978-94-017-1733-5_2"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78739-6_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:20:47Z","timestamp":1619508047000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78739-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787389","9783540787396"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78739-6_16","relation":{},"subject":[]}}