{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:05:12Z","timestamp":1770293112346,"version":"3.49.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            Precise static analyses are context-, field- and flow-sensitive. Context- and field-sensitivity are both expressible as context-free language (CFL) reachability problems. Solving both CFL problems along the same data-flow path is undecidable, which is why most flow-sensitive data-flow analyses over-approximate field-sensitivity through\n            <jats:italic>k<\/jats:italic>\n            -limited access-path, or through access graphs. Unfortunately, as our experience and this paper show, both representations do not scale very well when used to analyze programs with recursive data structures.\n          <\/jats:p>\n          <jats:p>Any single CFL-reachability problem is efficiently solvable, by means of a pushdown system. This work thus introduces the concept of synchronized pushdown systems (SPDS). SPDS encode both procedure calls\/returns and field stores\/loads as separate but \u201csynchronized\u201d CFL reachability problems. An SPDS solves both individual problems precisely, and approximation occurs only in corner cases that are apparently rare in practice: at statements where both problems are satisfied but not along the same data-flow path.<\/jats:p>\n          <jats:p>\n            SPDS are also efficient: formal complexity analysis shows that SPDS shift the complexity from |\n            <jats:italic>F<\/jats:italic>\n            |\n            <jats:sup>\n              3\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sup>\n            under\n            <jats:italic>k<\/jats:italic>\n            -limiting to |\n            <jats:italic>S<\/jats:italic>\n            ||\n            <jats:italic>F<\/jats:italic>\n            |\n            <jats:sup>2<\/jats:sup>\n            , where\n            <jats:italic>F<\/jats:italic>\n            is the set of fields and\n            <jats:italic>S<\/jats:italic>\n            the set of statements involved in a data-flow. Our evaluation using DaCapo shows this shift to pay off in practice: SPDS are almost as efficient as\n            <jats:italic>k<\/jats:italic>\n            -limiting with\n            <jats:italic>k<\/jats:italic>\n            =1 although their precision equals\n            <jats:italic>k<\/jats:italic>\n            =\u221e. For a typestate analysis SPDS accelerate the analysis up to 83\u00d7 for data-flows of objects that involve many field accesses but span rather few methods.\n          <\/jats:p>\n          <jats:p>We conclude that SPDS can provide high precision and further improve scalability, in particularly when used in analyses that expose rather local data flows.<\/jats:p>","DOI":"10.1145\/3290361","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":55,"title":["Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems"],"prefix":"10.1145","volume":"3","author":[{"given":"Johannes","family":"Sp\u00e4th","sequence":"first","affiliation":[{"name":"Fraunhofer IEM, Germany"}]},{"given":"Karim","family":"Ali","sequence":"additional","affiliation":[{"name":"University of Alberta, Canada"}]},{"given":"Eric","family":"Bodden","sequence":"additional","affiliation":[{"name":"University of Paderborn, Germany \/ Fraunhofer IEM, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3088515.3088517"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2259051.2259052"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236454.3236500"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/646732.701281"},{"key":"e_1_2_2_6_1","volume-title":"Optimal Dyck Reachability for DataDependence and Alias Analysis. In Symposium on Principles of Programming Languages (POPL). 30:1\u201330:30","author":"Chatterjee Krishnendu","year":"2018","unstructured":"Krishnendu Chatterjee , Bhavya Choudhary , and Andreas Pavlogiannis . 2018 . Optimal Dyck Reachability for DataDependence and Alias Analysis. In Symposium on Principles of Programming Languages (POPL). 30:1\u201330:30 . Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis. 2018. Optimal Dyck Reachability for DataDependence and Alias Analysis. In Symposium on Principles of Programming Languages (POPL). 30:1\u201330:30."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349311"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_29"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178263"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364576"},{"key":"e_1_2_2_11_1","volume-title":"Efficient Algorithms for Model Checking Pushdown Systems. In International Conference on Computer Aided Verification (CAV). 232\u2013247","author":"Esparza Javier","year":"2000","unstructured":"Javier Esparza , David Hansel , Peter Rossmanith , and Stefan Schwoon . 2000 . Efficient Algorithms for Model Checking Pushdown Systems. In International Conference on Computer Aided Verification (CAV). 232\u2013247 . Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. 2000. Efficient Algorithms for Model Checking Pushdown Systems. In International Conference on Computer Aided Verification (CAV). 232\u2013247."},{"key":"e_1_2_2_12_1","volume-title":"Bottom-Up Context-Sensitive Pointer Analysis for Java. In Asian Symposium on Programming Languages and Systems (APLAS). 465\u2013484","author":"Feng Yu","year":"2015","unstructured":"Yu Feng , Xinyu Wang , Isil Dillig , and Thomas Dillig . 2015 . Bottom-Up Context-Sensitive Pointer Analysis for Java. In Asian Symposium on Programming Languages and Systems (APLAS). 465\u2013484 . Yu Feng, Xinyu Wang, Isil Dillig, and Thomas Dillig. 2015. Bottom-Up Context-Sensitive Pointer Analysis for Java. In Asian Symposium on Programming Languages and Systems (APLAS). 465\u2013484."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348255"},{"key":"e_1_2_2_14_1","volume-title":"A Direct Symbolic Approach to Model Checking Pushdown Systems. Electronic Notes in Theoretical Computer Science","author":"Finkel Alain","year":"1997","unstructured":"Alain Finkel , Bernard Willems , and Pierre Wolper . 1997. A Direct Symbolic Approach to Model Checking Pushdown Systems. Electronic Notes in Theoretical Computer Science ( 1997 ), 27\u201337. Alain Finkel, Bernard Willems, and Pierre Wolper. 1997. A Direct Symbolic Approach to Model Checking Pushdown Systems. Electronic Notes in Theoretical Computer Science (1997), 27\u201337."},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Manuel Geffken Hannes Saffrich and Peter Thiemann. 2014. Precise Interprocedural Side-Effect Analysis. In International Colloquium on Theoretical Aspects of Computing (ICTAC). 188\u2013205.  Manuel Geffken Hannes Saffrich and Peter Thiemann. 2014. Precise Interprocedural Side-Effect Analysis. In International Colloquium on Theoretical Aspects of Computing (ICTAC). 188\u2013205.","DOI":"10.1007\/978-3-319-10882-7_12"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837631"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133926"},{"key":"e_1_2_2_18_1","volume-title":"Data-Flow Analysis of Programs with Associative Arrays. In International Workshop on Engineering Safety and Security Systems (ESSS). 56\u201370","author":"Hauzar David","year":"2014","unstructured":"David Hauzar , Jan Kofron , and Pavel Basteck\u00fd . 2014 . Data-Flow Analysis of Programs with Associative Arrays. In International Workshop on Engineering Safety and Security Systems (ESSS). 56\u201370 . David Hauzar, Jan Kofron, and Pavel Basteck\u00fd. 2014. Data-Flow Analysis of Programs with Associative Arrays. In International Workshop on Engineering Safety and Security Systems (ESSS). 56\u201370."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1028664.1028717"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595701"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931098"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179519"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1290520.1290521"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_2_2_25_1","volume-title":"European Conference on Object-Oriented Programming (ECOOP). 10:1\u201310:27","author":"Kr\u00fcger Stefan","year":"2018","unstructured":"Stefan Kr\u00fcger , Johannes Sp\u00e4th , Karim Ali , Eric Bodden , and Mira Mezini . 2018 . CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs . In European Conference on Object-Oriented Programming (ECOOP). 10:1\u201310:27 . Stefan Kr\u00fcger, Johannes Sp\u00e4th, Karim Ali, Eric Bodden, and Mira Mezini. 2018. CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs. In European Conference on Object-Oriented Programming (ECOOP). 10:1\u201310:27."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_32"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_7"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_44"},{"key":"e_1_2_2_29_1","volume-title":"Cetus Users and Compiler Infrastructure Workshop (CETUS","author":"Lam Patrick","year":"2011","unstructured":"Patrick Lam , Eric Bodden , Ond\u0159ej Lhot\u00e1k , and Laurie Hendren . 2011 . The Soot framework for Java program analysis: a retrospective . In Cetus Users and Compiler Infrastructure Workshop (CETUS 2011). http:\/\/www.bodden.de\/pubs\/lblh11soot. pdf Patrick Lam, Eric Bodden, Ond\u0159ej Lhot\u00e1k, and Laurie Hendren. 2011. The Soot framework for Java program analysis: a retrospective. In Cetus Users and Compiler Infrastructure Workshop (CETUS 2011). http:\/\/www.bodden.de\/pubs\/lblh11soot. pdf"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635878"},{"key":"e_1_2_2_31_1","volume-title":"Access-Path Abstraction: Scaling Field-Sensitive Data-Flow Analysis with Unbounded Access Paths. In International Conference on Automated Software Engineering (ASE). 619\u2013629","author":"Lerch Johannes","year":"2015","unstructured":"Johannes Lerch , Johannes Sp\u00e4th , Eric Bodden , and Mira Mezini . 2015 . Access-Path Abstraction: Scaling Field-Sensitive Data-Flow Analysis with Unbounded Access Paths. In International Conference on Automated Software Engineering (ASE). 619\u2013629 . Johannes Lerch, Johannes Sp\u00e4th, Eric Bodden, and Mira Mezini. 2015. Access-Path Abstraction: Scaling Field-Sensitive Data-Flow Analysis with Unbounded Access Paths. In International Conference on Automated Software Engineering (ASE). 619\u2013629."},{"key":"e_1_2_2_32_1","volume-title":"Hendren","author":"Lhot\u00e1k Ondrej","year":"2003","unstructured":"Ondrej Lhot\u00e1k and Laurie J . Hendren . 2003 . Scaling Java Points-to Analysis Using SPARK. In Compiler Construction (CC) . 153\u2013169. Ondrej Lhot\u00e1k and Laurie J. Hendren. 2003. Scaling Java Points-to Analysis Using SPARK. In Compiler Construction (CC). 153\u2013169."},{"key":"e_1_2_2_33_1","volume-title":"Lam","author":"Benjamin Livshits V.","year":"2005","unstructured":"V. Benjamin Livshits and Monica S . Lam . 2005 . Finding Security Vulnerabilities in Java Applications with Static Analysis. In USENIX Security Symposium . https:\/\/www.usenix.org\/conference\/14th- usenix- security- symposium\/ finding- security- vulnerabilities- java- applications- static V. Benjamin Livshits and Monica S. Lam. 2005. Finding Security Vulnerabilities in Java Applications with Static Analysis. In USENIX Security Symposium. https:\/\/www.usenix.org\/conference\/14th- usenix- security- symposium\/ finding- security- vulnerabilities- java- applications- static"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094840"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806631"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_8"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070515"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487568.2487569"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_2_41_1","volume-title":"Program Analysis Using Weighted Pushdown Systems. In International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 23\u201351","author":"Reps Thomas W.","year":"2007","unstructured":"Thomas W. Reps , Akash Lal , and Nicholas Kidd . 2007 . Program Analysis Using Weighted Pushdown Systems. In International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 23\u201351 . Thomas W. Reps, Akash Lal, and Nicholas Kidd. 2007. Program Analysis Using Weighted Pushdown Systems. In International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 23\u201351."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760283"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837659"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_2_46_1","first-page":"1","article-title":"IDEal : Efficient and Precise Alias-Aware Dataflow Analysis","volume":"99","author":"Sp\u00e4th Johannes","year":"2017","unstructured":"Johannes Sp\u00e4th , Karim Ali , and Eric Bodden . 2017 . IDEal : Efficient and Precise Alias-Aware Dataflow Analysis . In ObjectOriented Programming Systems, Languages and Applications (OOPSLA). 99 : 1 \u2013 99 :27. Johannes Sp\u00e4th, Karim Ali, and Eric Bodden. 2017. IDEal : Efficient and Precise Alias-Aware Dataflow Analysis. In ObjectOriented Programming Systems, Languages and Applications (OOPSLA). 99:1\u201399:27.","journal-title":"ObjectOriented Programming Systems, Languages and Applications (OOPSLA)."},{"key":"e_1_2_2_47_1","volume-title":"Boomerang: Demand-Driven Flow- and ContextSensitive Pointer Analysis for Java. In European Conference on Object-Oriented Programming (ECOOP). 22:1\u201322:26","author":"Sp\u00e4th Johannes","year":"2016","unstructured":"Johannes Sp\u00e4th , Lisa Nguyen Quang Do , Karim Ali , and Eric Bodden . 2016 . Boomerang: Demand-Driven Flow- and ContextSensitive Pointer Analysis for Java. In European Conference on Object-Oriented Programming (ECOOP). 22:1\u201322:26 . Johannes Sp\u00e4th, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. 2016. Boomerang: Demand-Driven Flow- and ContextSensitive Pointer Analysis for Java. In European Conference on Object-Oriented Programming (ECOOP). 22:1\u201322:26."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"Manu Sridharan Satish Chandra Julian Dolby Stephen J. Fink and Eran Yahav. 2013. Alias Analysis for Object-Oriented Programs. In Aliasing in Object-Oriented Programming. Types Analysis and Verification. 196\u2013232.   Manu Sridharan Satish Chandra Julian Dolby Stephen J. Fink and Eran Yahav. 2013. Alias Analysis for Object-Oriented Programs. In Aliasing in Object-Oriented Programming. Types Analysis and Verification. 196\u2013232.","DOI":"10.1007\/978-3-642-36946-9_8"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_15"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542486"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_30"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_6"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001440"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462159"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009848"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290361","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290361","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290361"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":58,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290361"],"URL":"https:\/\/doi.org\/10.1145\/3290361","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}