{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:01:19Z","timestamp":1781193679777,"version":"3.54.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_3","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:23Z","timestamp":1781192003000},"page":"48-69","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying a\u00a0Solver for\u00a0Mixed Flow-Sensitive Analyses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-9644-7475","authenticated-orcid":false,"given":"Sarah","family":"Tilscher","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-5821-6141","authenticated-orcid":false,"given":"Alexandra","family":"Gra\u00df","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2135-1593","authenticated-orcid":false,"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a Swiss army knife for program analysis. In: Jhala, R., Igarashi, A. (eds.) Programming Languages and Systems, pp. 157\u2013172, Springer Berlin Heidelberg, Berlin, Heidelberg (2012). ISBN 978-3-642-35182-2","DOI":"10.1007\/978-3-642-35182-2_12"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: Enhancing Top-Down Solving with Widening and Narrowing, pp. 272\u2013288. Springer International Publishing, Cham (2016). ISBN 978-3-319-27810-0, https:\/\/doi.org\/10.1007\/978-3-319-27810-0_14","DOI":"10.1007\/978-3-319-27810-0_14"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Types for Proofs and Programs, pp. 34\u201350, Springer Berlin Heidelberg, Berlin, Heidelberg (2004). ISBN 978-3-540-24849-1","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications, pp. 128\u2013141, Springer Berlin Heidelberg, Berlin, Heidelberg (1993). ISBN 978-3-540-48056-3","DOI":"10.1007\/BFb0039704"},{"key":"3_CR5","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: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252, POPL \u201977, Association for Computing Machinery, New York, NY, USA (1977). ISBN 9781450373500, https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"3_CR6","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/LOGCOM\/2.4.511","volume":"2","author":"P Cousot","year":"1992","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","journal-title":"J. Log. Comput."},{"key":"3_CR7","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":"3_CR8","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Karbyshev, A., Seidl, H.: Verifying a local generic solver in Coq. In: Cousot, R., Martel, M. (eds.) Static Analysis, pp. 340\u2013355, Springer Berlin Heidelberg, Berlin, Heidelberg (2010). ISBN 978-3-642-15769-1","DOI":"10.1007\/978-3-642-15769-1_21"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Karbyshev, A., Seidl, H.: What is a pure functional? In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf\u00a0der Heide, F., Spirakis, P.G. (eds.) Automata, Languages and Programming, pp. 199\u2013210, Springer Berlin Heidelberg, Berlin, Heidelberg (2010). ISBN 978-3-642-14162-1","DOI":"10.1007\/978-3-642-14162-1_17"},{"key":"3_CR10","unstructured":"Hofmann, M., Karbyshev, A., Seidl, H.: On the verification of local generic solvers. Tech. Rep. TUM-I1323 (2013)"},{"key":"3_CR11","unstructured":"Jourdan, J.: Verasco: a Formally Verified C Static Analyzer. (Verasco: un analyseur statique pour C formellement v\u00e9rifi\u00e9). Ph.D. thesis, Paris Diderot University, France (2016). https:\/\/tel.archives-ouvertes.fr\/tel-01327023"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 247\u2013259, POPL \u201915, Association for Computing Machinery, New York, NY, USA (2015). ISBN 9781450333009, https:\/\/doi.org\/10.1145\/2676726.2676966","DOI":"10.1145\/2676726.2676966"},{"key":"3_CR13","unstructured":"Karbyshev, A.: Monadic Parametricity of Second-Order Functionals. Ph.D. thesis, Technical University Munich (2013). https:\/\/nbn-resolving.org\/urn:nbn:de:bvb:91-diss-20130923-1144371-0-6"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"La\u00a0Spina, R., Demange, D., Blazy, S.: Formal verification of WTO-based dataflow solvers. In: Vafeiadis, V. (ed.) Programming Languages and Systems, pp. 91\u2013118, Springer Nature Switzerland, Cham (2025). ISBN 978-3-031-91121-7","DOI":"10.1007\/978-3-031-91121-7_4"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Lhot\u00e1k, O., Chung, K.C.A.: Points-to analysis with efficient strong updates. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 3\u201316, POPL \u201911, Association for Computing Machinery, New York, NY, USA (2011). ISBN 9781450304900,https:\/\/doi.org\/10.1145\/1926385.1926389","DOI":"10.1145\/1926385.1926389"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Midtgaard, J., Nielson, F., Nielson, H.R.: Iterated process analysis over lattice-valued regular expressions. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pp. 132\u2013145, PPDP \u201916, Association for Computing Machinery, New York, NY, USA (2016). ISBN 978145034148https:\/\/doi.org\/10.1145\/2967973.2968601","DOI":"10.1145\/2967973.2968601"},{"key":"3_CR17","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":"3_CR18","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 39\u201358, Springer Berlin Heidelberg, Berlin, Heidelberg (2014). ISBN 978-3-642-54013-4","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Static analysis of embedded real-time concurrent software with dynamic priorities. Electron. 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":"3_CR20","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) Foundations of Software Science and Computation Structures, pp. 347\u2013363, Springer Berlin Heidelberg, Berlin, Heidelberg (2001). ISBN 978-3-540-45315-4","DOI":"10.1007\/3-540-45315-6_23"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Abstract interpretation of annotated commands. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, pp. 116\u2013132, Springer Berlin Heidelberg, Berlin, Heidelberg (2012). ISBN 978-3-642-32347-8","DOI":"10.1007\/978-3-642-32347-8_9"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Klein, G.: Abstract Interpretation, pp. 219\u2013280. Springer International Publishing, Cham (2014). ISBN 978-3-319-10542-0, https:\/\/doi.org\/10.1007\/978-3-319-10542-0_13","DOI":"10.1007\/978-3-319-10542-0_13"},{"key":"3_CR23","doi-asserted-by":"crossref","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.) Static Analysis, pp. 359\u2013383, Springer International Publishing, Cham (2021). ISBN 978-3-030-88806-0","DOI":"10.1007\/978-3-030-88806-0_18"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V.: Clustered relational thread-modular abstract interpretation with local traces. In: Wies, T. (ed.) Programming Languages and Systems, pp. 28\u201358, Springer Nature Switzerland, Cham (2023). ISBN 978-3-031-30044-8","DOI":"10.1007\/978-3-031-30044-8_2"},{"issue":"9","key":"3_CR25","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":"3_CR26","unstructured":"Stade, Y., Tilscher, S., Seidl, H.: Partial correctness of the top-down solver. Archive of Formal Proofs (2024). ISSN 2150-914x, https:\/\/isa-afp.org\/entries\/Top_Down_Solver.html, Formal proof development"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Stade, Y., Tilscher, S., Seidl, H.: The top-down solver verified: Building confidence in static analyzers. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 303\u2013324, Springer Nature Switzerland, Cham (2024). ISBN 978-3-031-65627-9","DOI":"10.1007\/978-3-031-65627-9_15"},{"key":"3_CR28","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 (2025). https:\/\/doi.org\/10.1145\/3729297PLDI","DOI":"10.1145\/3729297PLDI"},{"key":"3_CR29","doi-asserted-by":"publisher","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","DOI":"10.1016\/J.JSS.2018.10.001"},{"key":"3_CR30","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":"3_CR31","doi-asserted-by":"publisher","unstructured":"Tilscher, S., Gra\u00df, A., Seidl, H.: Isabelle\/HOL formalization for \u2018Verifying a solver for mixed flow-sensitive analyses\u2019 (2026). https:\/\/doi.org\/10.5281\/zenodo.19259983","DOI":"10.5281\/zenodo.19259983"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Tilscher, S., Stade, Y., Schwarz, M., Vogler, R., Seidl, H.: The top-down solver\u2014an exercise in A2I. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds.) Challenges of Software Verification, vol. 238, pp. 157\u2013179, Springer Nature Singapore, Singapore (2023). https:\/\/doi.org\/10.1007\/978-981-19-9601-6_9","DOI":"10.1007\/978-981-19-9601-6_9"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"de\u00a0Vilhena, P.E., Pottier, F., Jourdan, J.H.: Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371101","DOI":"10.1145\/3371101"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:27Z","timestamp":1781192007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_3","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":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}