{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:08:07Z","timestamp":1746194887121},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642197178"},{"type":"electronic","value":"9783642197185"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19718-5_24","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T10:17:15Z","timestamp":1300097835000},"page":"459-479","source":"Crossref","is-referenced-by-count":6,"title":["Precise Interprocedural Analysis in the Presence of Pointers to the Stack"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Sotin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Jeannet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Andersen, L.: Program Analysis and Specialization for the C Programming Language. Ph.D. thesis (1994), \n                  \n                    http:\/\/ftp.diku.dk\/pub\/diku\/semantics\/papers\/D-203.dvi.Z"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (1990)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009 (2009)","DOI":"10.1145\/1640089.1640108"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: Prog. Lang. Design and Implementation, PLDI 1990 (1990)","DOI":"10.1145\/93542.93585"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, R., Ryder, B.G., Landi, W.: Relevant context inference. In: Principles of Prog. Languages, POPL 1999 (1999)","DOI":"10.1145\/292540.292554"},{"key":"24_CR6","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: Principles of Prog. Languages, POPL 1977 (1977)","DOI":"10.1145\/512950.512973"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conf. on Formal Description of Programming Concepts (1977)","DOI":"10.1145\/800022.808314"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Why does astr\u00e9e scale up? Formal Methods in System Design\u00a035(3) (2009)","DOI":"10.1007\/s10703-009-0089-6"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-04570-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"D. Delmas","year":"2009","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an industrial use of fluctuat on safety-critical avionics softwar. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol.\u00a05825, pp. 53\u201369. Springer, Heidelberg (2009)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"24_CR11","volume-title":"Prog. Lang. Design and Implementation, PLDI 2008","author":"N. Halbwachs","year":"2008","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: Prog. Lang. Design and Implementation, PLDI 2008. ACM, New York (2008)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Heintze, N., Tardieu, O.: Demand-driven pointer analysis. In: Prog. Lang. Design and Implementation, PLDI 2001 (2001)","DOI":"10.1145\/378795.378802"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: Prog. Analysis For Software Tools and Engineering, PASTE 2001 (2001)","DOI":"10.1145\/379605.379665"},{"key":"24_CR14","unstructured":"Jeannet, B.: The BDDAPRON logico-numerical abstract domains library, \n                  \n                    http:\/\/www.inrialpes.fr\/pop-art\/people\/bjeannet\/bjeannet-forge\/bddapron\/"},{"key":"24_CR15","volume-title":"Software Engineering and Formal Methods, SEFM 2009","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B.: Relational interprocedural verification of concurrent programs. In: Software Engineering and Formal Methods, SEFM 2009. IEEE, Los Alamitos (2009)"},{"key":"24_CR16","unstructured":"Jeannet, B., Argoud, M., Lalire, G.: The Interproc interprocedural analyzer, \n                  \n                    http:\/\/pop-art.inrialpes.fr\/interproc\/interprocweb.cgi"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. ACM Trans. On Programming Languages and Systems (TOPLAS)\u00a032(2) (2010)","DOI":"10.1145\/1667048.1667050"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: APRON: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009), \n                  \n                    http:\/\/apron.cri.ensmp.fr\/library\/"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-27815-3_22","volume-title":"Algebraic Methodology and Software Technology","author":"B. Jeannet","year":"2004","unstructured":"Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 258\u2013273. Springer, Heidelberg (2004)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (1992)"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Landi, W., Ryder, B.G.: A safe approximate algorithm for interprocedural pointer aliasing. In: PLDI (1992)","DOI":"10.1145\/143095.143137"},{"key":"24_CR22","unstructured":"Midtgaard, J.: Control-flow analysis of functional programs. ACM Computing Surveys (2011); preliminary version available as BRICS technical report RS-07-18"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Languages, Compilers and Tools for Embedded Systems, LCTES 2006 (2006)","DOI":"10.1145\/1134650.1134659"},{"key":"24_CR24","unstructured":"Polyspace, \n                  \n                    http:\/\/www.mathworks.com\/products\/polyspace\/"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/11547662_20","volume-title":"Static Analysis","author":"N. Rinetzky","year":"2005","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural shape analysis for cutpoint-free programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 284\u2013302. Springer, Heidelberg (2005)"},{"key":"24_CR26","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.\u00a07. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"24_CR27","unstructured":"Somenzi, F.:Cudd: Colorado University Decision Diagram Package, \n                  \n                    ftp:\/\/vlsi.colorado.edu\/pub"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Sotin, P., Jeannet, B.: Precise interprocedural analysis in the presence of pointers to the stack (January 2011), \n                  \n                    http:\/\/hal.archives-ouvertes.fr\/inria-00547888\/fr\/","DOI":"10.1007\/978-3-642-19718-5_24"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to Analysis in Almost Linear Time. In: Principles of Prog. Languages, POPL 1996 (1996)","DOI":"10.1145\/237721.237727"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Prog. Lang. Design and Implementation, PLDI 2004 (2004)","DOI":"10.1145\/996841.996859"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for c programs. In: Prog. Lang. Design and Implementation, PLDI 1995 (1995)","DOI":"10.1145\/207110.207111"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19718-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T07:26:13Z","timestamp":1558423573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19718-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642197178","9783642197185"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19718-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}