{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:42Z","timestamp":1750308582885,"version":"3.41.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,21]],"date-time":"2017-03-21T00:00:00Z","timestamp":1490054400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ONR","award":["N00014-{09-1-0510, 11-C-0447}"],"award-info":[{"award-number":["N00014-{09-1-0510, 11-C-0447}"]}]},{"name":"UW\u2014Madison Office of the Vice Chancellor for Research and Graduate Education"},{"DOI":"10.13039\/100006602","name":"AFRL","doi-asserted-by":"crossref","award":["FA9550-09-1-0279"],"award-info":[{"award-number":["FA9550-09-1-0279"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]},{"name":"DARPA CRASH","award":["FA8650-10-C-7088"],"award-info":[{"award-number":["FA8650-10-C-7088"]}]},{"name":"DARPA MUSE","award":["FA8750-14-2-0270"],"award-info":[{"award-number":["FA8750-14-2-0270"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-0904371"],"award-info":[{"award-number":["CCF-0904371"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"ARL","award":["W911NF-09-1-0413"],"award-info":[{"award-number":["W911NF-09-1-0413"]}]},{"name":"DARPA STAC","award":["FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-15-C-0082"]}]},{"DOI":"10.13039\/100001395","name":"Wisconsin Alumni Research Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100001395","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["HR0011-12-2-0012"],"award-info":[{"award-number":["HR0011-12-2-0012"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2017,6,30]]},"abstract":"<jats:p>Recently, Esparza et al. generalized Newton\u2019s method\u2014a numerical-analysis algorithm for finding roots of real-valued functions\u2014to a method for finding fixed-points of systems of equations over semirings. Their method provides a new way to solve interprocedural dataflow-analysis problems. As in its real-valued counterpart, each iteration of their method solves a simpler \u201clinearized\u201d problem.<\/jats:p>\n          <jats:p>\n            One of the reasons this advance is exciting is that some numerical analysts have claimed that \u201c\u2018all\u2019 effective and fast iterative [numerical] methods are forms (perhaps very disguised) of Newton\u2019s method.\u201d However, there is an important difference between the dataflow-analysis and numerical-analysis contexts: When Newton\u2019s method is used in numerical-analysis problems,\n            <jats:italic>\n              <jats:bold>commutativity of multiplication<\/jats:bold>\n            <\/jats:italic>\n            is relied on to rearrange an expression of the form \u201c\n            <jats:italic>a<\/jats:italic>\n            *\n            <jats:italic>X<\/jats:italic>\n            *\n            <jats:italic>b<\/jats:italic>\n            +\n            <jats:italic>c<\/jats:italic>\n            *\n            <jats:italic>X<\/jats:italic>\n            *\n            <jats:italic>d<\/jats:italic>\n            \u201d into \u201c(\n            <jats:italic>a<\/jats:italic>\n            *\n            <jats:italic>b<\/jats:italic>\n            +\n            <jats:italic>c<\/jats:italic>\n            *\n            <jats:italic>d<\/jats:italic>\n            )*\n            <jats:italic>X<\/jats:italic>\n            .\u201d Equations with such expressions correspond to path problems described by regular languages. In contrast, when Newton\u2019s method is used for interprocedural dataflow analysis, the \u201cmultiplication\u201d operation involves function composition and hence is non-commutative: \u201c\n            <jats:italic>a<\/jats:italic>\n            *\n            <jats:italic>X<\/jats:italic>\n            *\n            <jats:italic>b<\/jats:italic>\n            +\n            <jats:italic>c<\/jats:italic>\n            *\n            <jats:italic>X<\/jats:italic>\n            *\n            <jats:italic>d<\/jats:italic>\n            \u201d cannot be rearranged into \u201c(\n            <jats:italic>a<\/jats:italic>\n            *\n            <jats:italic>b<\/jats:italic>\n            +\n            <jats:italic>c<\/jats:italic>\n            *\n            <jats:italic>d<\/jats:italic>\n            )*\n            <jats:italic>X<\/jats:italic>\n            .\u201d Equations with such expressions correspond to path problems described by linear context-free languages (LCFLs).\n          <\/jats:p>\n          <jats:p>In this article, we present an improved technique for solving the LCFL sub-problems produced during successive rounds of Newton\u2019s method. Our method applies to predicate abstraction, on which most of today\u2019s software model checkers rely.<\/jats:p>","DOI":"10.1145\/3024084","type":"journal-article","created":{"date-parts":[[2017,3,23]],"date-time":"2017-03-23T16:19:44Z","timestamp":1490285984000},"page":"1-72","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Newtonian Program Analysis via Tensor Product"],"prefix":"10.1145","volume":"39","author":[{"given":"Thomas","family":"Reps","sequence":"first","affiliation":[{"name":"University of Wisconsin\u2014Madison and Gramma Tech, Inc., Madison, WI"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emma","family":"Turetsky","sequence":"additional","affiliation":[{"name":"University of Wisconsin\u2014Madison, Mountain View, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prathmesh","family":"Prabhu","sequence":"additional","affiliation":[{"name":"University of Wisconsin\u2014Madison, Mountain View, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,3,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672077"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"A. Bouajjani J. Esparza and T. Touili. 2003. A generic approach to the static analysis of concurrent programs with procedures. In POPL. 10.1145\/604131.604137","DOI":"10.1145\/604131.604137"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/800028.808480"},{"key":"e_1_2_1_5_1","unstructured":"P. Cousot and R. Cousot. 1978. Static determination of dynamic properties of recursive procedures. In Formal Descriptions of Programming Concepts. North-Holland."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"M. Droste W. Kuich and H. Vogler (Eds.). 2009. Handbook of Weighted Automata. Springer-Verlag.","DOI":"10.5555\/1667106"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651361"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"J. Esparza S. Kiefer and M. Luttenberger. 2008. Newton\u2019s method for omega-continuous semirings. In ICALP. 10.1007\/978-3-540-70583-3_2","DOI":"10.1007\/978-3-540-70583-3_2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1857914.1857917"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"A. Farzan and Z. Kincaid. 2015. Compositional recurrence analysis. In FMCAD.","DOI":"10.5555\/2893529.2893544"},{"key":"e_1_2_1_11_1","volume-title":"Personal communication. (Oct","author":"Gallagher J. P.","year":"2016","unstructured":"J. P. Gallagher. 2016. Personal communication. (Oct. 2016)."},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"P. Ganty R. Iosif and F. Kone\u010dn\u00fd. 2016. Underapproximation of procedure summaries for integer programs. Softw. Tools for Tech. Transfer (2016). Corrected version available as arXiv:1210.4289v3.","DOI":"10.1007\/s10009-016-0420-7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"S. Graf and H. Sa\u00efdi. 1997. Construction of abstract state graphs with PVS. In CAV.","DOI":"10.5555\/647766.733618"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321939"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","unstructured":"N. B. B. Grathwohl D. Kozen and K. Mamouras. 2014. KAT + B&excl;. In CSL-LICS. 10.1145\/2603088.2603095","DOI":"10.1145\/2603088.2603095"},{"key":"e_1_2_1_16_1","unstructured":"B. Kafle and J. P. Gallagher. 2015. Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Computer Languages Systems 8 Structures (2015)."},{"volume-title":"Proceedings of the 3rd Workshop on Horn Clauses for Verification and Synthesis.","author":"Kafle B.","key":"e_1_2_1_17_1","unstructured":"B. Kafle, J. P. Gallagher, and P. Ganty. 2016. Solving non-linear Horn clauses using a linear Horn clause solver. In Proceedings of the 3rd Workshop on Horn Clauses for Verification and Synthesis."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321938"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00290339"},{"key":"e_1_2_1_20_1","unstructured":"N. Kidd A. Lal and T. Reps. 2007. WALi: The Weighted Automaton Library. Retrieved from www.cs.wisc.edu\/wpis\/wpds\/download.php."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"G. A. Kildall. 1973. A unified approach to global program optimization. In POPL. 10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"e_1_2_1_22_1","volume-title":"Tech. Rep. TR-1840. Comp. Sci. Dept., Univ. of Wisconsin\u2014Madison.","author":"Kincaid Z.","year":"2016","unstructured":"Z. Kincaid, J. Breck, A. Forouhi Boroujeni, and T. Reps. 2016. Compositional Recurrence Analysis Revisited. Tech. Rep. TR-1840. Comp. Sci. Dept., Univ. of Wisconsin\u2014Madison."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","unstructured":"J. Knoop and B. Steffen. 1992. The interprocedural coincidence theorem. In CC.","DOI":"10.5555\/647471.727286"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(77)90002-3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391466"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"A. Lal and T. Reps. 2006. Improving pushdown system model checking. In CAV. 10.1007\/11817963_32","DOI":"10.1007\/11817963_32"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"A. Lal T. Reps and G. Balakrishnan. 2005. Extended weighted pushdown systems. In CAV. 10.1007\/11513988_44","DOI":"10.1007\/11513988_44"},{"key":"e_1_2_1_29_1","volume-title":"Tech. Rep. TR-1598. Comp. Sci. Dept.","author":"Lal A.","year":"2007","unstructured":"A. Lal, T. Touili, N. Kidd, and T. Reps. 2007. Interprocedural Analysis of Concurrent Programs Under a Context Bound. Tech. Rep. TR-1598. Comp. Sci. Dept., University of Wisconsin\u2014Madison."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"A. Lal T. Touili N. Kidd and T. Reps. 2008. Interprocedural analysis of concurrent programs under a context bound. In TACAS.","DOI":"10.5555\/1792734.1792761"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00500-013-1027-5"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEC.1960.5221603"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"U. M\u00f6ncke and R. Wilhelm. 1991. Grammar flow analysis. In Attribute Grammars Applications and Systems (Int. Summer School SAGA). 151--186.","DOI":"10.5555\/645843.758268"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"M. M\u00fcller-Olm and H. Seidl. 2004. Precise interprocedural analysis through linear algebra. In POPL. 10.1145\/964001.964029","DOI":"10.1145\/964001.964029"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"M. M\u00fcller-Olm and H. Seidl. 2005. Analysis of modular arithmetic. In ESOP.","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/547567"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"T. Reps S. Horwitz and M. Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. In POPL. 49--61. 10.1145\/199448.199462","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"T. Reps A. Lal and N. Kidd. 2007. Program analysis using weighted pushdown systems. In FSTTCS.","DOI":"10.5555\/1781794.1781799"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"T. Reps E. Turetsky and P. Prabhu. 2016. Newtonian program analysis via tensor product. In POPL. 10.1145\/2837614.2837659","DOI":"10.1145\/2837614.2837659"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"M. Schlund M. Terepeta and M. Luttenberger. 2013. Putting Newton into practice: A solver for polynomial equations over semirings. In LPAR.","DOI":"10.1007\/978-3-642-45221-5_48"},{"key":"e_1_2_1_43_1","unstructured":"M. Sharir and A. Pnueli. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall."},{"key":"e_1_2_1_44_1","unstructured":"Static Driver Verifier. 2017. Retrieved from msdn.microsoft.com\/en-us\/library\/windows\/hardware\/ff552808(v&equals;vs.85).aspx."},{"key":"e_1_2_1_45_1","unstructured":"R. A. Tapia. 2008. Inverse Shifted Inverse and Rayleigh Quotient Iteration as Newton\u2019s Method. Retrieved from www.frequency.com\/video\/lecture-series-\/18347021."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322272"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289078"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","unstructured":"J. D. Ullman and A. Van Gelder. 1986. Parallel complexity of logical query programs. In Foundations of Computer Science. 10.1109\/SFCS.1986.40","DOI":"10.1109\/SFCS.1986.40"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/6448"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","unstructured":"M. Yannakakis. 1990. Graph-theoretic methods in database theory. In PODS. 10.1145\/298514.298576","DOI":"10.1145\/298514.298576"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3024084","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3024084","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3024084","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:03Z","timestamp":1750273503000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3024084"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,21]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,6,30]]}},"alternative-id":["10.1145\/3024084"],"URL":"https:\/\/doi.org\/10.1145\/3024084","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2017,3,21]]},"assertion":[{"value":"2016-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}