Abstract
This paper addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields – i.e., interprocedural shape analysis. It presents a way to harness some previously known approaches to interprocedural dataflow analysis – which in past work have been applied only to much less rich settings – for interprocedural shape analysis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst. 24, 217–298 (2002)
Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: European Symp. on Programming, pp. 380–398 (2003)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280–301 (2000)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E. (ed.) Formal Descriptions of Programming Concepts, IFIP WG 2.2, St. Andrews, Canada, August 1977, pp. 237–277. North-Holland, Amsterdam (1978)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, pp. 189–234. Prentice-Hall, Englewood Cliffs (1981)
Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Comp. Construct., pp. 125–140 (1992)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Princ. of Prog. Lang., pp. 49–61. ACM Press, New York (1995)
Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comp. Sci. 167, 131–170 (1996)
Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 189–213. Springer, Heidelberg (2003)
Ball, T., Rajamani, S.: Bebop: A path-sensitive interprocedural dataflow engine. In: Prog. Analysis for Softw. Tools and Eng., pp. 97–103 (2001)
Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 133–149. Springer, Heidelberg (2001)
Jones, N., Muchnick, S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: Princ. of Prog. Lang., pp. 66–74 (1982)
Deutsch, A.: On determining lifetime and aliasing of dynamically allocated data in higherorder functional specifications. In: Princ. of Prog. Lang., pp. 157–168 (1990)
Gopan, D., DiMaio, F.: N.Dor, Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Tools and Algs. for the Construct. and Anal. of Syst., pp. 512–529 (2004)
Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement for 3-valued-logic analysis. Tech. Rep. 1504, Comp. Sci. Dept., Univ. of Wisconsin (2004)
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Tools and Algs. for the Construct. and Anal. of Syst., pp. 530–545 (2004)
Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. Tech. Rep. 1505, Comp. Sci. Dept., Univ. of Wisconsin (2004)
Yorsh, G.: Logical characterizations of heap abstractions. Master’s thesis, School of Computer Science, Tel Aviv University, Israel (2003)
Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Princ. of Prog. Lang., pp. 84–96 (1978)
Miné, A.: The octagon abstract domain. In: 8th Working Conf. on Rev. Eng., pp. 310–322 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jeannet, B., Loginov, A., Reps, T., Sagiv, M. (2004). A Relational Approach to Interprocedural Shape Analysis. In: Giacobazzi, R. (eds) Static Analysis. SAS 2004. Lecture Notes in Computer Science, vol 3148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27864-1_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-27864-1_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22791-5
Online ISBN: 978-3-540-27864-1
eBook Packages: Springer Book Archive