{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:08Z","timestamp":1783545308752,"version":"3.55.0"},"publisher-location":"Cham","reference-count":79,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Flow-sensitive and flow-insensitive analyses of programs occupy opposite ends of a spectrum. Between these extremes lie\n                    <jats:italic>mixed flow sensitive<\/jats:italic>\n                    approaches, where some aspects of program behavior are analyzed flow-insensitively and others flow-sensitively. Mixed flow-sensitivity arises, for example, in the analysis of multi-threaded code or code withnon-local control flow. Another instance is global store widening for efficient analysis of functional languages and some forms of pointer analysis. While mixed flow-sensitive analyses are common in the literature, the formulation of the particular analysis problem and the means to solve it are often tightly coupled.\n                    <jats:italic>Side-effecting constraint systems<\/jats:italic>\n                    provide a generic mechanism for describing mixed flow-sensitive analyses, thus decoupling the analysis definition from solver algorithm details. The abstract interpreter\n                    <jats:sc>Goblint<\/jats:sc>\n                    realizes this decoupling, and allows defining mixed flow-sensitive analyses independently of generic solvers. We indicate how the precision of specified analyses can be improved using\n                    <jats:italic>digests<\/jats:italic>\n                    (on the side of the formulation of the analysis problem) and suitable update rules (on the side of the solver). We explain how developers can use\n                    <jats:sc>Goblint<\/jats:sc>\n                    to implement their own mixed flow-sensitive analyses.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_22","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:22:10Z","timestamp":1779024130000},"page":"446-470","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mixed Flow-Sensitive Static Analysis: Engineering Modularity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2135-1593","authenticated-orcid":false,"given":"Helmut","family":"Seidl","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4336-7980","authenticated-orcid":false,"given":"Vesal","family":"Vojdani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1729-3925","authenticated-orcid":false,"given":"Julian","family":"Erhard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9828-0308","authenticated-orcid":false,"given":"Michael","family":"Schwarz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Afonso, V., et al.: Going native: using a large-scale analysis of android apps to create a practical native-code sandboxing policy. In: 23rd Annual Network and Distributed System Security Symposium, NDSS 2016, The Internet Society (2016). https:\/\/doi.org\/10.14722\/ndss.2016.23384","DOI":"10.14722\/ndss.2016.23384"},{"key":"22_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/J.SCICO.2015.12.005","volume":"120","author":"G Amato","year":"2016","unstructured":"Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing. Sci. Comput. Program. 120, 1\u201324 (2016). https:\/\/doi.org\/10.1016\/J.SCICO.2015.12.005","journal-title":"Sci. Comput. Program."},{"key":"22_CR3","unstructured":"Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, University of Copenhagen (1994)"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a swiss army knife for program analysis. In: Programming Languages and Systems, pp. 157\u2013172, Springer Berlin Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_12","DOI":"10.1007\/978-3-642-35182-2_12"},{"issue":"8","key":"22_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3470569","volume":"64","author":"P Baudin","year":"2021","unstructured":"Baudin, P., et al.: The dogged pursuit of bug-free c programs: the Frama-c software analysis platform. Commun. ACM 64(8), 56\u201368 (2021). https:\/\/doi.org\/10.1145\/3470569","journal-title":"Commun. ACM"},{"key":"22_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proceeding TACAS\u00a0(3), pp. 151\u2013186, LNCS\u00a015698, Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_9","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-52234-0_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Blazy","year":"2017","unstructured":"Blazy, S., B\u00fchler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112\u2013130. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_7"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: Proceeding of the 24th Annual ACM SIGPLAN Conf. on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, October 25\u201329, 2009, Orlando, Florida, USA, pp. 243\u2013262, ACM (2009). https:\/\/doi.org\/10.1145\/1640089.1640108","DOI":"10.1145\/1640089.1640108"},{"issue":"OOPSLA2","key":"22_CR9","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1145\/3622833","volume":"7","author":"Y Cai","year":"2023","unstructured":"Cai, Y., Zhang, C.: A cocktail approach to practical call graph construction. Proc. ACM Program. Lang. 7(OOPSLA2), 1001\u20131033 (2023). https:\/\/doi.org\/10.1145\/3622833","journal-title":"Proc. ACM Program. Lang."},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. In: Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, EPTCS, vol. 129, pp. 325\u2013336 (2013). https:\/\/doi.org\/10.4204\/EPTCS.129.19","DOI":"10.4204\/EPTCS.129.19"},{"key":"22_CR11","unstructured":"Cousot, P.: Principles of abstract interpretation. MIT Press (2021)"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252, ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269\u2013282 (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"22_CR14","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511\u2013547 (1992). https:\/\/doi.org\/10.1093\/LOGCOM\/2.4.511","DOI":"10.1093\/LOGCOM\/2.4.511"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269\u2013295. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55844-6_142"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Cousot, P., et al.: The astr\u00e9e analyzer. In: Programming Languages and Systems (ESOP 2005), pp. 21\u201330, LNCS 3444. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: The reduced product of abstract domains and the combination of decision procedures. In: Foundations of Software Science and Computational Structures (FOSSACS 2011), pp. 456\u2013472, LNCS 6604. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_31","DOI":"10.1007\/978-3-642-19805-2_31"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Cousot, P., Giacobazzi, R., Ranzato, F.: A$${^2}$$i: abstract$${^2}$$ interpretation. Proc. ACM Program. Lang. 3(POPL), 42:1\u201342:31 (2019). https:\/\/doi.org\/10.1145\/3290355","DOI":"10.1145\/3290355"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/11823230_27","volume-title":"Static Analysis","author":"D Dhurjati","year":"2006","unstructured":"Dhurjati, D., Das, M., Yang, Y.: Path-sensitive dataflow analysis with iterative refinement. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 425\u2013442. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_27"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Erhard, J., et al.: Interactive abstract interpretation: reanalyzing multithreaded C programs for cheap. Int. J. Softw. Tools Technol. Transf. 26(6), 647\u2013667 (2024). https:\/\/doi.org\/10.1007\/S10009-024-00768-9","DOI":"10.1007\/S10009-024-00768-9"},{"issue":"2","key":"22_CR21","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/S10009-025-00803-3","volume":"27","author":"J Erhard","year":"2025","unstructured":"Erhard, J., Schinabeck, J.F., Schwarz, M., Seidl, H.: Context gas and friends: taming context-sensitivity on the fly. Int. J. Softw. Tools Technol. Transf. 27(2), 289\u2013307 (2025). https:\/\/doi.org\/10.1007\/S10009-025-00803-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"Erhard, J., Schwarz, M., Vojdani, V., Saan, S., Seidl, H.: When long jumps fall short: control-flow tracking and misuse detection for nonlocal jumps in C. Int. J. Softw. Tools Technol. Transf. 26(5), 589\u2013605 (2024). https:\/\/doi.org\/10.1007\/S10009-024-00764-Z","DOI":"10.1007\/S10009-024-00764-Z"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/11560548_26","volume-title":"Correct Hardware Design and Verification Methods","author":"C Ferdinand","year":"2005","unstructured":"Ferdinand, C., Heckmann, R.: Verifying timing behavior by abstract interpretation of executable code. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 336\u2013339. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560548_34"},{"key":"22_CR24","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Conf. Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, 16\u201318 January 2002, pp. 191\u2013202, ACM (2002). https:\/\/doi.org\/10.1145\/503272.503291","DOI":"10.1145\/503272.503291"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-38856-9_3","volume-title":"Static Analysis","author":"G Gange","year":"2013","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Abstract interpretation over non-lattice abstract domains. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 6\u201324. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_3"},{"issue":"1\u20132","key":"22_CR26","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/S0304-3975(98)00194-7","volume":"216","author":"R Giacobazzi","year":"1999","unstructured":"Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theor. Comput. Sci. 216(1\u20132), 159\u2013211 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00194-7","journal-title":"Theor. Comput. Sci."},{"key":"22_CR27","doi-asserted-by":"publisher","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI \u201907, pp. 266\u2013277, ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250765","DOI":"10.1145\/1250734.1250765"},{"key":"22_CR28","doi-asserted-by":"publisher","unstructured":"Helm, D., K\u00fcbler, F., Reif, M., Eichberg, M., Mezini, M.: Modular collaborative program analysis in OPAL. In: ESEC\/FSE \u201920, pp. 184\u2013196, ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409765","DOI":"10.1145\/3368089.3409765"},{"issue":"1\u20132","key":"22_CR29","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1017\/S1471068411000457","volume":"12","author":"MV Hermenegildo","year":"2012","unstructured":"Hermenegildo, M.V., et al.: An overview of ciao and its design philosophy. Theory Pract. Log. Program. 12(1\u20132), 219\u2013252 (2012). https:\/\/doi.org\/10.1017\/S1471068411000457","journal-title":"Theory Pract. Log. Program."},{"issue":"1","key":"22_CR30","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.scico.2005.02.006","volume":"58","author":"MV Hermenegildo","year":"2005","unstructured":"Hermenegildo, M.V., Puebla, G., Bueno, F., L\u00f3pez-Garc\u00eda, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Sci. Comput. Program. 58(1), 115\u2013140 (2005). https:\/\/doi.org\/10.1016\/j.scico.2005.02.006","journal-title":"Sci. Comput. Program."},{"key":"22_CR31","doi-asserted-by":"publisher","unstructured":"Horn, D.V., Might, M.: Abstracting abstract machines. In: SIGPLAN International Conference on Functional Programming, pp. 51\u201362, ACM (2010). https:\/\/doi.org\/10.1145\/1863543.1863553","DOI":"10.1145\/1863543.1863553"},{"issue":"4\u20135","key":"22_CR32","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1017\/S0956796812000238","volume":"22","author":"DV Horn","year":"2012","unstructured":"Horn, D.V., Might, M.: Systematic abstraction of abstract machines. J. Funct. Program. 22(4\u20135), 705\u2013746 (2012). https:\/\/doi.org\/10.1017\/S0956796812000238","journal-title":"J. Funct. Program."},{"key":"22_CR33","doi-asserted-by":"publisher","unstructured":"Journault, M., Min\u00e9, A., Monat, R., Ouadjaout, A.: Combinations of reusable abstract domains for a multilingual static analyzer. In: Proceeding of VSTTE 2019, pp. 1\u201318, LNCS 12031. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_1","DOI":"10.1007\/978-3-030-41600-3_1"},{"key":"22_CR34","doi-asserted-by":"publisher","unstructured":"Keidel, S., Helm, D., Roth, T., Mezini, M.: A modular soundness theory for the blackboard analysis architecture. In: Programming Languages and Systems, pp. 361\u2013390, LNCS 14577. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57267-8_14","DOI":"10.1007\/978-3-031-57267-8_14"},{"key":"22_CR35","doi-asserted-by":"publisher","unstructured":"Kim, S., Rival, X., Ryu, S.: A theoretical foundation of sensitivity in an abstract interpretation framework. ACM Trans. Program. Lang. Syst. 40(3), 13:1\u201313:44 (2018). https:\/\/doi.org\/10.1145\/3230624","DOI":"10.1145\/3230624"},{"key":"22_CR36","doi-asserted-by":"publisher","unstructured":"Ko\u00e7al, A.R., Schwarz, M., Saan, S., Seidl, H.: Same engine, multiple gears: parallelizing fixpoint iteration at different granularities. In: Proceeding TACAS 2026, Lecture Notes in Computer Science (2026). https:\/\/doi.org\/10.1007\/978-3-032-22749-2_9","DOI":"10.1007\/978-3-032-22749-2_9"},{"key":"22_CR37","unstructured":"Le\u00a0Charlier, B., Van\u00a0Hentenryck, P.: A Universal top-down fixpoint algorithm. Technical Report CS-92-25, Brown University (1992)"},{"key":"22_CR38","doi-asserted-by":"publisher","unstructured":"Lermusiaux, P., Montagu, B.: Detection of uncaught exceptions in functional programs by abstract interpretation. In: European Symposium on Programming, pp. 391\u2013420, LNCS 14577, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57267-8_15","DOI":"10.1007\/978-3-031-57267-8_15"},{"key":"22_CR39","doi-asserted-by":"publisher","unstructured":"Lhot\u00e1k, O., Chung, K.A.: Points-to analysis with efficient strong updates. In: Proceeding of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 3\u201316, ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926389","DOI":"10.1145\/1926385.1926389"},{"key":"22_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-642-54833-8_27","volume-title":"Programming Languages and Systems","author":"R Mangal","year":"2014","unstructured":"Mangal, R., Naik, M., Yang, H.: A correspondence between two approaches to interprocedural analysis in the presence of join. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 513\u2013533. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_27"},{"key":"22_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-49051-7_5","volume-title":"Compiler Construction","author":"F Martin","year":"1999","unstructured":"Martin, F.: Experimental Comparison of Call String and Functional Approaches to Interprocedural Analysis. In: J\u00e4hnichen, S. (ed.) CC 1999. LNCS, vol. 1575, pp. 63\u201375. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-540-49051-7_5"},{"key":"22_CR42","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Log. Methods Comput. Sci. 8(1) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:26)2012","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"22_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-54013-4_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2014","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39\u201358. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_3"},{"key":"22_CR44","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Static analysis of embedded real-time concurrent software with dynamic priorities. Electr. Notes Theor. Comput. Sci. 331, 3\u201339 (2017). https:\/\/doi.org\/10.1016\/j.entcs.2017.02.002","DOI":"10.1016\/j.entcs.2017.02.002"},{"key":"22_CR45","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang. 4(3-4), 120\u2013372 (2017). https:\/\/doi.org\/10.1561\/2500000034","DOI":"10.1561\/2500000034"},{"key":"22_CR46","unstructured":"Montagu, B.: The design and implementation of an abstract interpreter for OCAML programs. In: ML Family 2023-Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop, pp. 1\u20134 (2023)"},{"key":"22_CR47","doi-asserted-by":"publisher","unstructured":"Munier, P.: Polyspace. In: Industrial Use of Formal Methods, pp. 123\u2013153, Wiley (2012). https:\/\/doi.org\/10.1002\/9781118561829.ch4","DOI":"10.1002\/9781118561829.ch4"},{"key":"22_CR48","unstructured":"Muthukumar, K., Hermenegildo, M.: Determination of variable dependence information at compile-time through abstract interpretation. In: North American Conference on Logic Programming, pp. 166\u2013189, MIT Press (1989)"},{"key":"22_CR49","unstructured":"Muthukumar, K., Hermenegildo, M.: Deriving a fixpoint computation algorithm for top-down abstract interpretation of logic programs. Technical Report ACT-DC-153-90, MCC (1990)"},{"key":"22_CR50","doi-asserted-by":"publisher","unstructured":"Negrini, L., Ferrara, P., Arceri, V., Cortesi, A.: Lisa: a generic framework for multilanguage static analysis. In: Challenges of Software Verification, Intelligent Systems Reference Library, vol. 238, pp. 19\u201342. Springer (2023). https:\/\/doi.org\/10.1007\/978-981-19-9601-6_2","DOI":"10.1007\/978-981-19-9601-6_2"},{"key":"22_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-030-11245-5_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Nicolay","year":"2019","unstructured":"Nicolay, J., Sti\u00e9venart, Q., De Meuter, W., De Roover, C.: Effect-driven flow analysis. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 247\u2013274. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_12"},{"key":"22_CR52","doi-asserted-by":"publisher","unstructured":"Park, J., Lee, H., Ryu, S.: A survey of parametric static analysis. ACM Comput. Surv. 54(7), 149:1\u2013149:37 (2022). https:\/\/doi.org\/10.1145\/3464457","DOI":"10.1145\/3464457"},{"key":"22_CR53","doi-asserted-by":"publisher","unstructured":"Rinetzky, N., Ramalingam, G., Sagiv, S., Yahav, E.: On the complexity of partially-flow-sensitive alias analysis. ACM Trans. Program. Lang. Syst. 30(3), 13:1\u201313:28 (2008). https:\/\/doi.org\/10.1145\/1353445.1353447","DOI":"10.1145\/1353445.1353447"},{"issue":"5","key":"22_CR54","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5), 26 (2007). https:\/\/doi.org\/10.1145\/1275497.1275501","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR55","unstructured":"Rival, X., Yi, K.: Introduction to static analysis: an abstract interpretation perspective. MIT Press (2020)"},{"key":"22_CR56","doi-asserted-by":"publisher","unstructured":"Roth, T., Helm, D., Reif, M., Mezini, M.: Cifi: versatile analysis of class and field immutability. In: 36th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2021, pp. 979\u2013990, IEEE (2021). https:\/\/doi.org\/10.1109\/ASE51524.2021.9678903","DOI":"10.1109\/ASE51524.2021.9678903"},{"key":"22_CR57","doi-asserted-by":"publisher","unstructured":"Roy, S., Srikant, Y.N.: Partial flow sensitivity. In: High Performance Computing - HIPC 2007, 14th International Conference Goa, India, 18\u201321 December 2007, Proceedings, pp. 245\u2013256, LNCS 4873. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-77220-0_25","DOI":"10.1007\/978-3-540-77220-0_25"},{"key":"22_CR58","doi-asserted-by":"publisher","unstructured":"Saan, S., et al.: Goblint: a portfolio for mixed flow-sensitive abstract interpretation (competition contribution). In: Proceeding TACAS 2026, Lecture Notes in Computer Science (2026). https:\/\/doi.org\/10.1007\/978-3-032-22749-2_26","DOI":"10.1007\/978-3-032-22749-2_26"},{"key":"22_CR59","doi-asserted-by":"publisher","unstructured":"Santos, J.C.S., Dolby, J.: Program analysis using WALA (tutorial). In: Proceeding of ESEC\/FSE 2022, pp. 1819\u20131819, ESEC\/FSE \u201922, ACM (2022). https:\/\/doi.org\/10.1145\/3540250.3569449","DOI":"10.1145\/3540250.3569449"},{"key":"22_CR60","unstructured":"Schwarz, M.: Thread-modular abstract interpretation: the local perspective. Ph.D. Thesis, Technical University of Munich (2025)"},{"issue":"6","key":"22_CR61","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/S10009-024-00773-Y","volume":"26","author":"M Schwarz","year":"2024","unstructured":"Schwarz, M., Erhard, J.: The digest framework: concurrency-sensitivity for abstract interpretation. Int. J. Softw. Tools Technol. Transf. 26(6), 727\u2013746 (2024). https:\/\/doi.org\/10.1007\/S10009-024-00773-Y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"22_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-030-88806-0_18","volume-title":"Static Analysis","author":"M Schwarz","year":"2021","unstructured":"Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V.: Improving thread-modular abstract interpretation. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) SAS 2021. LNCS, vol. 12913, pp. 359\u2013383. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_18"},{"key":"22_CR63","doi-asserted-by":"publisher","unstructured":"Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V.: Clustered relational thread-modular abstract interpretation with local traces. In: European Symposium on Programming, pp. 28\u201358, LNCS 13990. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_2","DOI":"10.1007\/978-3-031-30044-8_2"},{"key":"22_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-030-41103-9_5","volume-title":"From Lambda Calculus to Cybersecurity Through Program Analysis","author":"H Seidl","year":"2020","unstructured":"Seidl, H., Erhard, J., Vogler, R.: Incremental abstract interpretation. In: Di Pierro, A., Malacaria, P., Nagarajan, R. (eds.) From Lambda Calculus to Cybersecurity Through Program Analysis. LNCS, vol. 12065, pp. 132\u2013148. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41103-9_5"},{"key":"22_CR65","doi-asserted-by":"crossref","unstructured":"Seidl, H., Vene, V., M\u00fcller-Olm, M.: Global invariants for analysing multi-threaded applications. In: Proceeding\u2013Estonian Academy Of Sciences Physics Mathematics, vol.\u00a052, pp. 413\u2013436, Estonian Academy Publishers (2003)","DOI":"10.3176\/phys.math.2003.4.05"},{"issue":"9","key":"22_CR66","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1017\/S0960129521000499","volume":"31","author":"H Seidl","year":"2021","unstructured":"Seidl, H., Vogler, R.: Three improvements to the top-down solver. Math. Struct. Comput. Sci. 31(9), 1090\u20131134 (2021). https:\/\/doi.org\/10.1017\/S0960129521000499","journal-title":"Math. Struct. Comput. Sci."},{"key":"22_CR67","doi-asserted-by":"publisher","unstructured":"Seidl, H., Wilhelm, R., Hack, S.: Compiler design - analysis and transformation. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-17548-0","DOI":"10.1007\/978-3-642-17548-0"},{"key":"22_CR68","volume-title":"Two Approaches to Interprocedural Data Flow Analysis","author":"M Sharir","year":"1978","unstructured":"Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. New York University, Courant Institute of Mathematical Sciences (1978)"},{"key":"22_CR69","unstructured":"Shivers, O.G.: Control-flow analysis of higher-order languages or taming lambda. Ph.D. Thesis, Carnegie Mellon University (1991)"},{"issue":"OOPSLA2","key":"22_CR70","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/3689712","volume":"8","author":"J Simonnet","year":"2024","unstructured":"Simonnet, J., Lemerre, M., Sighireanu, M.: A dependent nominal physical type system for static analysis of memory in low level code. Proc. ACM Program. Lang. 8(OOPSLA2), 30\u201359 (2024). https:\/\/doi.org\/10.1145\/3689712","journal-title":"Proc. ACM Program. Lang."},{"key":"22_CR71","doi-asserted-by":"publisher","unstructured":"Stemmler, F., Schwarz, M., Erhard, J., Tilscher, S., Seidl, H.: Taking out the toxic trash: recovering precision in mixed flow-sensitive static analyses. Proc. ACM Program. Lang. 9(PLDI) (2025). https:\/\/doi.org\/10.1145\/3729297","DOI":"10.1145\/3729297"},{"key":"22_CR72","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/J.JSS.2018.10.001","volume":"147","author":"Q Sti\u00e9venart","year":"2019","unstructured":"Sti\u00e9venart, Q., Nicolay, J., de Meuter, W., de Roover, C.: A general method for rendering static analyses for diverse concurrency models modular. J. Syst. Softw. 147, 17\u201345 (2019). https:\/\/doi.org\/10.1016\/J.JSS.2018.10.001","journal-title":"J. Syst. Softw."},{"key":"22_CR73","doi-asserted-by":"publisher","unstructured":"Sui, Y., Xue, J.: On-demand strong update analysis via value-flow refinement. In: Proceeding of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE\u2019 2016, pp. 460\u2013473, ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950296","DOI":"10.1145\/2950290.2950296"},{"issue":"8","key":"22_CR74","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/tse.2018.2869336","volume":"46","author":"Y Sui","year":"2020","unstructured":"Sui, Y., Xue, J.: Value-flow-based demand-driven pointer analysis for C and C++. IEEE Trans. Software Eng. 46(8), 812\u2013835 (2020). https:\/\/doi.org\/10.1109\/tse.2018.2869336","journal-title":"IEEE Trans. Software Eng."},{"key":"22_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-030-02768-1_6","volume-title":"Programming Languages and Systems","author":"T Suzanne","year":"2018","unstructured":"Suzanne, T., Min\u00e9, A.: Relational thread-modular abstract interpretation under relaxed memory models. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 109\u2013128. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_6"},{"key":"22_CR76","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-024-00762-1","volume":"26","author":"ST Taft","year":"2024","unstructured":"Taft, S.T.: Sound and precise static analysis using a generalization of static single assignment and value numbering. Int. J. Softw. Tools Technol. Transfer 26, 621\u2013632 (2024). https:\/\/doi.org\/10.1007\/s10009-024-00762-1","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"22_CR77","doi-asserted-by":"crossref","unstructured":"Tilscher, S., Gra\u00df, A., Seidl, H.: Verifying a solver for mixed flow-sensitive analyses. In: NASA Formal Methods Symposium, Lecture Notes in Computer Science (2026)","DOI":"10.1007\/978-3-032-28079-4_3"},{"key":"22_CR78","doi-asserted-by":"publisher","unstructured":"Tilscher, S., Stade, Y., Schwarz, M., Vogler, R., Seidl, H.: The top-down solver - an exercise in a$$ ^{\\text{2}}$$i. In: Challenges of Software Verification, Intelligent Systems Reference Library, vol. 238, pp. 157\u2013179. Springer (2023). https:\/\/doi.org\/10.1007\/978-981-19-9601-6_9","DOI":"10.1007\/978-981-19-9601-6_9"},{"key":"22_CR79","doi-asserted-by":"publisher","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the goblint approach. In: 31st IEEE\/ACM International Conference on Automated Software Engineering, pp. 391\u2013402, ACM (2016). https:\/\/doi.org\/10.1145\/2970276.2970337","DOI":"10.1145\/2970276.2970337"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:41Z","timestamp":1783542581000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":79,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}