{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:21:56Z","timestamp":1770286916225,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544334","type":"print"},{"value":"9783662544341","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54434-1_33","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T04:20:06Z","timestamp":1489810806000},"page":"880-908","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization"],"prefix":"10.1007","author":[{"given":"Hao","family":"Tang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Di","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingfei","family":"Xiong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lingming","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyin","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lu","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Arzt, S., Bodden, E.: Stubdroid: automatic inference of precise data-flow summaries for the android framework. In: Proceedings of ICSE, pp. 725\u2013735 (2016)","DOI":"10.1145\/2884781.2884816"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Bastani, O., Anand, S., Aiken, A.: Specification inference using context-free language reachability. In: Proceedings of POPL, pp. 553\u2013566 (2015)","DOI":"10.1145\/2775051.2676977"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-45937-5_13","volume-title":"Compiler Construction","author":"P Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159\u2013179. Springer, Heidelberg (2002). doi:10.1007\/3-540-45937-5_13"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-319-21690-4_19","volume-title":"Computer Aided Verification","author":"A Das","year":"2015","unstructured":"Das, A., Lahiri, S.K., Lal, A., Li, Y.: Angelic verification: precise verification modulo unknowns. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 324\u2013342. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-21690-4_19"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-49538-X_5","volume-title":"ECOOP 95 \u2014 Object-Oriented Programming, 9th European Conference, \u00c5arhus, Denmark, August 7\u201311, 1995","author":"J Dean","year":"1995","unstructured":"Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1995. LNCS, vol. 952, pp. 77\u2013101. Springer, Heidelberg (1995). doi:10.1007\/3-540-49538-X_5"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: Proceedings of PLDI, pp. 567\u2013577 (2011)","DOI":"10.1145\/1993316.1993565"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: Proceedings of PASTE, pp. 54\u201361 (2001)","DOI":"10.1145\/379605.379665"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-08867-9_3","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2014","unstructured":"Itzhaky, S., Bj\u00f8rner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 35\u201351. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-08867-9_3"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-33125-1_17","volume-title":"Static Analysis","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: Path-sensitive backward slicing. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 231\u2013247. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33125-1_17"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Kodumal, J., Aiken, A.: The set constraint\/CFL reachability connection in practice. In: Proceedings of PLDI, pp. 207\u2013218 (2004)","DOI":"10.1145\/996893.996867"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Komondoor, R., Ramalingam, G.: Recovering data models via guarded dependences. In: Proceedings of WCRE, pp. 110\u2013119 (2007)","DOI":"10.1109\/WCRE.2007.40"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Kulkarni, S., Mangal, R., Zhang, X., Naik, M.: Accelerating program analyses by cross-program training. In: Proceedings of OOPSLA, pp. 359\u2013377 (2016)","DOI":"10.1145\/3022671.2984023"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Lattner, C., Lenharth, A., Adve, V.: Making context-sensitive points-to analysis with heap cloning practical for the real world. In: Proceedings of PLDI, pp. 278\u2013289 (2007)","DOI":"10.1145\/1273442.1250766"},{"key":"33_CR14","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. 2622, pp. 153\u2013169. Springer, Heidelberg (2003). doi:10.1007\/3-540-36579-6_12"},{"issue":"2","key":"33_CR15","first-page":"263","volume":"16","author":"A Lochbihler","year":"2009","unstructured":"Lochbihler, A., Snelting, G.: On temporal path conditions in dependence graphs. ASE 16(2), 263\u2013290 (2009)","journal-title":"ASE"},{"key":"33_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-642-40203-6_29","volume-title":"Computer Security \u2013 ESORICS 2013","author":"HD Macedo","year":"2013","unstructured":"Macedo, H.D., Touili, T.: Mining malware specifications through static reachability analysis. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 517\u2013535. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40203-6_29"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-33125-1_25","volume-title":"Static Analysis","author":"R Madhavan","year":"2012","unstructured":"Madhavan, R., Ramalingam, G., Vaswani, K.: Modular heap analysis for higher-order programs. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 370\u2013387. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33125-1_25"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Milanova, A., Huang, W., Dong, Y.: CFL-reachability and context-sensitive integrity types. In: Proceedings of PPPJ, pp. 99\u2013109 (2014)","DOI":"10.1145\/2647508.2647522"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: Proceedings of POPL, pp. 327\u2013338 (2007)","DOI":"10.1145\/1190215.1190265"},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/11823230_7","volume-title":"Static Analysis","author":"P Pratikakis","year":"2006","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.: Existential label flow inference via CFL reachability. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 88\u2013106. Springer, Heidelberg (2006). doi:10.1007\/11823230_7"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.W.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: Proceedings of PLDI, pp. 320\u2013331 (2006)","DOI":"10.1145\/1133255.1134019"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Ravitch, T., Jackson, S., Aderhold, E., Liblit, B.: Automatic generation of library bindings using static analysis. In: Proceedings of PLDI, pp. 352\u2013362 (2009)","DOI":"10.1145\/1543135.1542516"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Rehof, J., F\u00e4hndrich, M.: Type-based flow analysis: from polymorphic subtyping to CFL-reachability. In: Proceedings of POPL, pp. 54\u201366 (2001)","DOI":"10.1145\/373243.360208"},{"key":"33_CR24","doi-asserted-by":"crossref","unstructured":"Reps, T.: Shape analysis as a generalized path problem. In: Proceedings of PEPM, pp. 1\u201311 (1995)","DOI":"10.1145\/215465.215466"},{"issue":"11\u201312","key":"33_CR25","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/S0950-5849(98)00093-7","volume":"40","author":"T Reps","year":"1998","unstructured":"Reps, T.: Program analysis via graph reachability. Inf. Softw. Technol. 40(11\u201312), 701\u2013726 (1998)","journal-title":"Inf. Softw. Technol."},{"issue":"1","key":"33_CR26","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/345099.345137","volume":"22","author":"T Reps","year":"2000","unstructured":"Reps, T.: Undecidability of context-sensitive data-dependence analysis. TOPLAS 22(1), 162\u2013186 (2000)","journal-title":"TOPLAS"},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"33_CR28","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M., Rosay, G.: Speeding up slicing. In: Proceedings of FSE, pp. 11\u201320 (1994)","DOI":"10.1145\/195274.195287"},{"key":"33_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-44898-5_11","volume-title":"Static Analysis","author":"T Reps","year":"2003","unstructured":"Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 189\u2013213. Springer, Heidelberg (2003). doi:10.1007\/3-540-44898-5_11"},{"key":"33_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-71316-6_16","volume-title":"Programming Languages and Systems","author":"N Rinetzky","year":"2007","unstructured":"Rinetzky, N., Poetzsch-Heffter, A., Ramalingam, G., Sagiv, M., Yahav, E.: Modular shape analysis for dynamically encapsulated programs. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 220\u2013236. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-71316-6_16"},{"key":"33_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11688839_2","volume-title":"Compiler Construction","author":"A Rountev","year":"2006","unstructured":"Rountev, A., Kagan, S., Marlowe, T.: Interprocedural dataflow analysis in the presence of large libraries. In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol. 3923, pp. 2\u201316. Springer, Heidelberg (2006). doi:10.1007\/11688839_2"},{"key":"33_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-45306-7_3","volume-title":"Compiler Construction","author":"A Rountev","year":"2001","unstructured":"Rountev, A., Ryder, B.G.: Points-to and side-effect analyses for programs built with precompiled libraries. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 20\u201336. Springer, Heidelberg (2001). doi:10.1007\/3-540-45306-7_3"},{"key":"33_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-78791-4_4","volume-title":"Compiler Construction","author":"A Rountev","year":"2008","unstructured":"Rountev, A., Sharp, M., Xu, G.: IDE dataflow analysis in the presence of large object-oriented libraries. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 53\u201368. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78791-4_4"},{"issue":"1\u20132","key":"33_CR34","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0304-3975(96)00072-2","volume":"167","author":"M Sagiv","year":"1996","unstructured":"Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167(1\u20132), 131\u2013170 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"33_CR35","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/1178625.1178628","volume":"15","author":"G Snelting","year":"2006","unstructured":"Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. TOSEM 15(4), 410\u2013457 (2006)","journal-title":"TOSEM"},{"key":"33_CR36","doi-asserted-by":"crossref","unstructured":"Sridharan, M., Gopan, D., Shan, L., Bod\u00edk, R.: Demand-driven points-to analysis for Java. In: Proceedings of OOPSLA, pp. 57\u201376 (2005)","DOI":"10.1145\/1103845.1094817"},{"key":"33_CR37","doi-asserted-by":"crossref","unstructured":"Sridharan, M., Bod\u00edk, R.: Refinement-based context-sensitive points-to analysis for Java. In: Proceedings of PLDI, pp. 387\u2013400 (2006)","DOI":"10.1145\/1133255.1134027"},{"issue":"1","key":"33_CR38","first-page":"96","volume":"36","author":"S Sukumaran","year":"2010","unstructured":"Sukumaran, S., Sreenivas, A., Metta, R.: The dependence condition graph: precise conditions for dependence between program points. Comput. Lang. Syst. Struct. 36(1), 96\u2013121 (2010)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"33_CR39","doi-asserted-by":"crossref","unstructured":"Tang, H., Wang, X., Zhang, L., Xie, B., Zhang, L., Mei, H.: Summary-based context-sensitive data-dependence analysis in presence of callbacks. In: Proceedings of POPL, pp. 83\u201395 (2015)","DOI":"10.1145\/2775051.2676997"},{"key":"33_CR40","doi-asserted-by":"crossref","unstructured":"Tschantz, M.C., Wing, J.M.: Extracting conditional confidentiality policies. In: Proceedings of SEFM, pp. 107\u2013116 (2008)","DOI":"10.1109\/SEFM.2008.46"},{"key":"33_CR41","doi-asserted-by":"crossref","unstructured":"Xu, G., Rountev, A.: Merging equivalent contexts for scalable heap-cloning-based context-sensitive points-to analysis. In: Proceedings of ISSTA, pp. 225\u2013235 (2008)","DOI":"10.1145\/1390630.1390658"},{"key":"33_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-03013-0_6","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"G Xu","year":"2009","unstructured":"Xu, G., Rountev, A., Sridharan, M.: Scaling CFL-reachability-based points-to analysis using context-sensitive must-not-alias analysis. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 98\u2013122. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03013-0_6"},{"key":"33_CR43","doi-asserted-by":"crossref","unstructured":"Yannakakis, M.: Graph-theoretic methods in database theory. In: Proceedings of PODS, pp. 230\u2013242 (1990)","DOI":"10.1145\/298514.298576"},{"key":"33_CR44","doi-asserted-by":"crossref","unstructured":"Zhang, Q., Lyu, M.R., Yuan, H., Su, Z.: Fast algorithms for Dyck-CFL reachability with applications to alias analysis. In: Proceedings of PLDI, pp. 435\u2013446 (2013)","DOI":"10.1145\/2499370.2462159"},{"key":"33_CR45","doi-asserted-by":"crossref","unstructured":"Zhang, Q., Su, Z.: Context-sensitive data-dependence analysis via linear conjunctive language reachability. In: Proceedings of POPL, pp. 344\u2013358 (2017)","DOI":"10.1145\/3093333.3009848"},{"key":"33_CR46","doi-asserted-by":"crossref","unstructured":"Zhang, X., Mangal, R., Naik, M., Yang, H.: Hybrid top-down and bottom-up interprocedural analysis. In: Proceedings of PLDI, pp. 249\u2013258 (2014)","DOI":"10.1145\/2666356.2594328"},{"key":"33_CR47","doi-asserted-by":"crossref","unstructured":"Zheng, X., Rugina, R.: Demand-driven alias analysis for C. In: Proceedings of POPL, pp. 351\u2013363 (2008)","DOI":"10.1145\/1328438.1328464"},{"key":"33_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-319-03542-0_21","volume-title":"Programming Languages and Systems","author":"H Zhu","year":"2013","unstructured":"Zhu, H., Dillig, T., Dillig, I.: Automated inference of library specifications for source-sink property verification. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 290\u2013306. Springer, Heidelberg (2013). doi:10.1007\/978-3-319-03542-0_21"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54434-1_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T15:57:49Z","timestamp":1635263869000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}