{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T13:28:04Z","timestamp":1749648484849,"version":"3.37.3"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005967","name":"Linnaeus University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005967","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Static program analysis is in general more precise if it is sensitive to execution contexts (execution paths). But then it is also more expensive in terms of memory consumption. For languages with conditions and iterations, the number of contexts grows exponentially with the program size. This problem is not just a theoretical issue. Several papers evaluating inter-procedural context-sensitive data-flow analysis report severe memory problems, and the path-explosion problem is a major issue in program verification and model checking. In this paper we propose <jats:italic>\u03c7<\/jats:italic>-terms as a means to capture and manipulate context-sensitive program information in a data-flow analysis. <jats:italic>\u03c7<\/jats:italic>-terms are implemented as directed acyclic graphs without any redundant subgraphs. We introduce the <jats:italic>k<\/jats:italic><jats:italic>-approximation<\/jats:italic> and the <jats:italic>l<\/jats:italic><jats:italic>-loop-approximation<\/jats:italic> that limit the size of the context-sensitive information at the cost of analysis precision. We prove that every context-insensitive data-flow analysis has a corresponding <jats:italic>k<\/jats:italic>,<jats:italic>l<\/jats:italic><jats:italic>-approximated<\/jats:italic> context-sensitive analysis, and that these analyses are sound and guaranteed to reach a fixed point. We also present detailed algorithms outlining a compact, redundancy-free, and DAG-based implementation of <jats:italic>\u03c7<\/jats:italic>-terms.<\/jats:p>","DOI":"10.1007\/s00224-022-10093-w","type":"journal-article","created":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T04:02:56Z","timestamp":1658116976000},"page":"911-956","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Framework for Memory Efficient Context-Sensitive Program Analysis"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7555-7335","authenticated-orcid":false,"given":"Mathias","family":"Hedenborg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonas","family":"Lundberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Welf","family":"L\u00f6we","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Trapp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,7,18]]},"reference":[{"issue":"6","key":"10093_CR1","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"27","author":"SB Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. 27 (6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"10093_CR2","doi-asserted-by":"crossref","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201988. ACM (1988)","DOI":"10.1145\/73560.73561"},{"key":"10093_CR3","doi-asserted-by":"publisher","unstructured":"Ball, T., Rajamani, S.K.: Bebop: a path-sensitive interprocedural dataflow engine. In: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE \u201901, pp. 97\u2013103. ACM, New York. https:\/\/doi.org\/10.1145\/379605.379690 (2001)","DOI":"10.1145\/379605.379690"},{"key":"10093_CR4","doi-asserted-by":"crossref","unstructured":"Berndl, M., Lhotak, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: Proceedings of the Conference on Programmimg Language Design and Implementation (PLDI\u201903), pp. 103\u2013114 (2003)","DOI":"10.1145\/780822.781144"},{"key":"10093_CR5","doi-asserted-by":"publisher","unstructured":"Boonstoppel, P., Cadar, C., Engler, D.: RWset: attacking path explosion in constraint-based test generation. In: 14th International Conference, TACAS 2008, pp. 351\u2013366. Springer Berlin Heidelberg, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-540-78800-3\u2216_27 (2008)","DOI":"10.1007\/978-3-540-78800-3\u2216_27"},{"issue":"8","key":"10093_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"10093_CR7","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"10093_CR8","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013). https:\/\/doi.org\/10.1145\/2408776.2408795","journal-title":"Commun. ACM"},{"key":"10093_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximations of fixed points. In: Conference Record of the Fourth Annual ACM SIGACT\/SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"10093_CR10","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., Wegman, M., Zadeck, 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":"10093_CR11","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivanc\u0306i\u0107, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Proceedings of the Conference on Principles of Programming Languages (POPL \u201910) (2010)","DOI":"10.1145\/1706299.1706309"},{"key":"10093_CR12","doi-asserted-by":"publisher","unstructured":"Hedenborg, M., Lundberg, J., L\u00f6we, W.: Memory efficient context-sensitive program analysis. Elsevier J. Syst. Softw. 177. https:\/\/doi.org\/10.1016\/j.jss.2021.110952(2021)","DOI":"10.1016\/j.jss.2021.110952"},{"key":"10093_CR13","doi-asserted-by":"publisher","unstructured":"Heinze, T.S., Amme, W.: Sparse analysis of variable path predicates based upon SSA-form. In: 7th International Symposium, ISoLA 2016, pp. 227\u2013242. Springer International Publishing, Cham. https:\/\/doi.org\/10.1007\/978-3-319-47166-2\u2216_16 (2016)","DOI":"10.1007\/978-3-319-47166-2\u2216_16"},{"issue":"OOPSLA","key":"10093_CR14","doi-asserted-by":"publisher","first-page":"100:1","DOI":"10.1145\/3133924","volume":"1","author":"S Jeong","year":"2017","unstructured":"Jeong, S., Jeon, M., Cha, S., Oh, H.: Data-driven context-sensitivity for points-to analysis. Proc. ACM Program Lang. 1 (OOPSLA), 100:1\u2013100:28 (2017). https:\/\/doi.org\/10.1145\/3133924","journal-title":"Proc. ACM Program Lang."},{"issue":"6","key":"10093_CR15","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/2499370.2462191","volume":"48","author":"G Kastrinis","year":"2013","unstructured":"Kastrinis, G., Smaragdakis, Y.: Hybrid context-sensitivity for points-to analysis. SIGPLAN Not. 48(6), 423\u2013434 (2013). https:\/\/doi.org\/10.1145\/2499370.2462191","journal-title":"SIGPLAN Not."},{"issue":"3","key":"10093_CR16","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/3230624","volume":"40","author":"SW Kim","year":"2018","unstructured":"Kim, S.W., Rival, X., Ryu, S.: A theoretical foundation of sensitivity in an abstract interpretation framework. ACM Trans. Program. Lang. Syst. 40(3), 13:1\u201313:44 (2018). https:\/\/doi.org\/10.1145\/3230624","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10093_CR17","doi-asserted-by":"publisher","unstructured":"Knoop, J., R\u00fcthing, O.: Constant propagation on the value graph: simple constants and beyond. In: Watt, D. (ed.) Compiler Construction, Lecture Notes in Computer Science, vol. 1781, pp. 94\u2013110. Springer Berlin Heidelberg. https:\/\/doi.org\/10.1007\/3-540-46423-9\u2216_7 (2000)","DOI":"10.1007\/3-540-46423-9\u2216_7"},{"key":"10093_CR18","doi-asserted-by":"publisher","unstructured":"Lhot\u00e1k, O., Hendren, L.: Context-sensitive points-to analysis: is it worth it?. In: Proceedings of the 15th International Conference on Compiler Construction, CC\u201906, pp. 47\u201364. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/11688839\u2216_5(2006)","DOI":"10.1007\/11688839\u2216_5"},{"issue":"1","key":"10093_CR19","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. 18(1), 1\u201353 (2008). https:\/\/doi.org\/10.1145\/1391984.1391987https:\/\/doi.org\/10.1145\/1391984.1391987","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"1","key":"10093_CR20","doi-asserted-by":"publisher","first-page":"3: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. 18(1), 3:1\u20133:53 (2008). https:\/\/doi.org\/10.1145\/1391984.1391987","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"OOPSLA","key":"10093_CR21","doi-asserted-by":"publisher","first-page":"141:1","DOI":"10.1145\/3276511","volume":"2","author":"Y Li","year":"2018","unstructured":"Li, Y., Tan, T., M\u00f8ller, A., Smaragdakis, Y.: Precision-guided context sensitivity for pointer analysis. Proc. ACM Program. Lang. 2(OOPSLA), 141:1\u2013141:29 (2018). https:\/\/doi.org\/10.1145\/3276511","journal-title":"Proc. ACM Program. Lang."},{"key":"10093_CR22","doi-asserted-by":"publisher","unstructured":"Li, Y., Tan, T., M\u00f8ller, A., Smaragdakis, Y.: Scalability-first pointer analysis with self-tuning context-sensitivity. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2018, pp. 129\u2013140. ACM, New York. https:\/\/doi.org\/10.1145\/3236024.3236041 (2018)","DOI":"10.1145\/3236024.3236041"},{"key":"10093_CR23","unstructured":"Lundberg, J.: Fast and precise points-to analysis. Ph.D. thesis, Linnaeus University (2014)"},{"issue":"10","key":"10093_CR24","doi-asserted-by":"publisher","first-page":"1428","DOI":"10.1016\/j.infsof.2009.04.012","volume":"51","author":"J Lundberg","year":"2009","unstructured":"Lundberg, J., Gutzmann, T., Edvinsson, M., L\u00f6we, W.: Fast and precise points-to analysis. J. Inf. Softw. Technol. 51(10), 1428\u20131439 (2009)","journal-title":"J. Inf. Softw. Technol."},{"issue":"20","key":"10093_CR25","first-page":"2851","volume":"18","author":"J Lundberg","year":"2013","unstructured":"Lundberg, J., L\u00f6we, W.: Points-to analysis: a fine-grained evaluation. J. Univers. Comput. Sci. 18(20), 2851\u20132878 (2013)","journal-title":"J. Univers. Comput. Sci."},{"key":"10093_CR26","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01237234","volume":"28","author":"T Marlowe","year":"1990","unstructured":"Marlowe, T., Ryder, B.: Properties of data flow frameworks: a unified model. Acta Inform. 28, 121\u2013163 (1990)","journal-title":"Acta Inform."},{"issue":"1","key":"10093_CR27","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. 14 (1), 1\u201341 (2005)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"1","key":"10093_CR28","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. 14(1), 1\u201341 (2005). https:\/\/doi.org\/10.1145\/1044834.1044835","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10093_CR29","volume-title":"Advanced Compiler Design Implementation","author":"SS Muchnick","year":"1997","unstructured":"Muchnick, S.S.: Advanced Compiler Design Implementation. Morgan Kaufmann Publishers, San Francisco (1997)"},{"issue":"6","key":"10093_CR30","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1145\/2666356.2594318","volume":"49","author":"H Oh","year":"2014","unstructured":"Oh, H., Lee, W., Heo, K., Yang, H., Yi, K.: Selective context-sensitivity guided by impact pre-analysis. SIGPLAN Not. 49(6), 475\u2013484 (2014). https:\/\/doi.org\/10.1145\/2666356.2594318","journal-title":"SIGPLAN Not."},{"issue":"1","key":"10093_CR31","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. ACM Trans. Program. Lang. Syst. 22(1), 162\u2013186 (2000). https:\/\/doi.org\/10.1145\/345099.345137","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10093_CR32","doi-asserted-by":"publisher","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5). https:\/\/doi.org\/10.1145\/1275497.1275501 (2007)","DOI":"10.1145\/1275497.1275501"},{"key":"10093_CR33","doi-asserted-by":"publisher","unstructured":"R\u00fcthing, O., Knoop, J., Steffen, B.: Detecting equalities of variables: combining efficiency with precision. In: Cortesi, A., Fil\u00e9, G. (eds.) Static Analysis, Lecture Notes in Computer Science, vol. 1694, pp. 232\u2013247. Springer Berlin Heidelberg. https:\/\/doi.org\/10.1007\/3-540-48294-6\u2216_15 (1999)","DOI":"10.1007\/3-540-48294-6\u2216_15"},{"key":"10093_CR34","unstructured":"Shivers, O.: Control-flow analysis of higher-order languages. Tech. rep., PhD thesis, Carnegie-Mellon University, CMU-CS-91-145 (1991)"},{"issue":"6","key":"10093_CR35","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1145\/2666356.2594320","volume":"49","author":"Y Smaragdakis","year":"2014","unstructured":"Smaragdakis, Y., Kastrinis, G., Balatsouras, G.: Introspective analysis: context-sensitivity, across the board. SIGPLAN Not. 49(6), 485\u2013495 (2014). https:\/\/doi.org\/10.1145\/2666356.2594320","journal-title":"SIGPLAN Not."},{"issue":"6","key":"10093_CR36","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1145\/1133255.1134027","volume":"41","author":"M Sridharan","year":"2006","unstructured":"Sridharan, M., Bod\u00edk, R.: Refinement-based context-sensitive points-to analysis for java. SIGPLAN Not. 41(6), 387\u2013400 (2006). https:\/\/doi.org\/10.1145\/1133255.1134027","journal-title":"SIGPLAN Not."},{"issue":"6","key":"10093_CR37","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/3140587.3062359","volume":"52","author":"R Thiessen","year":"2017","unstructured":"Thiessen, R., Lhot\u00e1k, O.: Context transformations for pointer analysis. SIGPLAN Not. 52(6), 263\u2013277 (2017). https:\/\/doi.org\/10.1145\/3140587.3062359","journal-title":"SIGPLAN Not."},{"key":"10093_CR38","doi-asserted-by":"publisher","unstructured":"Tonella, P.: Reverse engineering of object oriented code. In: Proceedings of the 27th International Conference on Software Engineering, ICSE \u201905, pp. 724\u2013725. ACM, New York. https:\/\/doi.org\/10.1145\/1062455.1062637https:\/\/doi.org\/10.1145\/1062455.1062637 (2005)","DOI":"10.1145\/1062455.1062637 10.1145\/1062455.1062637"},{"key":"10093_CR39","unstructured":"Trapp, M.: Optimerung Objektorientierter Programme. Ph.D. thesis, Universit\u00e4t Karlsruhe (1999)"},{"key":"10093_CR40","first-page":"154","volume":"1337","author":"M Trapp","year":"2015","unstructured":"Trapp, M., Hedenborg, M., Lundberg, J., L\u00f6we, W.: Capturing and manipulating context-sensitive program information. Software Engineering Workshops 2015 1337, 154\u2013163 (2015). http:\/\/ceur-ws.org\/Vol-1337\/","journal-title":"Software Engineering Workshops 2015"},{"key":"10093_CR41","doi-asserted-by":"crossref","unstructured":"Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI\u201904) (2004)","DOI":"10.1145\/996841.996859"},{"key":"10093_CR42","doi-asserted-by":"publisher","unstructured":"Zhu, J.: Symbolic pointer analysis. In: Proceedings of the 2002 IEEE\/ACM International Conference on Computer-aided Design, ICCAD \u201902, pp. 150\u2013157. ACM, New York. https:\/\/doi.org\/10.1145\/774572.774594https:\/\/doi.org\/10.1145\/774572.774594 (2002)","DOI":"10.1145\/774572.774594 10.1145\/774572.774594"},{"issue":"6","key":"10093_CR43","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/996893.996860","volume":"39","author":"J Zhu","year":"2004","unstructured":"Zhu, J., Calman, S.: Symbolic pointer analysis revisited. SIGPLAN Not. 39(6), 145\u2013157 (2004). https:\/\/doi.org\/10.1145\/996893.996860","journal-title":"SIGPLAN Not."}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-022-10093-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00224-022-10093-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-022-10093-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T07:03:17Z","timestamp":1664434997000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00224-022-10093-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,18]]},"references-count":43,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["10093"],"URL":"https:\/\/doi.org\/10.1007\/s00224-022-10093-w","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"type":"print","value":"1432-4350"},{"type":"electronic","value":"1433-0490"}],"subject":[],"published":{"date-parts":[[2022,7,18]]},"assertion":[{"value":"13 June 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 July 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}