Abstract
We introduce a systematic approach to designing summarizing abstract numeric domains from existing numeric domains. Summarizing domains use summary dimensions to represent potentially unbounded collections of numeric objects. Such domains are of benefit to analyses that verify properties of systems with an unbounded number of numeric objects, such as shape analysis, or systems in which the number of numeric objects is bounded, but large.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)
Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Symp. on Princ. of Prog. Lang. (1978)
Dantzig, G.B., Eaves, B.C.: Fourier-motzkin elimination and its dual. Journal of Combinatorial Theory (A) 14, 288–297 (1973)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Automatic Verification Methods for Finite State Systems, pp. 197–212 (1989)
Granger, P.: Analyses Semantiques de Congruence. PhD thesis, Ecole Polytechnique (1991)
Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2), 157–185 (1997)
Harrison, W.H.: Compiler analysis of the value ranges for variables. Trans. on Softw. Eng. 3(3), 243–250 (1977)
Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Int. Symp. on Software Testing and Analysis, pp. 26–38 (2000)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280–301 (2000)
Masdupuy, F.: Array Indices Relational Semantic Analysis using Rational Cosets and Trapezoids. PhD thesis, Ecole Polytechnique (1993)
Mine, A.: The octagon abstract domain. In: Proc. Eighth Working Conf. on Rev. Eng., pp. 310–322 (2001)
Mine, A.: A few graph-based relational numerical abstract domains. In: Static Analysis Symp., pp. 117–132 (2002)
Saad, Y.: Sparsekit: A basic tool kit for sparse matrix computations, version 2. Tech. rep., Comp. Sci. Dept. Univ. of Minnesota (June 1994)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst. 24(3), 217–298 (2002)
Verbrugge, C., Co, P., Hendren, L.J.: Generalized constant propagation: A study in C. In: Gyimóthy, T. (ed.) CC 1996. LNCS, vol. 1060, pp. 74–90. Springer, Heidelberg (1996)
Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Symp. on Network and Distributed Systems Security (NDSS) (February 2000)
Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Static Analysis Symp., pp. 69–84 (2002)
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
Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M. (2004). Numeric Domains with Summarized Dimensions. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_38
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive