{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:06:38Z","timestamp":1746158798050,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_16","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"282-301","source":"Crossref","is-referenced-by-count":7,"title":["Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java"],"prefix":"10.1007","author":[{"given":"Zhoulai","family":"Fu","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Technical Report 457, Dipartimento di Matematica, Universit\u00e0 di Parma, Italy (2006)"},{"issue":"1-2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0167-6423(97)00009-9","volume":"30","author":"R. Bagnara","year":"1998","unstructured":"Bagnara, R.: A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Sci. Comput. Program.\u00a030(1-2), 119\u2013155 (1998)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"16_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1921532.1921553","volume":"36","author":"J. Bertrane","year":"2011","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis by abstract interpretation of embedded critical software. ACM SIGSOFT Software Engineering Notes\u00a036(1), 1\u20138 (2011)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Blackburn, S.M., Garner, R., Hoffman, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M., Lee, H., Moss, J.E.B., Phansalkar, A., Stefanovi\u0107, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA 2006: Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications, pp. 169\u2013190. ACM Press, New York (2006)","DOI":"10.1145\/1167473.1167488"},{"issue":"6","key":"16_CR5","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C. Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM\u00a058(6), 26 (2011)","journal-title":"J. ACM"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247\u2013260 (2008)","DOI":"10.1145\/1328897.1328469"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B.-Y.E. Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 384\u2013401. Springer, Heidelberg (2007)"},{"issue":"1-3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S0167-6423(99)00045-3","volume":"38","author":"A. Cortesi","year":"2000","unstructured":"Cortesi, A., Le Charlier, B., Van Hentenryck, P.: Combinations of abstract domains for logic programming: open product and generic pattern construction. Sci. Comput. Program.\u00a038(1-3), 27\u201371 (2000)","journal-title":"Sci. Comput. Program."},{"key":"16_CR9","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, pp. 106\u2013130, Dunod, Paris (1976)"},{"issue":"4","key":"16_CR10","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"16_CR11","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, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-19805-2_31","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: The reduced product of abstract domains and the combination of decision procedures. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 456\u2013472. Springer, Heidelberg (2011)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Deutsch, A.: A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations. In: ICCL, pp. 2\u201313 (1992)","DOI":"10.1109\/ICCL.1992.185463"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Emami, M., Ghiya, R., Hendren, L.J.: Context-sensitive interprocedural points-to analysis in the presence of function pointers. In: PLDI, pp. 242\u2013256 (1994)","DOI":"10.1145\/773473.178264"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M. F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 10\u201330. Springer, Heidelberg (2011)"},{"key":"16_CR17","unstructured":"Fu, Z.: Static Analysis of Numerical Properties in the Presence of Pointers. PhD thesis, Universit\u00e9 de Rennes 1 \u2013 INRIA, France (2013)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-24730-2_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Gopan","year":"2004","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 512\u2013529. Springer, Heidelberg (2004)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013302. Springer, Heidelberg (2000)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-36579-6_12","volume-title":"Compiler Construction","author":"O. Lhot\u00e1k","year":"2003","unstructured":"Lhot\u00e1k, O., Hendren, L.: Scaling java points-to analysis using SPARK. In: Hedin, G. (ed.) CC 2003. LNCS, vol.\u00a02622, pp. 153\u2013169. Springer, Heidelberg (2003)"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15769-1_6","volume-title":"Static Analysis","author":"B. McCloskey","year":"2010","unstructured":"McCloskey, B., Reps, T., Sagiv, M.: Statically inferring complex heap, array, and numeric invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 71\u201399. Springer, Heidelberg (2010)"},{"key":"16_CR22","unstructured":"Min\u00e9, A.: Weakly Relational Numerical Abstract Domains. PhD thesis, \u00c9cole Polytechnique, Palaiseau, France (December 2004)"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded c programs with union types and pointer arithmetics. In: LCTES, pp. 54\u201363 (2006)","DOI":"10.1145\/1159974.1134659"},{"issue":"1","key":"16_CR24","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation\u00a019(1), 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"16_CR25","unstructured":"Pioli, A., Hind, M.: Combining interprocedural pointer analysis and conditional constant propagation. Technical report, IBM T. J. Watson Research Center (1999)"},{"key":"16_CR26","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/292540.292552","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999","author":"M. Sagiv","year":"1999","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999, pp. 105\u2013118. ACM, New York (1999)"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Simon, A.: Value-Range Analysis of C Programs. Springer (August 2008)","DOI":"10.1007\/978-1-84800-017-9"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-35873-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Toubhans","year":"2013","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced product combination of abstract domains for shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 375\u2013395. Springer, Heidelberg (2013)"},{"key":"16_CR29","unstructured":"Vall\u00e9e-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a java bytecode optimization framework. In: Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, CASCON 1999, p. 13. IBM Press (1999)"},{"key":"16_CR30","unstructured":"Vallee-Rai, R., Hendren, L.J.: Jimple: Simplifying java bytecode for analyses and transformations. Technical report, Sable Research Group, McGill University (July 1998)"},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-540-69149-5_24","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A. Venet","year":"2008","unstructured":"Venet, A.: Towards the integration of symbolic and numerical static analysis. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 227\u2013236. Springer, Heidelberg (2008)"},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"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-642-54013-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T10:40:07Z","timestamp":1746096007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}