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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
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.
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.
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.
G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. ACM Comput. Surv., 28(2):333–336, 1996.
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.
P. Granger. Static analysis of arithmetical congruences. Intern. J. Computer Math., 30:165–190, 1989.
P. Granger. Analyses sémantiques de congruences. PhD thesis, École Polytechnique, 1991.
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.
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.
L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras. Part I. North-Holland, Amsterdam, 1971.
D.A. Huffman. A method for the construction of minimum redundancy codes. IRE, 40(10):1011–1098, 1952.
M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133–151, 1976.
J.C. Lagarias. The 3x + 1 problem and its generalizations. Amer. Math. Monthly, 92:3–23, 1985.
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.
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.
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.
N. Saheb-Djahromi. Cpo’s of measures for nondeterminism. Theor. Comput. Sci., 12:19–37, 1980.
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.
C.E. Shannon. A mathematical theory of communication. The Bell System Technical Journal, 27:379–423 and 623-656, 1948.
M. N. Wegman and F. K. Zadeck. Constant propagation with conditional branches. ACM Trans. Program. Lang. Syst., 13(2):181–210, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mastroeni, I. (2001). Numerical Power Analysis. In: Danvy, O., Filinski, A. (eds) Programs as Data Objects. PADO 2001. Lecture Notes in Computer Science, vol 2053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44978-7_8
Download citation
DOI: https://doi.org/10.1007/3-540-44978-7_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42068-2
Online ISBN: 978-3-540-44978-2
eBook Packages: Springer Book Archive