Advertisement

Numerical Power Analysis

  • Isabella Mastroeni
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2053)

Abstract

In this paper we design abstract domains for numerical power analysis. These domains are conceived to discover properties of the following type: “The integer (or rational) variable X at a given program point is the numerical power of c with the exponent having a given property π”, where c and π are automatically determined. A family of domains is presented, two of these suppose that the exponent can be any natural or integer value, the others include also the analysis of properties of the exponent set. Relevant lattice-theoretic properties of these domains are proved such as the absence of infinite ascending chains and the structure of their meet-irreducible elements. These domains are applied in the analysis of integer powers of imperative programs and in the analysis of probabilistic concurrent programming, with probabilistic non-deterministic choice.

Keywords

Abstract interpretation static program analysis numerical power analysis probabilistic analysis 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL’ 77), pages 238–252. ACM Press, New York, 1977.CrossRefGoogle Scholar
  2. 2.
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL’ 79), pages 269–282. ACM Press, New York, 1979.CrossRefGoogle Scholar
  3. 3.
    P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation (Invited Paper). In M. Bruynooghe and M. Wirsing, editors, Proc. of the 4th Internat. Symp. on Programming Language Implementation and Logic Programming (PLILP’ 92), volume 631 of Lecture Notes in Computer Science, pages 269–295. Springer-Verlag, Berlin, 1992.Google Scholar
  4. 4.
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the 5th ACM Symp. on Principles of Programming Languages (POPL’ 78), pages 84–97. ACM Press, New York, 1978.CrossRefGoogle Scholar
  5. 5.
    G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. ACM Comput. Surv., 28(2):333–336, 1996.CrossRefGoogle Scholar
  6. 6.
    R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP’ 97), volume 1256 of Lecture Notes in Computer Science, pages 771–781. Springer-Verlag, Berlin, 1997.Google Scholar
  7. 7.
    P. Granger. Static analysis of arithmetical congruences. Intern. J. Computer Math., 30:165–190, 1989.CrossRefzbMATHGoogle Scholar
  8. 8.
    P. Granger. Analyses sémantiques de congruences. PhD thesis, École Polytechnique, 1991.Google Scholar
  9. 9.
    P. Granger. Static analysis of linear concruence equalities among variables of a program. In S. Abramsky and T.S.E. Maibaum, editors, Proc. of the Int. Joint Conference on Theory and Practice of Software Development, (TAPSOFT’91), volume 493 of Lecture Notes in Computer Science, pages 169–192. Springer-Verlag, Berlin, 1991.Google Scholar
  10. 10.
    V. Gupta, R. Jagadeesan, and V. Saraswat. Probabilistic concurrent constraint programming. In Proc. of CONCUR’ 97, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1997.Google Scholar
  11. 11.
    L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras. Part I. North-Holland, Amsterdam, 1971.Google Scholar
  12. 12.
    D.A. Huffman. A method for the construction of minimum redundancy codes. IRE, 40(10):1011–1098, 1952.Google Scholar
  13. 13.
    M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133–151, 1976.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    J.C. Lagarias. The 3x + 1 problem and its generalizations. Amer. Math. Monthly, 92:3–23, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    F. Masdupuy. Array operations using semantic analysis of trapezoid congruences. In Proc. of the 1992 ACM International Conf. on Supercomputing (ICS’ 92), pages 226–235. ACM Press, New York, 1992.Google Scholar
  16. 16.
    D. Monniaux. Abstract interpretation of probabilistic semantics. In J. Palsberg, editor, Proc. of the 7th Internat. Static Analysis Symp. (SAS’ 00), volume 1824 of Lecture Notes in Computer Science, pages 322–339. Springer-Verlag, Berlin, 2000.Google Scholar
  17. 17.
    A. Di Pierro and H. Wiklicky. An operational semantics for probabilistic concurrent constraint programming. In Proc. of the 1998 IEEE Internat. Conf. on Computer Languages (ICCL’ 98). IEEE Computer Society Press, Los Alamitos, Calif., 1998.Google Scholar
  18. 18.
    N. Saheb-Djahromi. Cpo’s of measures for nondeterminism. Theor. Comput. Sci., 12:19–37, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    V. Saraswat, V. A. Rinard, and P. Panangaden. Semantic foundations of concurrent constraint programming. In Conference Record of the 18th ACM Symp. on Principles of Programming Languages (POPL’ 91), pages 333–353. ACM Press, New York, 1991.CrossRefGoogle Scholar
  20. 20.
    C.E. Shannon. A mathematical theory of communication. The Bell System Technical Journal, 27:379–423 and 623-656, 1948.MathSciNetGoogle Scholar
  21. 21.
    M. N. Wegman and F. K. Zadeck. Constant propagation with conditional branches. ACM Trans. Program. Lang. Syst., 13(2):181–210, 1991.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Isabella Mastroeni
    • 1
  1. 1.Dipartimento Scientifico e TecnologicoUniversità di VeronaVeronaItaly

Personalised recommendations