{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,19]],"date-time":"2026-09-19T00:49:20Z","timestamp":1789778960651,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466681","type":"print"},{"value":"9783662466698","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46669-8_20","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T18:37:37Z","timestamp":1427913457000},"page":"483-509","source":"Crossref","is-referenced-by-count":5,"title":["Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages"],"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":"20_CR1","doi-asserted-by":"crossref","unstructured":"Bae, S.G., Cho, H., Lim, I., Ryu, S.: SAFE $_{\\mbox{\\scriptsize WAPI}}$ : Web API misuse detector for web applications. In: FSE 2014 (2014)","DOI":"10.1145\/2635868.2635916"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Bodin, M., Chargu\u00e9raud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: POPL, pp. 87\u2013100 (2014)","DOI":"10.1145\/2535838.2535876"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Bor-Yuh\u00a0Evan Chang and K.\u00a0Rustan\u00a0M. Leino. Abstract interpretation with alien expressions and heap structures. In: VMCAI, pp. 147\u2013163 (2005)","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Charlton, N., Horsfall, B., Reus, B.: Crowfoot: A verifier for higher-order store programs. In: VMCAI, pp. 136\u2013151 (2012)","DOI":"10.1007\/978-3-642-27940-9_10"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Chugh, R., Herman, D., Jhala, R.: Dependent types for JavaScript. In: OOPSLA, pp. 587\u2013606 (2012a)","DOI":"10.1145\/2398857.2384659"},{"key":"20_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 (2012b)","DOI":"10.1145\/2103621.2103686"},{"key":"20_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":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-10936-7_9","volume-title":"Static Analysis","author":"A. Cox","year":"2014","unstructured":"Cox, A., Chang, B.-Y.E., Rival, X.: Automatic analysis of open objects in dynamic language programs. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol.\u00a08723, pp. 134\u2013150. Springer, Heidelberg (2014)"},{"key":"20_CR9","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":"20_CR10","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":"20_CR11","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":"20_CR12","unstructured":"Gardner, P., Naudziuniene, D., Smith, G.: JuS: Squeezing the sense out of JavaScript programs. In: JSTools (2013)"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI, pp. 376\u2013386 (2006)","DOI":"10.1145\/1133255.1134026"},{"key":"20_CR14","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":"20_CR15","doi-asserted-by":"crossref","unstructured":"Hardekopf, B., Wiedermann, B., Churchill, B.R., Kashyap, V.: Widening for control-flow. In: VMCAI, pp. 472\u2013491 (2014)","DOI":"10.1007\/978-3-642-54013-4_26"},{"issue":"10","key":"20_CR16","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":"20_CR17","doi-asserted-by":"crossref","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Type analysis for JavaScript. In: SAS, pp. 238\u2013255 (2009)","DOI":"10.1007\/978-3-642-03237-0_17"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Interprocedural analysis with lazy propagation. In: SAS, pp. 320\u2013339 (2010)","DOI":"10.1007\/978-3-642-15769-1_20"},{"key":"20_CR19","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":"20_CR20","unstructured":"Krishnawami, N.R.: Verifying Higher-Order Imperative Programs with HIgher-Order Separation Logic. PhD thesis, Carnegie Mellon University (2011)"},{"key":"20_CR21","unstructured":"Lee, H., Won, S., Jin, J., Cho, J., Ryu, S.: SAFE: Formal specification and implementation of a scalable analysis framework for ECMAScript. In: FOOL 2012 (2012)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Madhavan, R., Ramalingam, G., Vaswani, K.: Modular heap analysis for higher-order programs. In: SAS, pp. 370\u2013387 (2012)","DOI":"10.1007\/978-3-642-33125-1_25"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Nguyen, P.C., Tobin-Hochstadt, S., Van Horn, D.: Soft contract verification. In: ICFP (2014)","DOI":"10.1145\/2628136.2628156"},{"key":"20_CR24","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":"20_CR25","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural shape analysis for cutpoint-free programs. In: SAS, pp. 284\u2013302 (2005)","DOI":"10.1007\/11547662_20"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare triples and frame rules for higher-order store. Logical Methods in Computer Science\u00a07(3) (2011)","DOI":"10.2168\/LMCS-7(3:21)2011"},{"key":"20_CR27","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)"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: SAS, pp. 298\u2013315 (2011)","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Xu, D.N., Jones, S.L.P., Claessen, K.: Static contract checking for Haskell. In: POPL, pp. 41\u201352 (2009)","DOI":"10.1145\/1594834.1480889"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46669-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T20:24:04Z","timestamp":1747859044000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46669-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466681","9783662466698"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46669-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}