{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T06:48:44Z","timestamp":1791269324206,"version":"4.1.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319109350","type":"print"},{"value":"9783319109367","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10936-7_9","type":"book-chapter","created":{"date-parts":[[2014,9,6]],"date-time":"2014-09-06T15:17:55Z","timestamp":1410016675000},"page":"134-150","source":"Crossref","is-referenced-by-count":21,"title":["Automatic Analysis of Open Objects in Dynamic Language Programs"],"prefix":"10.1007","author":[{"given":"Arlen","family":"Cox","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"9_CR1","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.\u00a04134, pp. 221\u2013239. Springer, Heidelberg (2006)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-27940-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 1\u201322. Springer, Heidelberg (2012)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2006","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"key":"9_CR4","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":"9_CR5","doi-asserted-by":"crossref","unstructured":"Chugh, R., Herman, D., Jhala, R.: Dependent types for JavaScript. In: OOPSLA, pp. 587\u2013606 (2012)","DOI":"10.1145\/2398857.2384659"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Chugh, R., Rondon, P.M., Jhala, R.: Nested refinements: A logic for duck typing. In: POPL, pp. 231\u2013244 (2012)","DOI":"10.1145\/2103621.2103686"},{"key":"9_CR7","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":"9_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL, pp. 105\u2013118 (2011)","DOI":"10.1145\/1925844.1926399"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-39038-8_17","volume-title":"ECOOP 2013 \u2013 Object-Oriented Programming","author":"A. Cox","year":"2013","unstructured":"Cox, A., Chang, B.-Y.E., Sankaranarayanan, S.: QUIC graphs: Relational invariant generation for containers. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol.\u00a07920, pp. 401\u2013425. Springer, Heidelberg (2013)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Cox, A., Chang, B.-Y.E., Rival, X.: Automatic analysis of open objects in dynamic language programs (extended). Technical report, University of Colorado Boulder (2014)","DOI":"10.1007\/978-3-319-10936-7_9"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I. Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 246\u2013266. Springer, Heidelberg (2010)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: POPL, pp. 187\u2013200 (2011)","DOI":"10.1145\/1925844.1926407"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Gardner, P., Maffeis, S., Smith, G.D.: Towards a program logic for JavaScript. In: POPL, pp. 31\u201344 (2012)","DOI":"10.1145\/2103621.2103663"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: POPL, pp. 338\u2013350 (2005)","DOI":"10.1145\/1047659.1040333"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: PLDI, pp. 339\u2013348 (2008)","DOI":"10.1145\/1379022.1375623"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-642-54013-4_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Hardekopf","year":"2014","unstructured":"Hardekopf, B., Wiedermann, B., Churchill, B., Kashyap, V.: Widening for control-flow. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol.\u00a08318, pp. 472\u2013491. Springer, Heidelberg (2014)"},{"issue":"10","key":"9_CR20","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-03237-0_17","volume-title":"Static Analysis","author":"S.H. Jensen","year":"2009","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 238\u2013255. Springer, Heidelberg (2009)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-642-15769-1_20","volume-title":"Static Analysis","author":"S.H. Jensen","year":"2010","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Interprocedural analysis with lazy propagation. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 320\u2013339. Springer, Heidelberg (2010)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Kashyap, V., Sarracino, J., Wagner, J., Wiedermann, B., Hardekopf, B.: Type refinement for static analysis of JavaScript. In: DLS, pp. 17\u201326 (2013)","DOI":"10.1145\/2508168.2508175"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"9_CR26","unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)"},{"key":"9_CR27","unstructured":"Parkinson, M.J.: Local reasoning for Java. PhD thesis, University of Cambridge (2005)"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"656","DOI":"10.1007\/978-3-642-22110-1_53","volume-title":"Computer Aided Verification","author":"T.-H. Pham","year":"2011","unstructured":"Pham, T.-H., Trinh, M.-T., Truong, A.-H., Chin, W.-N.: Fixbag: A fixpoint calculator for quantified bag constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 656\u2013662. Springer, Heidelberg (2011)"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Richards, G., Lebresne, S., Burg, B., Vitek, J.: An analysis of the dynamic behavior of JavaScript programs. In: PLDI, pp. 1\u201312 (2010)","DOI":"10.1145\/1809028.1806598"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-31057-7_20","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"M. Sridharan","year":"2012","unstructured":"Sridharan, M., Dolby, J., Chandra, S., Sch\u00e4fer, M., Tip, F.: Correlation tracking for points-to analysis of JavaScript. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol.\u00a07313, pp. 435\u2013458. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10936-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T14:18:17Z","timestamp":1746368297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10936-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319109350","9783319109367"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10936-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}