{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:42Z","timestamp":1780994622743,"version":"3.54.1"},"reference-count":46,"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\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-14-2-0270,FA9750-15-C-0082"],"award-info":[{"award-number":["FA8750-14-2-0270,FA9750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2889"],"award-info":[{"award-number":["N00014-17-1-2889"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100001395","name":"Wisconsin Alumni Research Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100001395","id-type":"DOI","asserted-by":"publisher"}]}],"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            Algebraic program analyses compute information about a program\u2019s behavior by first (a) computing a valid\n            <jats:italic>path expression<\/jats:italic>\n            \u2014i.e., a regular expression that recognizes all feasible execution paths (and usually more)\u2014and then (b) interpreting the path expression in a semantic algebra that defines the analysis. There are an infinite number of different regular expressions that qualify as valid path expressions, which raises the question \u201c\n            <jats:italic>Which one should we choose?<\/jats:italic>\n            \u201d While any choice yields a sound result, for many analyses the choice can have a drastic effect on the precision of the results obtained. This paper investigates the following two questions: (1)\n            <jats:italic>What does it mean for one valid path expression to be \u201cbetter\u201d than another<\/jats:italic>\n            ? (2)\n            <jats:italic>Can we compute a valid path expression that is \u201cbetter,\u201d and if so, how<\/jats:italic>\n            ? We show that it is not satisfactory to compare two path expressions\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            and\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            solely by means of the\n            <jats:italic>languages that they generate<\/jats:italic>\n            . Counter to one\u2019s intuition, it is possible for\n            <jats:italic>L<\/jats:italic>\n            (\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            ) \u228a\n            <jats:italic>L<\/jats:italic>\n            (\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            ), yet for\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            to produce a\n            <jats:italic>less-precise<\/jats:italic>\n            analysis result than\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2014and thus we would not want to perform the transformation\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2192\n            <jats:italic>E<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            . However, the exclusion of paths so as to analyze a smaller language of paths is exactly the refinement criterion used by some prior methods.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we develop an algorithm that takes as input a valid path expression\n            <jats:italic>E<\/jats:italic>\n            , and returns a valid path expression\n            <jats:italic>E<\/jats:italic>\n            \u2032 that is guaranteed to yield analysis results that are at least as good as those obtained using\n            <jats:italic>E<\/jats:italic>\n            . While the algorithm sometimes returns\n            <jats:italic>E<\/jats:italic>\n            itself, it typically does not: (i) we prove a\n            <jats:italic>no-degradation result<\/jats:italic>\n            for the algorithm\u2019s base case\u2014for transforming a leaf loop (i.e., a most-deeply-nested loop); (ii) at a non-leaf loop\n            <jats:italic>L<\/jats:italic>\n            , the algorithm treats each loop\n            <jats:italic>L<\/jats:italic>\n            \u2032 in the body of\n            <jats:italic>L<\/jats:italic>\n            as an indivisible atom, and applies the leaf-loop algorithm to\n            <jats:italic>L<\/jats:italic>\n            ; the no-degradation result carries over to (ii), as well. Our experiments show that the technique has a substantial impact: the loop-refinement algorithm allows the implementation of Compositional Recurrence Analysis to prove over 25% more assertions for a collection of challenging loop micro-benchmarks.\n          <\/jats:p>","DOI":"10.1145\/3290358","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":17,"title":["Refinement of path expressions for static analysis"],"prefix":"10.1145","volume":"3","author":[{"given":"John","family":"Cyphert","sequence":"first","affiliation":[{"name":"University of Wisconsin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jason","family":"Breck","sequence":"additional","affiliation":[{"name":"University of Wisconsin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, USA \/ GrammaTech, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277665"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.09.002"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629335.1629343"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379690"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604137"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_29"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503290"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375615"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651361"},{"key":"e_1_2_2_14_1","unstructured":"A. Farzan and Z. Kincaid. 2013. An Algebraic Framework for Compositional Program Analysis. CoRR (arXiv) (2013).  A. Farzan and Z. Kincaid. 2013. An Algebraic Framework for Compositional Program Analysis. CoRR (arXiv) (2013)."},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"A. Farzan and Z. Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD.   A. Farzan and Z. Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD.","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1981.1675827"},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"A. Flores-Montoya and R. H\u00e4hnle. 2014. Resource analysis of complex programs with cost equations. In APLAS.  A. Flores-Montoya and R. H\u00e4hnle. 2014. Resource analysis of complex programs with cost equations. In APLAS.","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"A. Gurfinkel T. Kahsai A. Komuravelli and J.A. Navas. 2015. The SeaHorn Verification Framework. In CAV.  A. Gurfinkel T. Kahsai A. Komuravelli and J.A. Navas. 2015. The SeaHorn Verification Framework. In CAV.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_53"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.234509"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"B. Jeannet and W. Serwe. 2004. Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. In AMAST.  B. Jeannet and W. Serwe. 2004. Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. In AMAST.","DOI":"10.1007\/978-3-540-27815-3_22"},{"key":"e_1_2_2_23_1","series-title":"SIAM J. Comput. (1975)","volume-title":"Finding All the Elementary Circuits of a Directed Graph","author":"Johnson D.","unstructured":"D. Johnson . 1975. Finding All the Elementary Circuits of a Directed Graph . SIAM J. Comput. (1975) . D. Johnson. 1975. Finding All the Elementary Circuits of a Directed Graph. SIAM J. Comput. (1975)."},{"key":"e_1_2_2_24_1","unstructured":"N. Kidd A. Lal and T. Reps. 2007. WALi: The Weighted Automaton Library. http:\/\/www.cs.wisc.edu\/wpis\/wpds\/download. php  N. Kidd A. Lal and T. Reps. 2007. WALi: The Weighted Automaton Library. http:\/\/www.cs.wisc.edu\/wpis\/wpds\/download. php"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Z. Kincaid. 2018. Numerical Invariants via Abstract Machines. In SAS.  Z. Kincaid. 2018. Numerical Invariants via Abstract Machines. In SAS.","DOI":"10.1007\/978-3-319-99725-4_3"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_16"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.02.028"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_2_31_1","volume-title":"Kleene Algebra with Tests and the Static Analysis of Programs. TR 2003-1915. Dept. of Comp. Sci","author":"Kozen D.","unstructured":"D. Kozen . 2003. Kleene Algebra with Tests and the Static Analysis of Programs. TR 2003-1915. Dept. of Comp. Sci ., Cornell Univ. , Ithaca, NY . D. Kozen. 2003. Kleene Algebra with Tests and the Static Analysis of Programs. TR 2003-1915. Dept. of Comp. Sci., Cornell Univ., Ithaca, NY."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275504"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_38"},{"key":"e_1_2_2_41_1","unstructured":"M. Sharir and A. Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall.  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_2_42_1","doi-asserted-by":"crossref","unstructured":"R. Sharma I. Dillig T. Dillig and A. Aiken. 2011. Simplifying Loop Invariant Generation Using Splitter Predicates. In CAV.   R. Sharma I. Dillig T. Dillig and A. Aiken. 2011. Simplifying Loop Invariant Generation Using Splitter Predicates. In CAV.","DOI":"10.1007\/978-3-642-22110-1_57"},{"key":"e_1_2_2_43_1","unstructured":"SVCOMP16 2016. 5th Int. Competition on Software Verification (SV-COMP16). https:\/\/sv- comp.sosy- lab.org\/2016\/  SVCOMP16 2016. 5th Int. Competition on Software Verification (SV-COMP16). https:\/\/sv- comp.sosy- lab.org\/2016\/"},{"key":"e_1_2_2_44_1","series-title":"SIAM J. Comput. (1972)","volume-title":"Depth-first Search and Linear Graph Algorithms","author":"Tarjan R.","unstructured":"R. Tarjan . 1972. Depth-first Search and Linear Graph Algorithms . SIAM J. Comput. (1972) . R. Tarjan. 1972. Depth-first Search and Linear Graph Algorithms. SIAM J. Comput. (1972)."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322272"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/949952.940115"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290358","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290358","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290358","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\/3290358"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290358"],"URL":"https:\/\/doi.org\/10.1145\/3290358","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"}}]}}