{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:16Z","timestamp":1740122716606,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,8,3]],"date-time":"2017-08-03T00:00:00Z","timestamp":1501718400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10703-017-0288-5","type":"journal-article","created":{"date-parts":[[2017,8,3]],"date-time":"2017-08-03T09:38:01Z","timestamp":1501753081000},"page":"313-338","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Enforcing termination of interprocedural analysis"],"prefix":"10.1007","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3521-918X","authenticated-orcid":false,"given":"Stefan","family":"Schulze\u00a0Frielinghaus","sequence":"first","affiliation":[]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[]},{"given":"Ralf","family":"Vogler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,3]]},"reference":[{"key":"288_CR1","doi-asserted-by":"crossref","unstructured":"Alt M, Martin F (1995) Generation of efficient interprocedural analyzers with PAG. In: 2nd international symposium on static analysis (SAS), LNCS, vol 983, pp 33\u201350. Springer","DOI":"10.1007\/3-540-60360-3_31"},{"key":"288_CR2","doi-asserted-by":"crossref","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 (2016) Efficiently intertwining widening and narrowing. Sci Comput Program 120:1\u201324","journal-title":"Sci Comput Program"},{"key":"288_CR3","doi-asserted-by":"crossref","unstructured":"Apinis K, Seidl H, Vojdani V (2012) Side-effecting constraint systems: a swiss army knife for program analysis. In: 10th Asian symposium on programming languages and systems (APLAS), LNCS, vol 7705, Springer. pp 157\u2013172","DOI":"10.1007\/978-3-642-35182-2_12"},{"key":"288_CR4","doi-asserted-by":"crossref","unstructured":"Apinis K, Seidl H, Vojdani V (2013) How to combine widening and narrowing for non-monotonic systems of equations. In: 34th ACM SIGPLAN conference on programming language design and implementation (PLDI). ACM, pp 377\u2013386","DOI":"10.1145\/2491956.2462190"},{"key":"288_CR5","doi-asserted-by":"crossref","unstructured":"Apinis K, Seidl H, Vojdani V (2016) Enhancing top-down solving with widening and narrowing. In: Semantics, logics, and calculi\u2014essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays, LNCS, vol 9560, pp 272\u2013288. Springer","DOI":"10.1007\/978-3-319-27810-0_14"},{"issue":"1\u20132","key":"288_CR6","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R Bagnara","year":"2005","unstructured":"Bagnara R, Hill PM, Ricci E, Zaffanella E (2005) Precise widening operators for convex polyhedra. Sci Comput Program 58(1\u20132):28\u201356","journal-title":"Sci Comput Program"},{"key":"288_CR7","doi-asserted-by":"crossref","unstructured":"Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner D, Broy M, Pottosin IV (eds) Formal methods in programming and their applications, LNCS, vol 735. Springer, pp 128\u2013141","DOI":"10.1007\/BFb0039704"},{"key":"288_CR8","doi-asserted-by":"crossref","unstructured":"Chen L, Min\u00e9 A, Wang J, Cousot P (2010) An abstract domain to discover interval linear equalities. In: 11th international conference verification on model checking, and abstract interpretation (VMCAI), LNCS, vol 5944. Springer, pp 112\u2013128","DOI":"10.1007\/978-3-642-11319-2_11"},{"key":"288_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P (2015) Abstracting induction by extrapolation and interpolation. In: 16th International conference on verification, model checking, and abstract interpretation (VMCAI), LNCS, vol 8931. Springer, pp 19\u201342","DOI":"10.1007\/978-3-662-46081-8_2"},{"key":"288_CR10","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Fourth ACM symposium on principles of programming languages (POPL). ACM, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"288_CR11","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Static determination of dynamic properties of generalized type unions. In: ACM conference on language design for reliable software (LDRS), pp 77\u201394. ACM","DOI":"10.1145\/390017.808314"},{"key":"288_CR12","unstructured":"Cousot P, Cousot R (1977) Static determination of dynamic properties of recursive procedures. In: IFIP conference on formal description of programming concepts. North-Holland, pp 237\u2013277"},{"issue":"4","key":"288_CR13","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot P, Cousot R (1992) Abstract interpretation frameworks. J Log Comput 2(4):511\u2013547","journal-title":"J Log Comput"},{"issue":"3","key":"288_CR14","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P Cousot","year":"2009","unstructured":"Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Rival X (2009) Why does Astr\u00e9e scale up? Form Methods Syst Des 35(3):229\u2013264","journal-title":"Form Methods Syst Des"},{"key":"288_CR15","doi-asserted-by":"crossref","unstructured":"Fecht C, Seidl H (1996) An even faster solver for general systems of equations. In: Third international symposium on static analysis (SAS), LNCS, vol 1145. Springer, pp 189\u2013204","DOI":"10.1007\/3-540-61739-6_42"},{"key":"288_CR16","doi-asserted-by":"crossref","unstructured":"Gonnord L, Halbwachs N (2006) Combining widening and acceleration in linear relation analysis. In: 13th international symposium on static analysis (SAS), LNCS, vol 4134. Springer, pp 144\u2013160","DOI":"10.1007\/11823230_10"},{"issue":"1\u20132","key":"288_CR17","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1017\/S1471068411000457","volume":"12","author":"MV Hermenegildo","year":"2012","unstructured":"Hermenegildo MV, Bueno F, Carro M, L\u00f3pez-Garc\u00eda P, Mera E, Morales JF, Puebla G (2012) An overview of Ciao and its design philosophy. Theory Pract Log Program 12(1\u20132):219\u2013252","journal-title":"Theory Pract Log Program"},{"issue":"1\u20132","key":"288_CR18","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.scico.2005.02.006","volume":"58","author":"MV Hermenegildo","year":"2005","unstructured":"Hermenegildo MV, Puebla G, Bueno F, L\u00f3pez-Garc\u00eda P (2005) Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Sci Comput Program 58(1\u20132):115\u2013140","journal-title":"Sci Comput Program"},{"key":"288_CR19","doi-asserted-by":"crossref","unstructured":"Hofmann M, Karbyshev A, Seidl H (2010) Verifying a local generic solver in Coq. In: 17th international symposium on static analysis (SAS), LNCS, vol 6337. Springer, pp 340\u2013355","DOI":"10.1007\/978-3-642-15769-1_21"},{"key":"288_CR20","unstructured":"Hofmann M, Karbyshev A, Seidl H (2010) What is a pure functional? In: 37th international colloquium conference on automata, languages and programming (ICALP), LNCS, vol 6199. Springer, pp 199\u2013210"},{"key":"288_CR21","unstructured":"Karbyshev A (2013) Monadic parametricity of second-order functionals. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, September 2013"},{"issue":"3","key":"288_CR22","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1090\/S0002-9947-1937-1501929-X","volume":"42","author":"HM MacNeille","year":"1937","unstructured":"MacNeille HM (1937) Partially ordered sets. Trans Am Math Soc 42(3):416\u2013460","journal-title":"Trans Am Math Soc"},{"key":"288_CR23","unstructured":"Muthukumar K, Hermenegildo MV (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, April 1990"},{"key":"288_CR24","doi-asserted-by":"crossref","unstructured":"Schulze\u00a0Frielinghaus S, Seidl H, Vogler R (2016) Enforcing termination of interprocedural analysis. In: Rival X (eds) 23rd international symposium Static analysis (SAS), LNCS, vol 9837. Springer, pp 447\u2013468","DOI":"10.1007\/978-3-662-53413-7_22"},{"issue":"2","key":"288_CR25","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/S0743-1066(99)00058-8","volume":"43","author":"H Seidl","year":"2000","unstructured":"Seidl H, Fecht C (2000) Interprocedural analyses: a comparison. J Log Program 43(2):123\u2013156","journal-title":"J Log Program"},{"key":"288_CR26","first-page":"189","volume-title":"Program flow analysis: theory and application","author":"M Sharir","year":"1981","unstructured":"Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. In: Muchnick S, Jones N (eds) Program flow analysis: theory and application. Prentice-Hall, Englewood Cliffs, pp 189\u2013233"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0288-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0288-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0288-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T20:27:58Z","timestamp":1569961678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0288-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,3]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["288"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0288-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,8,3]]}}}