{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T10:34:37Z","timestamp":1725878077968},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_24","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"442-461","source":"Crossref","is-referenced-by-count":1,"title":["Conjunctive Abstract Interpretation Using Paramodulation"],"prefix":"10.1007","author":[{"given":"Or","family":"Ozeri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"24_CR1","volume-title":"Compilers: Principles, Techniques and Tools","author":"AV Aho","year":"1988","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1988)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). doi: 10.1007\/11804192_17"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-662-48288-9_15","volume-title":"Static Analysis","author":"G Castelnuovo","year":"2015","unstructured":"Castelnuovo, G., Naik, M., Rinetzky, N., Sagiv, M., Yang, H.: Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 252\u2013274. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48288-9_15"},{"issue":"3","key":"24_CR4","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0743-1066(95)00064-X","volume":"25","author":"M Codish","year":"1995","unstructured":"Codish, M., Demoen, B.: Analyzing logic programs using \"PROP\"-ositional logic programs and a magic wand. J. Log. Program. 25(3), 249\u2013274 (1995)","journal-title":"J. Log. Program."},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixed points. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 269\u2013282. ACM Press, New York (1979)","DOI":"10.1145\/567752.567778"},{"key":"24_CR7","unstructured":"del Val, A.: A new method for consequence finding and compilation in restricted languages. In: Hendler, J., Subramanian, D. (eds.) Proceedings of 16th National Conference on Artificial Intelligence and 11th Conference on Innovative Applications of Artificial Intelligence, 18\u201322 July 1999, Orlando, Florida, USA, pp. 259\u2013264. AAAI Press\/The MIT Press (1999)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006). doi: 10.1007\/11691372_19"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014221","volume-title":"Languages and Compilers for Parallel Computing","author":"R Ghiya","year":"1996","unstructured":"Ghiya, R., Hendren, L.J.: Connection analysis: a practical interprocedural heap analysis for C. In: Huang, C.-H., Sadayappan, P., Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1995. LNCS, vol. 1033, pp. 515\u2013533. Springer, Heidelberg (1996). doi: 10.1007\/BFb0014221"},{"issue":"1\u20132","key":"24_CR10","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/S0304-3975(98)00194-7","volume":"216","author":"R Giacobazzi","year":"1999","unstructured":"Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theoret. Comput. Sci. 216(1\u20132), 159\u2013211 (1999)","journal-title":"Theoret. Comput. Sci."},{"issue":"5","key":"24_CR11","doi-asserted-by":"crossref","first-page":"1067","DOI":"10.1145\/293677.293680","volume":"20","author":"R Giacobazzi","year":"1998","unstructured":"Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst. 20(5), 1067\u20131109 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"24_CR12","unstructured":"Inoue, K.: Consequence-finding based on ordered linear resolution. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of 12th International Joint Conference on Artificial Intelligence, 24\u201330 August 1991, Sydney, Australia, pp. 158\u2013164. Morgan Kaufmann (1991)"},{"issue":"1\u20134","key":"24_CR13","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/176454.176519","volume":"2","author":"K Marriott","year":"1993","unstructured":"Marriott, K., S\u00f8ndergaard, H.: Precise and efficient groundness analysis for logic programs. LOPLAS 2(1\u20134), 181\u2013196 (1993)","journal-title":"LOPLAS"},{"issue":"2","key":"24_CR14","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"volume-title":"Handbook of Automated Reasoning","year":"2001","key":"24_CR15","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 1. Elsevier Science Publishers B. V., Amsterdam (2001)"},{"issue":"1","key":"24_CR16","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"1\u20132","key":"24_CR17","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0304-3975(00)00316-9","volume":"277","author":"F Scozzari","year":"2002","unstructured":"Scozzari, F.: Logical optimality of groundness analysis. Theoret. Comput. Sci. 277(1\u20132), 149\u2013184 (2002)","journal-title":"Theoret. Comput. Sci."},{"key":"24_CR18","unstructured":"Simon, L., del Val, A.: Efficient consequence finding. In: Nebel, B. (ed.) Proceedings of 17th International Joint Conference on Artificial Intelligence, IJCAI 2001, 4\u201310 August 2001, Seattle, Washington, USA, pp. 359\u2013370. Morgan Kaufmann (2001)"},{"issue":"1","key":"24_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1561\/2500000014","volume":"2","author":"Y Smaragdakis","year":"2015","unstructured":"Smaragdakis, Y., Balatsouras, G.: Pointer analysis. Found. Trends Program. Lang. 2(1), 1\u201369 (2015)","journal-title":"Found. Trends Program. Lang."},{"key":"24_CR20","unstructured":"US-CERT\/NIST: Vulnerability summary for cve-2014-7841, April 2014. https:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2014-7841"}],"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-319-52234-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T03:53:56Z","timestamp":1498362836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}