Numerical Power Analysis
- 153 Downloads
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.
KeywordsAbstract interpretation static program analysis numerical power analysis probabilistic analysis
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 8.P. Granger. Analyses sémantiques de congruences. PhD thesis, École Polytechnique, 1991.Google Scholar
- 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.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.L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras. Part I. North-Holland, Amsterdam, 1971.Google Scholar
- 12.D.A. Huffman. A method for the construction of minimum redundancy codes. IRE, 40(10):1011–1098, 1952.Google Scholar
- 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.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.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