{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:40:57Z","timestamp":1777347657705,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540242970","type":"print"},{"value":"9783540305798","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_11","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"147-163","source":"Crossref","is-referenced-by-count":36,"title":["Abstract Interpretation with Alien Expressions and Heap Structures"],"prefix":"10.1007","author":[{"given":"Bor-Yuh Evan","family":"Chang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/10721959_5","volume-title":"Automated Deduction - CADE-17","author":"L. Bachmair","year":"2000","unstructured":"Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 64\u201378. Springer, Heidelberg (2000)"},{"issue":"2","key":"11_CR2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L. Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. Journal of Automated Reasoning\u00a031(2), 129\u2013168 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005) (to appear)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Birkhoff, G.: Lattice Theory, volume XXV of Colloquium Publications. American Mathematical Society (1940)","DOI":"10.1090\/coll\/025"},{"key":"11_CR5","unstructured":"Chang, B.-Y.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. Technical Report MSR-TR-2004-115, Microsoft Research (November 2004)"},{"key":"11_CR6","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: Fourth POPL, pp. 238\u2013252 (January 1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Sixth POPL, pp. 269\u2013282 (January 1979)","DOI":"10.1145\/567752.567778"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Fifth POPL, pp. 84\u201396 (January 1978)","DOI":"10.1145\/512760.512770"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-30538-5_26","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Tiwari, A., Necula, G.C.: Join algorithms for the theory of uninterpreted functions. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 311\u2013323. Springer, Heidelberg (2004)"},{"issue":"4","key":"11_CR10","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C.A.R. Hoare","year":"1973","unstructured":"Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica\u00a02(4), 335\u2013355 (1973)","journal-title":"Acta Informatica"},{"key":"11_CR11","unstructured":"Rustan, K., Leino, M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, Available as Technical Report Caltech-CS-TR-95-03 (1995)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: International Symposium on Software Testing and Analysis (ISSTA 2000), pp. 26\u201338 (2000)","DOI":"10.1145\/347324.348031"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-27815-3_27","volume-title":"Algebraic Methodology and Software Technology","author":"F. Logozzo","year":"2004","unstructured":"Logozzo, F.: Separate compositional analysis of class-based object-oriented languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 332\u2013346. Springer, Heidelberg (2004)"},{"key":"11_CR14","first-page":"102","volume-title":"Program Flow Analysis: Theory and Applications, ch. 4","author":"S.S. Muchnick","year":"1981","unstructured":"Muchnick, S.S., Jones, N.D.: Flow analysis and optimization of Lisplike structures. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, ch. 4, pp. 102\u2013131. Prentice-Hall, Englewood Cliffs (1981)"},{"issue":"2","key":"11_CR15","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 Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR16","unstructured":"Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitationsschrift, Technische Universit\u00e4t M\u00fcnchen (1997)"},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"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-540-30579-8_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:13Z","timestamp":1605759853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}