{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:51:36Z","timestamp":1721937096349},"reference-count":30,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2022,2,3]],"date-time":"2022-02-03T00:00:00Z","timestamp":1643846400000},"content-version":"unspecified","delay-in-days":125,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,10]]},"abstract":"Abstract<\/jats:title>The local solver TD<\/jats:bold> is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD<\/jats:bold> gains efficiency by detecting dependencies between unknowns on the fly. This algorithm has been recently extended to deal with widening<\/jats:italic> and narrowing<\/jats:italic> as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many unknowns are encountered, and all right-hand sides are monotonic<\/jats:italic>. While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all<\/jats:italic> encountered unknowns instead of a minimal set sufficient for performing the iteration. By consuming unnecessarily much space, interprocedural analyses may not succeed on seemingly small programs. In the present paper, we therefore extend the top-down<\/jats:italic> solver TD<\/jats:bold> in three ways. First, we indicate how the restriction to monotonic right-hand sides can be lifted without compromising termination. We then show how the solver can be tuned to store abstract values only when their preservation is inevitable. Finally, we also show how the solver can be extended to side-effecting<\/jats:italic> equation systems. Right-hand sides of these may not only provide values for the corresponding left-hand side unknowns but at the same time produce contributions to other unknowns. This practical extension has successfully been used for a seamless combination of context-sensitive analyses (e.g., of local states) with flow-insensitive analyses (e.g., of globals).<\/jats:p>","DOI":"10.1017\/s0960129521000499","type":"journal-article","created":{"date-parts":[[2022,2,3]],"date-time":"2022-02-03T12:56:30Z","timestamp":1643892990000},"page":"1090-1134","update-policy":"http:\/\/dx.doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":10,"title":["Three improvements to the top-down solver"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-2135-1593","authenticated-orcid":false,"given":"Helmut","family":"Seidl","sequence":"first","affiliation":[]},{"given":"Ralf","family":"Vogler","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2022,2,3]]},"reference":[{"key":"S0960129521000499_ref19","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/0743-1066(92)90035-2","article-title":"Compile-time derivation of variable dependency using abstract interpretation","volume":"13","author":"Hermenegildo","year":"1992","journal-title":"Journal of Logic Programming"},{"key":"S0960129521000499_ref20","unstructured":"Karbyshev, A. (2013). Monadic Parametricity of Second-Order Functionals. Phd thesis, Technical University Munich."},{"key":"S0960129521000499_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_12"},{"key":"S0960129521000499_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_1"},{"key":"S0960129521000499_ref29","first-page":"141","article-title":"Goblint: Path-sensitive data race analysis","volume":"30","author":"Vojdani","year":"2009","journal-title":"Annales Universitatis Scientiarum Budape- stinensis de Rolando Eotvos Nominatae, Sectio Geologica"},{"key":"S0960129521000499_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0089-6"},{"key":"S0960129521000499_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00009-X"},{"key":"S0960129521000499_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_22"},{"key":"S0960129521000499_ref25","unstructured":"Muthukumar, K. and Hermenegildo, M. (1990). Deriving a fixpoint computation algorithm for top-down abstract interpretation of logic programs. Technical Report ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759, April 1990."},{"key":"S0960129521000499_ref3","volume-title":"Lecture Notes in Computer Science","volume":"9560","author":"Apinis","year":"2016"},{"key":"S0960129521000499_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.12.005"},{"key":"S0960129521000499_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S0960129521000499_ref18","unstructured":"Hermenegildo, M. and Muthukumar, K. (1989). Determination of variable dependence information at compile-time through abstract interpretation. In: North American Conference on Logic Programming, MIT Press, 166\u2013189."},{"key":"S0960129521000499_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"S0960129521000499_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-8191(00)00051-X"},{"key":"S0960129521000499_ref22","unstructured":"Min\u00c9, A. (2001). The octagon abstract domain. In: Burd, E. , Aiken, P. and Koschke, R. (eds.) Proceedings of the Eighth Working Conference on Reverse Engineering, WCRE\u201901, Stuttgart, Germany, October 2\u20135, 2001, IEEE Computer Society, 310."},{"key":"S0960129521000499_ref23","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"S0960129521000499_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"S0960129521000499_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970337"},{"key":"S0960129521000499_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_2"},{"key":"S0960129521000499_ref21","volume-title":"Programming in the OSEK\/VDX Environment","author":"Lemieux","year":"2001"},{"key":"S0960129521000499_ref27","doi-asserted-by":"crossref","unstructured":"Seidl, H. and Vogler, R. (2018). Three improvements to the top-down solver. In: Sabel, D. and Thiemann, P. (eds.) Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03\u201305, 2018, ACM, 21:1\u201321:14.","DOI":"10.1145\/3236950.3236967"},{"key":"S0960129521000499_ref9","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"S0960129521000499_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/210308.210315"},{"key":"S0960129521000499_ref5","unstructured":"Bruynooghe, M. , Janssens, G. , Callebaut, A. and Demoen, B. (1987). Abstract interpretation: Towards the global optimization of prolog programs. In: Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, USA, August 31\u2013September 4, 1987, IEEE-CS, 192\u2013204."},{"key":"S0960129521000499_ref6","unstructured":"Charlier, B. L. and Van Hentenryck, P. (1992). A universal top-down fixpoint algorithm. Technical report, Providence, RI, USA."},{"key":"S0960129521000499_ref17","doi-asserted-by":"crossref","unstructured":"Hermenegildo, M. , Mendez-Lojo, M. and Navas, J. (2007). A flexible (C)LP-based approach to the analysis of object-oriented programs. In: LOPSTR, LNCS, vol. 4915, Springer, 154\u2013168.","DOI":"10.1007\/978-3-540-78769-3_11"},{"key":"S0960129521000499_ref13","unstructured":"Gallagher, J. P. and Henriksen, K. S. (2006). Abstract interpretation of PIC programs through logic programming. In: SCAM, IEEE Computer Society, 184\u2013196."},{"key":"S0960129521000499_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"S0960129521000499_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039704"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000499","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,21]],"date-time":"2022-06-21T05:54:48Z","timestamp":1655790888000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000499\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10]]},"references-count":30,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["S0960129521000499"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000499","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}