{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:28:55Z","timestamp":1707521335950},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2016,4,20]],"date-time":"2016-04-20T00:00:00Z","timestamp":1461110400000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10009-016-0420-7","type":"journal-article","created":{"date-parts":[[2016,4,20]],"date-time":"2016-04-20T12:26:33Z","timestamp":1461155193000},"page":"565-584","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Underapproximation of procedure summaries for integer programs"],"prefix":"10.1007","volume":"19","author":[{"given":"Pierre","family":"Ganty","sequence":"first","affiliation":[]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[]},{"given":"Filip","family":"Kone\u010dn\u00fd","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,20]]},"reference":[{"key":"420_CR1","unstructured":"Lalire, G., Argoud, M., Jeannet, B.: Interproc. http:\/\/pop-art.inrialpes.fr\/people\/bjeannet\/bjeannet-forge\/interproc\/index.html"},{"key":"420_CR2","unstructured":"Atig, M.F., Ganty, P.: Approximating petri net reachability along context-free traces. In: FSTTCS\u201911, Volume\u00a013 of LIPIcs, pp. 152\u2013163. Schloss Dagstuhl, Wadern (2011)"},{"issue":"3","key":"420_CR3","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM 56(3), 16 (2009)","journal-title":"JACM"},{"key":"420_CR4","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems\u2014tool paper. In: FM 2012: Formal Methods, Volume 7436 of LNCS, pp. 247\u2013251. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-32759-9_21"},{"key":"420_CR5","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, Chapter\u00a07, pp. 189\u2013233. Prentice-Hall, Inc., Upper Saddle River (1981)"},{"issue":"6","key":"420_CR6","doi-asserted-by":"crossref","first-page":"33:1","DOI":"10.1145\/1857914.1857917","volume":"57","author":"J Esparza","year":"2010","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. JACM 57(6), 33:1\u201333:47 (2010)","journal-title":"JACM"},{"key":"420_CR7","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL\u201995, pp. 49\u201361. ACM, New York (1995)","DOI":"10.1145\/199448.199462"},{"key":"420_CR8","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI\u201912, Volume 7148 of LNCS, pp. 39\u201355. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"420_CR9","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL\u201910, pp. 43\u201356. ACM, New York (2010)","DOI":"10.1145\/1706299.1706307"},{"key":"420_CR10","doi-asserted-by":"crossref","unstructured":"Cook, A.P.B., Rybalchenko, A.: Summarization for termination: no return!. Formal Methods Syst. Design 35, 369\u2013387 (2009)","DOI":"10.1007\/s10703-009-0087-8"},{"key":"420_CR11","doi-asserted-by":"crossref","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. In: CAV\u201913: Proc. 23rd Int. Conf. on Computer Aided Verification, LNCS, pp. 381\u2013396. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_26"},{"key":"420_CR12","doi-asserted-by":"crossref","unstructured":"Latteux, M.: Mots infinis et langages commutatifs. Informatique Th\u00e9orique et Appl. 12(3), 185\u2013192 (1978)","DOI":"10.1051\/ita\/1978120301851"},{"key":"420_CR13","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF01744305","volume":"13","author":"M Luker","year":"1980","unstructured":"Luker, M.: Control sets on grammars using depth-first derivations. Math. Syst. Theory 13, 349\u2013359 (1980)","journal-title":"Math. Syst. Theory"},{"key":"420_CR14","volume-title":"The Mathematical Theory of Context-Free Languages","author":"S Ginsburg","year":"1966","unstructured":"Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill Inc, New York (1966)"},{"key":"420_CR15","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: CAV\u201910, Volume 6174 of LNCS, pp. 227\u2013242. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"420_CR16","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, University of Li\u00e8ge (1998)"},{"key":"420_CR17","doi-asserted-by":"crossref","unstructured":"Finkel, A., Leroux, J.: How to compose presburger-accelerations: applications to broadcast protocols. In: FSTTCS\u201902, Volume 2556 of LNCS, pp. 145\u2013156. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36206-1_14"},{"issue":"1","key":"420_CR18","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1016\/S0019-9958(78)91015-X","volume":"39","author":"M Luker","year":"1978","unstructured":"Luker, M.: A family of languages having only finite-index grammars. Inform. Control 39(1), 14\u201318 (1978)","journal-title":"Inform. Control"},{"key":"420_CR19","doi-asserted-by":"crossref","unstructured":"Godoy, G., Tiwari, A.: Invariant checking for programs with procedure calls. In: SAS\u201909, Volume 5673 of LNCS, pp. 326\u2013342. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03237-0_22"},{"key":"420_CR20","doi-asserted-by":"crossref","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: fast acceleration of symbolic transition systems. In: CAV\u201903, Volume 2725 of LNCS, pp. 118\u2013121. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_12"},{"issue":"2","key":"420_CR21","doi-asserted-by":"crossref","first-page":"275","DOI":"10.3233\/FI-2009-0044","volume":"91","author":"M Bozga","year":"2009","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae 91(2), 275\u2013303 (2009)","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"420_CR22","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/s10703-011-0136-y","volume":"40","author":"P Ganty","year":"2012","unstructured":"Ganty, P., Majumdar, R., Monmege, B.: Bounded underapproximations. Formal Methods Syst. Design 40(2), 206\u2013231 (2012)","journal-title":"Formal Methods Syst. Design"},{"key":"420_CR23","unstructured":"Termination Competition 2011. http:\/\/termcomp.uibk.ac.at\/termcomp\/home.seam"},{"key":"420_CR24","doi-asserted-by":"crossref","unstructured":"Cowles, J.: Knuth\u2019s generalization of mccarthy\u2019s 91 function. In: Computer-Aided Reasoning: ACL2 Case Studies, pp. 283\u2013299. Kluwer Academic Publishers, Berlin (2000)","DOI":"10.1007\/978-1-4757-3188-0_17"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0420-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0420-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0420-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0420-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,18]],"date-time":"2020-09-18T22:19:52Z","timestamp":1600467592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0420-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,20]]},"references-count":24,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["420"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0420-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,20]]}}}