{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:09:11Z","timestamp":1743127751626,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":29,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789811996009"},{"type":"electronic","value":"9789811996016"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-981-19-9601-6_9","type":"book-chapter","created":{"date-parts":[[2023,7,24]],"date-time":"2023-07-24T16:02:22Z","timestamp":1690214542000},"page":"157-179","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The Top-Down Solver\u2014An Exercise in $$\\text {A}^{2}$$I"],"prefix":"10.1007","author":[{"given":"Sarah","family":"Tilscher","sequence":"first","affiliation":[]},{"given":"Yannick","family":"Stade","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Schwarz","sequence":"additional","affiliation":[]},{"given":"Ralf","family":"Vogler","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,22]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: A swiss army knife for program analysis. In: R.\u00a0Jhala, A.\u00a0Igarashi (eds.) Programming Languages and Systems - 10th Asian Symposium, APLAS 2012. Proceedings, LNCS, vol. 7705, pp. 157\u2013172. Springer (2012)","DOI":"10.1007\/978-3-642-35182-2_12"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: Enhancing top-down solving with widening and narrowing. In: C.W. Probst, C.\u00a0Hankin, R.R. Hansen (eds.) Semantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, LNCS, vol. 9560, pp. 272\u2013288. Springer (2016)","DOI":"10.1007\/978-3-319-27810-0_14"},{"issue":"8","key":"9_CR3","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3470569","volume":"64","author":"P Baudin","year":"2021","unstructured":"Baudin, P., Bobot, F., B\u00fchler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., Williams, N.: The dogged pursuit of bug-free C programs: the frama-c software analysis platform. Commun. ACM 64(8), 56\u201368 (2021).","journal-title":"Commun. ACM"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Blazy, S., B\u00fchler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: A.\u00a0Bouajjani, D.\u00a0Monniaux (eds.) Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings, LNCS, vol. 10145, pp. 112\u2013130. Springer (2017)","DOI":"10.1007\/978-3-319-52234-0_7"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: D.\u00a0Bj\u00f8rner, M.\u00a0Broy, I.V. Pottosin (eds.) Formal Methods in Programming and Their Applications, International Conference, 1993, Proceedings, LNCS, vol. 735, pp. 128\u2013141. Springer (1993)","DOI":"10.1007\/BFb0039704"},{"key":"9_CR6","unstructured":"Charlier, B.L., Van Hentenryck, P.: A universal top-down fixpoint algorithm. Tech. rep, Providence, RI, USA (1992)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Abstracting induction by extrapolation and interpolation. In: D.\u00a0D\u2019Souza, A.\u00a0Lal, K.G. Larsen (eds.) Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015. Proceedings, LNCS, vol. 8931, pp. 19\u201342. Springer (2015)","DOI":"10.1007\/978-3-662-46081-8_2"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: R.M. Graham, M.A. Harrison, R.\u00a0Sethi (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"9_CR9","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: E.J. Neuhold (ed.) Formal Description of Programming Concepts: Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts, 1977, pp. 237\u2013278. North-Holland (1977)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: A.V. Aho, S.N. Zilles, B.K. Rosen (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, 1979, pp. 269\u2013282. ACM Press (1979)","DOI":"10.1145\/567752.567778"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Comparing the galois connection and widening\/narrowing approaches to abstract interpretation. In: M.\u00a0Bruynooghe, M.\u00a0Wirsing (eds.) Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP\u201992, Proceedings, LNCS, vol. 631, pp. 269\u2013295. Springer (1992)","DOI":"10.1007\/3-540-55844-6_142"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The astre\u00e9 analyzer. In: S.\u00a0Sagiv (ed.) Programming Languages and Systems, 14th European Symposium on Programming,ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Proceedings, LNCS, vol. 3444, pp. 21\u201330. Springer (2005)","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Giacobazzi, R., Ranzato, F.: A$${^2}$$I: Abstract$${^2}$$ interpretation. Proc. ACM Program. Lang. 3(POPL), 42:1\u201342:31 (2019)","DOI":"10.1145\/3290355"},{"issue":"8","key":"9_CR14","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/3338112","volume":"62","author":"D Distefano","year":"2019","unstructured":"Distefano, D., F\u00e4hndrich, M., Logozzo, F., O\u2019Hearn, P.W.: Scaling static analyses at facebook. Commun. ACM 62(8), 62\u201370 (2019).","journal-title":"Commun. ACM"},{"issue":"2","key":"9_CR15","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0167-6423(99)00009-X","volume":"35","author":"C Fecht","year":"1999","unstructured":"Fecht, C., Seidl, H.: A faster solver for general systems of equations. Sci. Comput. Program. 35(2), 137\u2013161 (1999).","journal-title":"Sci. Comput. Program."},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"1685","DOI":"10.1016\/S0167-8191(00)00051-X","volume":"13\u201314","author":"M Hermenegildo","year":"2000","unstructured":"Hermenegildo, M.: Parallelizing irregular and pointer-based computations automatically: Perspectives from logic and constraint programming. Parallel Computing (13\u201314), 1685\u20131708 (2000).","journal-title":"Parallel Computing"},{"issue":"1\u20132","key":"9_CR17","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1017\/S1471068411000457","volume":"12","author":"MV Hermenegildo","year":"2012","unstructured":"Hermenegildo, M.V., Bueno, F., Carro, M., L\u00f3pez-Garc\u00eda, P., Mera, E., Morales, J.F., Puebla, G.: An overview of Ciao and its design philosophy. Theory Pract. Log. Program. 12(1\u20132), 219\u2013252 (2012).","journal-title":"Theory Pract. Log. Program."},{"issue":"1\u20132","key":"9_CR18","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). Science of Computer Programming 58(1\u20132), 115\u2013140 (2005).","journal-title":"Science of Computer Programming"},{"key":"9_CR19","unstructured":"Hofmann, M., Karbyshev, A., Seidl, H.: What is a pure functional? In: S.\u00a0Abramsky, C.\u00a0Gavoille, C.\u00a0Kirchner, F.M. auf\u00a0der Heide, P.G. Spirakis (eds.) Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Proceedings, Part II, LNCS, vol. 6199, pp. 199\u2013210. Springer (2010)"},{"key":"9_CR20","unstructured":"K.\u00a0Muthukumar, M.H.: 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":"9_CR21","doi-asserted-by":"crossref","unstructured":"K.\u00a0Muthukumar, M.H.: Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming 13(2\/3), 315\u2013347 (1992)","DOI":"10.1016\/0743-1066(92)90035-2"},{"key":"9_CR22","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":"9_CR23","doi-asserted-by":"crossref","unstructured":"K.S.\u00a0Henriksen, J.G.: Abstract interpretation of PIC programs through logic programming. In: SCAM, p. 184-196. IEEE Computer Society (2006)","DOI":"10.1109\/SCAM.2006.1"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"M.\u00a0Mendez-Lojo J.\u00a0Navas, M.H.: A flexible (C)LP-based approach to the analysis of object-oriented programs. In: LOPSTR, p. 154-168. LNCS 4915, Springer (2007)","DOI":"10.1007\/978-3-540-78769-3_11"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: A multilanguage static analysis of python programs with native C extensions. In: C.\u00a0Dragoi, S.\u00a0Mukherjee, K.S. Namjoshi (eds.) Static Analysis - 28th International Symposium, SAS 2021, Proceedings, Lecture Notes in Computer Science, vol. 12913, pp. 323\u2013345. Springer (2021)","DOI":"10.1007\/978-3-030-88806-0_16"},{"key":"9_CR26","unstructured":"Muthukumar, K., Hermenegildo, M.: Deriving a fixpoint computation algorithm for top-down abstract interpretation of logic programs. Tech. Rep. ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759 (1990)"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V.: Improving thread-modular abstract interpretation. In: C.\u00a0Dragoi, S.\u00a0Mukherjee, K.S. Namjoshi (eds.) Static Analysis - 28th International Symposium, SAS 2021, Proceedings, LNCS, vol. 12913, pp. 359\u2013383. Springer (2021)","DOI":"10.1007\/978-3-030-88806-0_18"},{"issue":"9","key":"9_CR28","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).","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the goblint approach. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016, pp. 391\u2013402. ACM (2016)","DOI":"10.1145\/2970276.2970337"}],"container-title":["Intelligent Systems Reference Library","Challenges of Software Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-19-9601-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,24]],"date-time":"2023-07-24T16:06:07Z","timestamp":1690214767000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-19-9601-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9789811996009","9789811996016"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-981-19-9601-6_9","relation":{},"ISSN":["1868-4394","1868-4408"],"issn-type":[{"type":"print","value":"1868-4394"},{"type":"electronic","value":"1868-4408"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}