{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T02:00:08Z","timestamp":1768960808990,"version":"3.49.0"},"reference-count":50,"publisher":"Frontiers Media SA","license":[{"start":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T00:00:00Z","timestamp":1768867200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["frontiersin.org"],"crossmark-restriction":true},"short-container-title":["Front. Comput. Sci."],"abstract":"<jats:p>\n                    Value analysis is the task of understanding what concrete values a program might compute for each variable or memory region. Historically, research focused mostly on numerical analysis (i.e., value analysis of programs manipulating numeric values), while string analyses have received wider attention in the last two decades. String analyses present a key challenge: reasoning about strings entails reasoning about integer values either used as arguments to string operations (e.g., evaluating a substring) or returned by string operations (e.g., calculating the length of a string). Traditionally, string analyses were formalized with respect to a specific numeric analysis, usually considering constant values or their possible ranges, tailoring definitions, semantic proofs, and implementations to that particular combination, hence hindering the adoption of the analyses in different contexts. This study presents a modular framework to define\n                    <jats:italic>whole-value analyses<\/jats:italic>\n                    (that is, combinations of numeric analyses, string analyses, and possibly other value types computed by a program) by Abstract Interpretation. The framework defines information exchange between the different analyses in the form of abstract constraints, allowing each analysis to perform given only a generic and analysis-independent description of the abstract values computed by other analyses. Adopting such a framework (i) ensures that soundness proofs are still valid when changing the combination of domains used, and (ii) eases implementation and experimentation of different combinations of value analyses, simplifying comparisons between different scientific contributions and augmenting the set of domains an abstract interpreter can use to analyze a program.\n                  <\/jats:p>","DOI":"10.3389\/fcomp.2025.1655377","type":"journal-article","created":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T13:30:51Z","timestamp":1768915851000},"update-policy":"https:\/\/doi.org\/10.3389\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Whole-value analysis by abstract interpretation"],"prefix":"10.3389","volume":"7","author":[{"given":"Luca","family":"Negrini","sequence":"first","affiliation":[{"name":"Department of Environmental Sciences, Informatics and Statistics, Ca' Foscari University of Venice","place":["Venice, Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1965","published-online":{"date-parts":[[2026,1,20]]},"reference":[{"key":"B1","first-page":"943","article-title":"\u201cEfficient handling of string-number conversion,\u201d","volume-title":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020","author":"Abdulla","year":"2020"},{"key":"B2","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/978-3-319-08867-9_10","article-title":"\u201cString constraints for verification,\u201d","volume-title":"Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26","author":"Abdulla","year":"2014"},{"key":"B3","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-030-31784-3_16","article-title":"\u201cChain-free string constraints,\u201d","volume-title":"Automated Technology for Verification and Analysis: 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings 17","author":"Abdulla","year":"2019"},{"key":"B4","doi-asserted-by":"publisher","first-page":"297","DOI":"10.3233\/FI-2018-1650","article-title":"Reference abstract domains and applications to string analysis","volume":"158","author":"Amadini","year":"2018","journal-title":"Fundam. Inform"},{"key":"B5","doi-asserted-by":"publisher","first-page":"103368","DOI":"10.1016\/j.artint.2020.103368","article-title":"Dashed strings for string constraint solving","volume":"289","author":"Amadini","year":"2020","journal-title":"Artif. Intell"},{"key":"B6","volume-title":"Frameworks for Analyzing Multi-Threaded C","author":"Apinis","year":"2014"},{"key":"B7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.entcs.2017.02.003","article-title":"Abstract domains for type juggling","volume":"331","author":"Arceri","year":"2017","journal-title":"Electron. Notes Theor. Comput. Sci"},{"key":"B8","doi-asserted-by":"publisher","first-page":"3525","DOI":"10.3390\/app10103525","article-title":"Static analysis for ecmascript string manipulation programs","volume":"10","author":"Arceri","year":"2020","journal-title":"Appl. Sci"},{"key":"B9","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1051\/ita:2000127","article-title":"Computing the prefix of an automaton","volume":"34","author":"B\u00e9al","year":"2000","journal-title":"RAIRO"},{"key":"B10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290362","article-title":"Decision procedures for path feasibility of string-manipulating programs with complex operations","volume":"3","author":"Chen","year":"2019","journal-title":"Proc ACM Program Lang"},{"key":"B11","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/11924661_23","article-title":"\u201cA practical string analyzer by the widening approach,\u201d","volume-title":"Asian Symposium on Programming Languages and Systems","author":"Choi","year":"2006"},{"key":"B12","doi-asserted-by":"publisher","first-page":"814","DOI":"10.1145\/945885.945890","article-title":"Extending java for high-level web service construction","volume":"25","author":"Christensen","year":"","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"B13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","article-title":"\u201cPrecise analysis of string expressions,\u201d","author":"Christensen","year":"","journal-title":"Static Analysis"},{"key":"B14","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1067625.806556","article-title":"Information transmission in computational systems","volume":"11","author":"Cohen","year":"1977","journal-title":"SIGOPS Oper. Syst. Rev"},{"key":"B15","doi-asserted-by":"publisher","first-page":"325","DOI":"10.4204\/EPTCS.129.19","article-title":"A survey on product operators in abstract interpretation","volume":"129","author":"Cortesi","year":"2013","journal-title":"Electron. Proc. Theor. Comp. Sci"},{"key":"B16","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1002\/spe.2218","article-title":"A suite of abstract domains for static analysis of string values","volume":"45","author":"Costantini","year":"2015","journal-title":"Softw. Pract. Exp"},{"key":"B17","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1145\/263699.263744","article-title":"\u201cTypes as abstract interpretations,\u201d","volume-title":"Proceedings of POPL '97, POPL '97","author":"Cousot","year":"1997"},{"key":"B18","author":"Cousot","year":"2021","journal-title":"Principles of Abstract Interpretation, Vol. 1"},{"key":"B19","first-page":"238","article-title":"\u201cAbstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints,\u201d","volume-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, POPL '77","author":"Cousot","year":"1977"},{"key":"B20","first-page":"269","article-title":"\u201cSystematic design of program analysis frameworks,\u201d","volume-title":"Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '79","author":"Cousot","year":"1979"},{"key":"B21","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-45937-5_13","article-title":"\u201cModular static program analysis,\u201d","author":"Cousot","year":"2002","journal-title":"Compiler Construction, Vol. 2304"},{"key":"B22","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-77505-8_23","article-title":"\u201cCombination of abstractions in the ASTR\u00c9E static analyzer,\u201d","author":"Cousot","year":"2007","journal-title":"Advances in Computer Science"},{"key":"B23","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/512760.512770","article-title":"\u201cAutomatic discovery of linear restraints among variables of a program,\u201d","author":"Cousot","year":"1978","journal-title":"POPL '78"},{"key":"B24","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1145\/2676726.2676986","article-title":"\u201cAbstract symbolic automata: Mixed syntactic\/semantic similarity analysis of executables,\u201d","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Dalla Preda","year":"2015"},{"key":"B25","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-642-35873-9_14","article-title":"\u201cStatic analysis of string encoders and decoders,\u201d","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"D'Antoni","year":"2013"},{"key":"B26","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-662-48899-7_10","article-title":"\u201cBoolean formulas for the static identification of injection attacks in java,\u201d","author":"Ernst","year":"2015","journal-title":"Logic for Prog., Art. Int"},{"key":"B27","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.tcs.2016.04.001","article-title":"A generic framework for heap and value analyses of object-oriented programming languages","volume":"631","author":"Ferrara","year":"2016","journal-title":"Theor. Comput. Sci"},{"key":"B28","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1145\/1133255.1134026","article-title":"Combining abstract interpreters","volume":"41","author":"Gulwani","year":"2006","journal-title":"ACM SIGPLAN Notices"},{"key":"B29","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1109\/SSNE.2011.9","article-title":"\u201cStatic analysis of format string vulnerabilities,\u201d","volume-title":"2011 First ACIS International Symposium on Software and Network Engineering","author":"Han","year":"2011"},{"key":"B30","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","article-title":"\u201cApron: a library of numerical abstract domains for static analysis,\u201d","author":"Jeannet","year":"2009","journal-title":"Computer Aided Verification, Vol. 5643"},{"key":"B31","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1145\/2775051.2676966","article-title":"A formally-verified c static analyzer","volume":"50","author":"Jourdan","year":"2015","journal-title":"ACM Sigplan Notices"},{"key":"B32","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-642-18275-4_21","article-title":"\u201cString analysis as an abstract interpretation,\u201d","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"Kim","year":"2011"},{"key":"B33","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1145\/2786805.2786879","article-title":"\u201cString analysis for java and android applications,\u201d","volume-title":"Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering","author":"Li","year":"2015"},{"key":"B34","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1016\/j.scico.2009.04.004","article-title":"Pentagons: a weakly relational abstract domain for the efficient validation of array accesses","volume":"75","author":"Logozzo","year":"2010","journal-title":"Sci. Comput. Program"},{"key":"B35","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-54807-9_12","article-title":"\u201cString analysis for dynamic field access,\u201d","author":"Madsen","year":"2014","journal-title":"Compiler Construction"},{"key":"B36","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"High. Order Symb. Comp"},{"key":"B37","first-page":"267","article-title":"\u201cTwinning automata and regular expressions for string static analysis,\u201d","volume-title":"Proc. of VMCAI '21, Volume 12597 of LNCS","author":"Negrini","year":"2021"},{"key":"B38","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-981-19-9601-6_2","article-title":"\u201cLiSA: a generic framework for multilanguage static analysis,\u201d","author":"Negrini","year":"","journal-title":"Challenges of Software Verification"},{"key":"B39","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1145\/3689609.3689995","article-title":"\u201cStability: an abstract domain for the trend of variation of numerical variables,\u201d","volume-title":"Proceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains, NSAD '24","author":"Negrini","year":"2024"},{"key":"B40","first-page":"8","article-title":"\u201cStatic analysis of data transformations in jupyter notebooks,\u201d","volume-title":"Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2023","author":"Negrini","year":""},{"key":"B41","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1109\/ASE.2011.6100047","article-title":"\u201cAuto-locating and fix-propagating for html validation errors to php server-side code,\u201d","volume-title":"2011 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2011)","author":"Nguyen","year":"2011"},{"key":"B42","first-page":"1","article-title":"\u201cInformation flow analysis for detecting non-determinism in blockchain,'","volume":"23","author":"Olivieri","year":"2023","journal-title":"37th European Conference on Object-Oriented' Programming (ECOOP 2023), Volume 263 of Leibniz International Proceedings in Informatics (LIPIcs)"},{"key":"B43","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/2989225.2989228","article-title":"\u201cPrecise and scalable static analysis of jquery using a regular expression domain,\u201d","volume-title":"Proceedings of the 12th Symposium on Dynamic Languages","author":"Park","year":"2016"},{"key":"B44","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","article-title":"Classes of recursively enumerable sets and their decision problems","volume":"74","author":"Rice","year":"1953","journal-title":"Trans. Am. Math. Soc"},{"key":"B45","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-642-39274-0_3","article-title":"\u201cApplications of symbolic finite automata,\u201d","volume-title":"Implementation and Application of Automata: 18th International Conference, CIAA 2013, Halifax, NS, Canada, July 16-19, 2013. Proceedings 18","author":"Veanes","year":"2013"},{"key":"B46","first-page":"623","article-title":"\u201cA symbolic model checking approach to the analysis of string and length constraints,\u201d","volume-title":"Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE '18","author":"Wang","year":"2018"},{"key":"B47","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/s10703-013-0189-1","article-title":"Automata-based symbolic string analysis for vulnerability detection","volume":"44","author":"Yu","year":"2014","journal-title":"Form. Methods Syst. Des"},{"key":"B48","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-540-85114-1_21","article-title":"\u201cSymbolic string verification: an automata-based approach,\u201d","volume-title":"International SPIN Workshop on Model Checking of Software","author":"Yu","year":"2008"},{"key":"B49","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/s10009-024-00777-8","article-title":"Inference of access policies through static analysis","volume":"26","author":"Zanatta","year":"2025","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"B50","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/2491411.2491456","article-title":"\u201cZ3-str: a z3-based string solver for web application analysis,\u201d","volume-title":"Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering","author":"Zheng","year":"2013"}],"container-title":["Frontiers in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/fcomp.2025.1655377\/full","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T13:30:56Z","timestamp":1768915856000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/fcomp.2025.1655377\/full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,20]]},"references-count":50,"alternative-id":["10.3389\/fcomp.2025.1655377"],"URL":"https:\/\/doi.org\/10.3389\/fcomp.2025.1655377","relation":{},"ISSN":["2624-9898"],"issn-type":[{"value":"2624-9898","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,20]]},"article-number":"1655377"}}