{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T04:07:19Z","timestamp":1768968439153,"version":"3.49.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_23","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"653-682","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Evaluating Design Tradeoffs in Numeric Static Analysis for Java"],"prefix":"10.1007","author":[{"given":"Shiyi","family":"Wei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Mardziel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Ruef","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"23_CR1","unstructured":"Facebook Infer. http:\/\/fbinfer.com . Accessed 11 Nov 2016"},{"key":"23_CR2","unstructured":"Watson, T.J.: Libraries for Analysis (WALA). http:\/\/wala.sourceforge.net\/ , version 1.3"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Arcuri, A., Briand, L.: A practical guide for using statistical tests to assess randomized algorithms in software engineering. In: ICSE (2011)","DOI":"10.1145\/1985793.1985795"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337\u2013354. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_19"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11823230_15","volume-title":"Static Analysis","author":"G Balakrishnan","year":"2006","unstructured":"Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221\u2013239. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_15"},{"key":"23_CR6","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)","DOI":"10.1145\/1167473.1167488"},{"issue":"5","key":"23_CR7","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/780822.781153","volume":"38","author":"Bruno Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)","journal-title":"ACM SIGPLAN Notices"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Bortz, A., Boneh, D.: Exposing private information by timing web applications. In: WWW (2007)","DOI":"10.1145\/1242572.1242656"},{"issue":"10","key":"23_CR9","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1145\/1639949.1640108","volume":"44","author":"Martin Bravenboer","year":"2009","unstructured":"Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: OOPSLA (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"23_CR10","unstructured":"Brodkin, J.: Huge portions of the web vulnerable to hashing denial-of-service attack (2011). http:\/\/arstechnica.com\/business\/2011\/12\/huge-portions-of-web-vulnerable-to-hashing-denial-of-service-attack\/"},{"key":"23_CR11","unstructured":"Brumley, D., Boneh, D.: Remote timing attacks are practical. In: USENIX Security (2003)"},{"issue":"1","key":"23_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/s00265-010-1029-6","volume":"65","author":"Kenneth P. Burnham","year":"2010","unstructured":"Burnham, K.P., Anderson, D.R., Huyvaert, K.P.: AIC model selection and multimodel inference in behavioral ecology: some background, observations, and comparisons. Behav. Ecol. Sociobiol. 65(1), 23\u201325 (2011)","journal-title":"Behavioral Ecology and Sociobiology"},{"issue":"6","key":"23_CR13","doi-asserted-by":"publisher","first-page":"1","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 58(6), 1\u201366 (2011)","journal-title":"J. ACM"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Chang, B.Y.E., Rival, X.: Relational inductive shape analysis. In: POPL (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Chang, B.Y.E., Rival, X.: Modular construction of shape-numeric analyzers. In: Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (SAIRP) (2013)","DOI":"10.4204\/EPTCS.129.11"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-662-46081-8_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Christakis","year":"2015","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: An experimental evaluation of deliberate unsoundness in a static program analyzer. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 336\u2013354. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_19"},{"key":"23_CR17","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming (1976)"},{"key":"23_CR18","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":"23_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978)","DOI":"10.1145\/512760.512770"},{"issue":"4","key":"23_CR20","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR21","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/978-3-642-31057-7_29","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"Arnab De","year":"2012","unstructured":"De, A., D\u2019Souza, D.: Scalable flow-sensitive pointer analysis for java with strong updates. In: ECOOP (2012)"},{"key":"23_CR22","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. 6528, pp. 10\u201330. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18070-5_2"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-642-54013-4_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Ferrara","year":"2014","unstructured":"Ferrara, P.: Generic combination of heap and value analyses in abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 302\u2013321. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_17"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-662-46081-8_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Ferrara","year":"2015","unstructured":"Ferrara, P., M\u00fculler, P., Novacek, M.: Automatic inference of heap properties exploiting value domains. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 393\u2013411. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_22"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-54013-4_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z Fu","year":"2014","unstructured":"Fu, Z.: Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for java. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 282\u2013301. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_16"},{"key":"23_CR26","unstructured":"Goodin, D.: Long passwords are good, but too much length can be a dos hazard (2013). http:\/\/arstechnica.com\/security\/2013\/09\/long-passwords-are-good-but-too-much-length-can-be-bad-for-security\/"},{"key":"23_CR27","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. 2988, pp. 512\u2013529. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_38"},{"issue":"6","key":"23_CR28","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1145\/1543135.1542518","volume":"44","author":"Sumit Gulwani","year":"2009","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"23_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-71316-6_18","volume-title":"Programming Languages and Systems","author":"S Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 253\u2013267. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_18"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI (2010)","DOI":"10.1145\/1806596.1806630"},{"key":"23_CR31","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2012.11.003","volume":"289","author":"J Henry","year":"2012","unstructured":"Henry, J., Monniaux, D., Moy, M.: Pagai: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15\u201325 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: PASTE (2001)","DOI":"10.1145\/379605.379665"},{"key":"23_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"key":"23_CR34","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. 1824, pp. 280\u2013301. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-540-45099-3_15"},{"issue":"1","key":"23_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1391984.1391987","volume":"18","author":"O Lhot\u00e1k","year":"2008","unstructured":"Lhot\u00e1k, O., Hendren, L.: Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation. ACM Trans. Softw. Eng. Methodol. (TOSEM) 18(1), 1\u201353 (2008)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"23_CR36","doi-asserted-by":"crossref","unstructured":"Logozzo, F., F\u00e4hndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: SAC (2008)","DOI":"10.1145\/1363686.1363736"},{"key":"23_CR37","doi-asserted-by":"crossref","unstructured":"Magill, S.: Instrumentation analysis: an automated method for producing numeric abstractions of heap-manipulating programs. Ph.D. thesis, School of Computer Science, Carnegie Mellon University (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"23_CR38","unstructured":"Mardziel, P., Magill, S., Hicks, M., Srivatsa, M.: Dynamic enforcement of knowledge-based security policies using probabilistic abstract interpretation. J. Comput. Secur. 21(4), 463\u2013532 (2013)"},{"key":"23_CR39","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. 6337, pp. 71\u201399. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_6"},{"issue":"1","key":"23_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1044834.1044835","volume":"14","author":"A Milanova","year":"2005","unstructured":"Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for java. ACM Trans. Softw. Eng. Methodol. (TOSEM) 14(1), 1\u201314 (2005)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"23_CR41","unstructured":"Min\u00e9, A.: APRON numerical abstract domain library. http:\/\/apron.cri.ensmp.fr\/library\/"},{"key":"23_CR42","doi-asserted-by":"crossref","unstructured":"Oh, H., Heo, K., Lee, W., Lee, W., Yi, K.: Design and implementation of sparse global analyses for c-like languages. In: PLDI (2012)","DOI":"10.1145\/2254064.2254092"},{"key":"23_CR43","unstructured":"Pioli, A., Hind, M.: Combining interprocedural pointer analysis and conditional constant propagation. Technical report, IBM T. J. Watson Research Center (1999)"},{"key":"23_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-36579-6_10","volume-title":"Compiler Construction","author":"BG Ryder","year":"2003","unstructured":"Ryder, B.G.: Dimensions of precision in reference analysis of object-oriented programming languages. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 126\u2013137. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36579-6_10"},{"key":"23_CR45","unstructured":"Seltman, H.: Experimental design and analysis (2015). http:\/\/www.stat.cmu.edu\/~hseltman\/309\/Book\/Book.pdf . e-book"},{"key":"23_CR46","unstructured":"Shivers, O.: Control-flow analysis of higher-order languages or taming lambda. Ph.D. thesis, School of Computer Science, Carnegie Mellon University (1991)"},{"key":"23_CR47","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.: ETH Library for Numerical Analysis. http:\/\/elina.ethz.ch and https:\/\/github.com\/eth-srl\/ELINA"},{"key":"23_CR48","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: POPL (2017)","DOI":"10.1145\/3009837.3009885"},{"issue":"1","key":"23_CR49","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1925844.1926390","volume":"46","author":"Yannis Smaragdakis","year":"2011","unstructured":"Smaragdakis, Y., Bravenboer, M., Lhot\u00e1k, O.: Pick your contexts well: understanding object-sensitivity. In: POPL (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"23_CR50","unstructured":"Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: NDSS (2000)"},{"key":"23_CR51","unstructured":"Wei, S., Mardziel, P., Ruef, A., Foster, J.S., Hicks, M.: Evaluating design tradeoffs in numeric static analysis for java (extended version). Technical report (2018). http:\/\/www.cs.umd.edu\/~mwh\/papers\/jana-extended.pdf"},{"key":"23_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-662-44202-9_1","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"S Wei","year":"2014","unstructured":"Wei, S., Ryder, B.G.: State-sensitive points-to analysis for the dynamic behavior of javascript objects. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 1\u201326. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_1"},{"issue":"10","key":"23_CR53","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1145\/320385.320400","volume":"34","author":"John Whaley","year":"1999","unstructured":"Whaley, J., Rinard, M.: Compositional pointer and escape analysis for java programs. In: OOPSLA (1999)","journal-title":"ACM SIGPLAN Notices"},{"key":"23_CR54","doi-asserted-by":"crossref","unstructured":"Zhang, X., Mangal, R., Naik, M., Yang, H.: Hybrid top-down and bottom-up interprocedural analysis. In: PLDI (2014)","DOI":"10.1145\/2594291.2594328"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:33:23Z","timestamp":1571157203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}