×

zbMATH — the first resource for mathematics

An abstract domain to infer symbolic ranges over nonnegative parameters. (English) Zbl 1337.68077
Simon, Axel (ed.) et al., Proceedings of the 5th international workshop on numerical and symbolic abstract domains, NSAD 2014, Munich, Germany, September 10, 2014. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 307, 33-45, electronic only (2014).
Summary: The value range information of program variables is useful in many applications such as compiler optimization and program analysis. In the framework of abstract interpretation, the interval abstract domain infers numerical bounds for each program variable. However, in certain applications such as automatic parallelization, symbolic ranges are often desired. In this paper, we present a new numerical abstract domain, namely the abstract domain of parametric ranges, to infer symbolic ranges over nonnegative parameters for each program variable. The new domain is designed based on the insight that in certain contexts, program procedures often have nonnegative parameters, such as the length of an input list and the size of an input array. The domain of parametric ranges seeks to infer the lower and upper bounds for each program variable where each bound is a linear expression over nonnegative parameters. The time and memory complexity of the domain operations of parametric ranges is \(O(n m)\) where \(n\) is the number of program variables and \(m\) is the number of nonnegative parameters. On this basis, we show the application of parametric ranges to infer symbolic ranges of the sizes of list segments in programs manipulating singly-linked lists. Finally, we show preliminary experimental results.
For the entire collection see [Zbl 1310.68020].
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q25 Analysis of algorithms and problem complexity
Software:
Apron; ASTREE; Interproc
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bessiere, C., Constraint propagation, (Rossi, F.; van Beek, P.; Walsh, T., Handbook of Constraint Programming, (2006), Elsevier)
[2] Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., A static analyzer for large safety-critical software, (PLDI, (2003)), 196-207
[3] Blume, W.; Eigenmann, R., Symbolic range propagation, (IPPS, (1995)), 357-363
[4] Chen, L.; Li, R.; Wu, X.; Wang, J., Static analysis of List-manipulating programs via bit-vectors and numerical abstractions, (SAC, (2013)), 1204-1210
[5] Chen, L.; Li, R.; Wu, X.; Wang, J., Static analysis of lists by combining shape and numerical abstractions, Science of Computer Programming, (2014)
[6] Chen, L.; Miné, A.; Wang, J.; Cousot, P., An abstract domain to discover interval linear equalities, (VMCAI, LNCS, vol. 5944, (2010)), 112-128 · Zbl 1273.68081
[7] Cousot, P.; Cousot, R., Static determination of dynamic properties of programs, (Proc. of the 2nd International Symposium on Programming, (1976)), 106-130
[8] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (POPL, (1977)), 238-252
[9] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (POPL, (1978)), 84-96
[10] Gulwani, S., Speed: symbolic complexity bound analysis, (CAV, LNCS, vol. 5643, (2009)), 51-62 · Zbl 1242.68121
[11] Jeannet, B.; Miné, A., Apron: A library of numerical abstract domains for static analysis, (CAV, LNCS, vol. 5643, (2009)), 661-667
[12] Karr, M., Affine relationships among variables of a program, Acta Inf., 6, 133-151, (1976) · Zbl 0358.68025
[13] Lalire, G.; Argoud, M.; Jeannet, B., Interproc
[14] Rugina, R.; Rinard, M. C., Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Trans. Program. Lang. Syst., 27, 185-235, (2005)
[15] Sankaranarayanan, S.; Ivancic, F.; Gupta, A., Program analysis using symbolic ranges, (SAS, LNCS, vol. 4634, (2007)), 366-383 · Zbl 1211.68101
[16] Venet, A., The gauge domain: scalable analysis of linear inequality invariants, (CAV, LNCS, vol. 7358, (2012)), 139-154
[17] Zaks, A.; Yang, Z.; Shlyakhter, I.; Ivancic, F.; Cadambi, S.; Ganai, M. K.; Gupta, A.; Ashar, P., Bitwidth reduction via symbolic interval analysis for software model checking, IEEE Trans. on CAD of Integrated Circuits and Systems, 27, 1513-1517, (2008)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.