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 P'', where c and P are automatically determined. A family of domains is presented, two of these consider 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.

Numerical Power Analysis

MASTROENI, Isabella
2001

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 P'', where c and P are automatically determined. A family of domains is presented, two of these consider 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.
9783540420682
abstract interpretation; static program analysis; numerical power analysis; probabilistic analysis
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/19659
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact