{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:40:45Z","timestamp":1725565245220},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223818"},{"type":"electronic","value":"9783540278153"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27815-3_22","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T00:32:16Z","timestamp":1284424336000},"page":"258-273","source":"Crossref","is-referenced-by-count":15,"title":["Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs"],"prefix":"10.1007","author":[{"given":"Bertrand","family":"Jeannet","sequence":"first","affiliation":[]},{"given":"Wendelin","family":"Serwe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"22_CR2","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/604131.604137","volume-title":"POPL 2003","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL 2003, pp. 62\u201373. ACM, New York (2003)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0024192","volume-title":"Programming Language Implementation and Logic Programming","author":"F. Bourdoncle","year":"1990","unstructured":"Bourdoncle, F.: Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In: Deransart, P., Ma\u0142uszy\u0144ski, J. (eds.) PLILP 1990. LNCS, vol.\u00a0456, pp. 307\u2013323. Springer, Heidelberg (1990)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/3-540-57209-0_33","volume-title":"Software Engineering - ESEC \u201993","author":"F. Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Assertion-based debugging of imperative programs by abstract interpretation. In: Sommerville, I., Paul, M. (eds.) ESEC 1993. LNCS, vol.\u00a0717, pp. 501\u2013516. Springer, Heidelberg (1993)"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"POPL 1977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238\u2013252. ACM, New York (1977)"},{"key":"22_CR6","first-page":"237","volume-title":"Formal Description of Programming Concepts","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Formal Description of Programming Concepts, pp. 237\u2013277. North Holland, Amsterdam (1977)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming\u00a013(2\u20133) (1992)","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"22_CR8","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/512760.512770","volume-title":"POPL 1978","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84\u201397. ACM, New York (1978)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Creusillet, B., Irigoin, F.: Interprocedural array region analyses. International Journal of Parallel Programming, 24(6) (1996)","DOI":"10.1007\/BF03356758"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1145\/178243.178263","volume-title":"PLDI 1994","author":"A. Deutsch","year":"1994","unstructured":"Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: PLDI 1994, pp. 230\u2013241. ACM, New York (1994)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural dataflow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 14\u201330. Springer, Heidelberg (1999)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/3-540-47764-0_24","volume-title":"Static Analysis","author":"J. Feret","year":"2001","unstructured":"Feret, J.: Abstract interpretation-based static analysis of mobile ambients. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 412\u2013430. Springer, Heidelberg (2001)"},{"key":"22_CR14","unstructured":"Gaucher, F., Jahier, E., Jeannet, B., Maraninchi, F.: Automatic state reaching for debugging reactive programs. In: AADEBUG 2003 (2003)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Dynamic partitioning in linear relation analysis. Application to the verification of reactive systems. Formal Methods in System Design, 23(1) (2003)","DOI":"10.1023\/A:1024480913162"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. Research Report 4904, INRIA (July 2003)","DOI":"10.1007\/978-3-540-27815-3_22"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45315-6_17","volume-title":"Foundations of Software Science and Computation Structures","author":"T. Jensen","year":"2001","unstructured":"Jensen, T., Spoto, F.: Class analysis of object-oriented programs through abstract interpretation. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 261\u2013275. Springer, Heidelberg (2001)"},{"key":"22_CR18","volume-title":"POPL 1982","author":"N.D. Jones","year":"1982","unstructured":"Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: POPL 1982, ACM, New York (1982)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/3-540-55984-1_13","volume-title":"Compiler Construction","author":"J. Knoop","year":"1992","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol.\u00a0641, pp. 125\u2013140. Springer, Heidelberg (1992)"},{"key":"22_CR20","first-page":"310","volume-title":"AST 2001 in WCRE 2001","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310\u2013319. IEEE, Los Alamitos (2001)"},{"key":"22_CR21","unstructured":"Nielson, F.: Tensor products generalize the relational data flow analysis method. In: 4th Hungarian Computer Science Conference (1985)"},{"key":"22_CR22","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/199448.199462","volume-title":"POPL 1995","author":"T. Reps","year":"1995","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995, pp. 49\u201361. ACM, New York (1995)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_11","volume-title":"Static Analysis","author":"T. Reps","year":"2003","unstructured":"Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-45306-7_10","volume-title":"Compiler Construction","author":"N. Rinetzky","year":"2001","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol.\u00a02027, pp. 133\u2013149. Springer, Heidelberg (2001)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-40911-4_20","volume-title":"Integrated Formal Methods","author":"V. Rusu","year":"2000","unstructured":"Rusu, V., du Bousquet, L., J\u00e9ron, T.: An approach to symbolic test generation. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 338\u2013357. Springer, Heidelberg (2000)"},{"issue":"1\u20132","key":"22_CR26","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0304-3975(96)00072-2","volume":"167","author":"M. Sagiv","year":"1996","unstructured":"Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. TCS\u00a0167(1\u20132), 131\u2013170 (1996)","journal-title":"TCS"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM ToPLaS\u00a024(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"22_CR28","series-title":"ch.7","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications. ch.7, Prentice Hall, Englewood Cliffs (1981)"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27815-3_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:22:28Z","timestamp":1605741748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27815-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223818","9783540278153"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27815-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}