Maria Emilia

Alonso Garcia
email: alonso.mariemi@gmail.com

André Galligo
email: galligo@unice.fr

A Root Isolation Algorithm for Sparse Univariate Polynomials

Keywords: J.2 [Mathematics], I.1.2 [Computing methodologies]: Symbolic and Algebraic Manipulation-Algebraic Algorithms Algorithms,Theory real univariate polynomial, fewnomial, real root isolation, Generalized Budan-Fourier theorem, F virtual roots, F Budan table, Newton process, discretization, separation bounds

. To such a f is associated a set of d + 1 F-derivatives. The Budan-Fourier function V f (x) counts the sign changes in the sequence of F-derivatives of the f evaluated at x. The values at which this function jumps are called the F-virtual roots of f , these include the real roots of f . We also consider the augmented F-virtual roots of f and introduce a genericity property which eases our study. We present a real root isolation method and an algorithm which has been implemented in Maple. We rely on an improved generalized Budan-Fourier count applied to both the input polynomial and its reciprocal, together with Newton like approximation steps. The paper is illustrated with examples and pictures.

INTRODUCTION

On the one hand the concept of sparse representations and more particularly of fewnomial play a crucial role in modern real algebraic geometry and in complexity theory, see [START_REF] Bochnack | Real Algebraic Geometry[END_REF][START_REF] Basu | Algorithms in real algebraic geometry[END_REF]. On the other hand, during the last two decades, algorithmic and theoretic progresses have been made on real or complex root finding of a univariate real polynomial; see e.g [START_REF] Mcnamee | A bibliography on roots of polynomials[END_REF] and [START_REF] Pan | Solving a polynomial equation: some history and recent progress[END_REF] and the references therein. See also [START_REF] Eigenwillig | Almost tight complexity bounds for the Descartes method[END_REF][START_REF] Emiris | Random polynomials and expected complexity of bissection methods for real solving[END_REF][START_REF] Tsigaridas | I: On the complexity of real root isolation using continued fractions[END_REF][START_REF] Zhang | A New Method for Real Root Isolation of Univariate Polynomials[END_REF][START_REF] Mourrain | On the complexity of isolating real roots ofand computing with certainty the topological degree[END_REF][START_REF] Sagraloff | When Newton meets Descartes: A simple and fast algorithm to isolate the real roots of a polynomial[END_REF][START_REF] Sagraloff | A simple but exact and efficient algorithm for complex root isolation[END_REF].

In this paper we address, with new tools presented initially in [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF] and [START_REF] Galligo | Improved Budan-Fourier count for Root Finding[END_REF], the root finding problem for sparse polynomials. We consider a univariate polynomial f with real coefficients having a high degree N but a rather small number d + 1 of monomials, with d << N . Such a polynomial (often called sparse) has a number of real root smaller or equal to d. Our target is to find for each real root of f an interval isolating this root from the others. The usual subdivision methods relying either on Sturm sequences or Moebius transform followed by Descartes's rule of sign destruct the sparse structure, hence can hardly be used for very large N .

In the 19th century the Budan-Fourier theorem, which counts signs variations of a sequence of derivatives was considered as an important progress but it only provided a bound on the number of real roots. Then Sturm introduced the Sturm sequences, defined via polynomial Euclidean divisions, to provide an exact count of the real roots in an interval. This breakthrough was followed by many algorithmic progresses, emphasized with the use of computer algebra systems and their applications in applied sciences.

However in some applications (e.g. cryptography) the polynomials have high degrees but are sparse, therefore the efficient determination of their real roots is a natural problem. Our approach relies on the generalized Budan-Fourier theorem of Coste, Lajous, Lombardi, Roy [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF] and the techniques developed in [START_REF] Bembe | A: Virtual roots of real polynomials and fractional derivatives[END_REF] and [START_REF] Galligo | Budan Tables of Real Univariate Polynomials[END_REF]. See also [START_REF] Sturm | Mémoire sur la résolution des équations num'eriques[END_REF][START_REF] De | Nouvelle méthode pour la résolution des équations numériques d'un degré quelconque[END_REF][START_REF] Fourier | Analyse des équations déterminées[END_REF] and [START_REF] Bembe | A: Virtual roots of real polynomials and fractional derivatives[END_REF]. To such a f is associated a set of F-derivatives. The Budan-Fourier function V f (x) counts the sign changes in the sequence of F-derivatives of f evaluated at x. The values at which this function jumps are called the virtual roots of f , these include the real roots of f . We also define the augmented F-virtual roots of f . The table containing the signs of all the F-derivatives of a polynomial f is called, in this paper its F-Budan table, in honor of Budan de Boilorant [START_REF] De | Nouvelle méthode pour la résolution des équations numériques d'un degré quelconque[END_REF]. Once the coefficients are bounded it is also the case for the real roots of f and all its F-derivatives. So the table is a rectangle decomposed into positive and negative blocks

In [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF] it is proved that the ordered sequence of F-virtual roots depend continuously on the coefficient of f . We will also consider a generic condition on f , we call (FP), which imposes that the F-derivatives have pairwise distinct simple roots, but we allow clusters of such roots. This condition eases the analysis and the presentation; since we also consider clusters the general case can be seen as a limit situation. To isolate the real (or F-virtual) roots of f we need a separation bound (which will depend on the size of the coefficients and on d and N ), it will serve to stop a subdivision process. Intuitively in the case of integer coefficients, such a separation bound expresses the fact that the input belongs to a finite set of data, consequently the event that two roots collide is discrete and must correspond to a jump. It is well known that a minimum separation bound s satisfies log(s) is Õ(N t), where t is the maximum bit size of the integer coefficients of f .

Our strategy of computation is based on simple ideas. First, we borrowed from [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF], the sequence of derivatives naturally adapted to sparsity and constructed the F-Budan table which has the same features than the "usual" one studied in [START_REF] Galligo | Improved Budan-Fourier count for Root Finding[END_REF]. Second, we consider successive approximations of the shape of the F-Budan table, or of portions of this table, defined by evaluations of the F-derivatives at some points determined by an exclusion/inclusion process, which draws a discretized picture of the table. This process can be viewed a revisited version of the classical work of Collins and Loos [START_REF] Collins | Polynomial Real Root Isolation by Differentiation[END_REF], which was recently reconsidered and improved in [START_REF] Pan | Real root-finding[END_REF], see also [START_REF] Pan | Univariate polynomials: Nearly optimal algorithms for numerical factorization and rootfinding[END_REF]. Third, we noticed that although the positive roots of F (x) = x N f (1/x) are the reciprocal of the positive roots of f (x), this is generally not the case for the other F-virtual roots. Hence isolating simultaneously the virtual roots of these two sparse polynomials allows to focus on the real roots and get rid of the other F-virtual roots.

We do not provide a complexity analysis of our algorithm. However, let us say that its complexity is bounded by the complexity of computing the roots of all F-derivatives, adapting [START_REF] Collins | Polynomial Real Root Isolation by Differentiation[END_REF] and [START_REF] Pan | Real root-finding[END_REF]. As above, we denote by t the maximum bit size of the integer coefficients of f . We observe that the evaluation cost of all d + 1 F-derivatives of f at a dyadic number of bit size Õ(N t) is bounded by Õ(N 2 t 2 d 2 ), while for a non sparse polynomial the corresponding cost of a (fast) Taylor shift is at least Õ(N 3 t), hence greater when N > tildeO(td 2 ). Adapting [START_REF] Pan | Real root-finding[END_REF] one can compute (recursively on increasing i) the roots of gi, the F-derivatives of f , in intervals where they are already isolated and where all the gj with j < i keep a constant sign (hence the generalized Budan-Fourier count indicates 1). We expect, but did not prove yet, that in that situation a Newton like process will converge quadratically. Since there are less than d 2 such points, we would arrive at a bound of Õ(N 2 t 2 d 4 ). So, we expect our algorithm to be competitive with the best non sparse ones, at least when N > tildeO(td 4 ).

The paper is organized as follows. Section 2 introduces definitions, concepts and properties of F-Budan tables and (augmented) F-virtual roots of a sparse polynomial. Section 3 illustrates them on examples. Section 4 presents our certified root finding algorithms of real roots of a sparse polynomial f , then reports some experiments. Section 5 consider more general fewnomials, recalling the results of [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF].

Notations and illustrative example R denotes the field of real numbers, and R+ the set of positive real numbers, A sparse polynomial f is given by the list of its (d + 1) terms, we denote the (non zero) coefficients by ai and the strictly decreasing degrees by ri, f := i=d i=0 aix r i . The degree N = r d is thought much greater than d. We use as illustrative example the following sparse polynomial with 50 monomials, degree 1881, and important difference in the sizes of its integer coefficients.

DEFINITIONS AND CONCEPTS

F-derivatives

The idea of F-derivative of a sparse polynomial f (x) := i=d i=0 aix r i , is quite natural. ( [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF] reports that it was already considered by Sturm in a special case). It is based on the simple observation that if f (x) admits a monomial factor x m then for any x0 ∈ R+, f (x0) and f (x0)/x m 0 have the same sign. One first forms the polynomial g d (x) = f (x)/x r 0 which has a non zero constant term, degree r d -r0, and the same distribution of signs on R+ than f . Then consider the usual derivative g d (x), since r1 > r0 it admits a factor x r 1 -r 0 -1 , then define the polynomial g d-1 (x) := g d (x)/x r 1 -r 0 -1 ; it has d terms (one less than g d ), degree r d -r1. So we can iterate this construction. Definition 1. With the previous notations, given a sparse polynomial f , we associate to it the following sequence of its d + 1 F-derivatives constructed by induction as follows.

g d := f /x r 0 , for i from 1 to d, g d-i := (g d-i+1 ) /x r i -r i-1 -1 .
So g d-i is a sparse polynomial with d -i monomials and degree r d -ri and g0 is a constant.

Remark 1. When we restrict to the half line x > 0 as we noticed above, g d-i and the derivative of g d-i+1 have the same sign. Hence if

g d-i+1 (x0) = 0 and g d-i is positive for x > x0 then g d-i+1 is also positive for x > x0, but if g d-i is positive for x < x0 then g d-i+1 is negative for x < x0.

(Respectively when we exchange the words positive and negative).

This is a simple but key remark for understanding the structure of the F-Budan table of f , which collects the signs of all the polynomials g d-i , for i = 0..d. Illustrative examples are provided in the next section.

F-Budan tables and F-virtual roots Definition 2. With the previous notations, let f be a monic sparse polynomial and (g d-i )i the sequence of its Fderivatives. The F-Budan table of f is a subset of the real plane equal to the union of d + 1 infinite rectangles of height one

Li := R+ × [i -1/2, i + 1/2[ for i from 0 to d, called rows. For i from 0 to d,
Remark 2.

1. Once we know the coefficients of f , the positive real roots of all its derivatives are contained in an interval [0, 2 M ] for some integer M . So the table is in fact finite, and when we say ∞ we mean 2 M .

Since f is assumed monic, every infinite right rectangle

of each row is gray.

3. Since g0 is a positive constant, the row L0 is a gray infinite rectangle.

The first rectangle of each row

Li is gray (resp. black), if ai is positive (resp. negative).

We are interested by the connected components of the union of the closures of the gray rectangles; and respectively for the black rectangles. It is clear that there is a gray connected component containing the infinite right rectangles of all rows. The other connected components (gray or black) are said bounded on the right.

A "descriptor" attached to a F-Budan table is the function V f (x) of the real positive indeterminate x with values in the set of integers N, it counts the number of sign changes in the sequence formed by f and its F-derivatives evaluated at x.

Definition 3. For a sequence (b 0 , . . . , b n ) ∈ (R\{0}) n+1
the number of sign changes V(b0, . . . , bn) is defined inductively in the following way:

V(b0) := 0; V(b0, . . . , bi) := V(b0, . . . , bi-1) if bi-1bi > 0, V(b0, . . . , bi-1) + 1 if bi-1bi < 0.
To determine the number of sign changes of a sequence (b0, . . . , bn) ∈ R n+1 , delete the zeros in (b0, . .

. , bn) and apply the previous rule. (V of the empty sequence equals 0).

The following proposition contains the Generalized Budan-Fourier theorem of [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF].

Proposition 1. With the previous notations, let f be a monic sparse polynomial and (g d-i )i the sequence of its Fderivatives. Then,

• V f (0) equals the number of sign changes in the se- quence of coefficients of f , while V f (∞) = 0.
• Near a real root c of multiplicity k of f , which is not a root of another F-derivative of f , V f decreases by k when x moves from c -h to c + h, for sufficiently small positive h .

• Near a real root c > 0 of multiplicity k of g d-m , (or equivalently of k successive F-derivatives), which is not a root of another non successive F-derivative of f , the following happens:

If k is even, V f decreases by k.
If k is odd, V f decreases by the even integer k + s1s2, where s1 and s2 are the signs at c of g d-m+1 and g d-m-k .

• Near c > 0, a real root of several non successive Fderivatives of f , V f decreases by the sum of the quantities corresponding to each of them.

• Near the other points of R+, V f is constant.

The function V f is decreasing (but not strictly) on R+.

• For a, b ∈ R with 0 < a < b, the number m of real roots of f in the interval ]a, b] counted with multiplicities is at most V f (a) -V f (b). Moreover the defect V f (a) - V f (b) -m is an even integer.
Definition 4. With the previous notations, let f be a monic sparse polynomial and (g d-i ) the sequence of its Fderivatives. The x value of the rightmost upper edge of a connected component (either gray or black) of the F-Budan table of f is called a F-virtual root of f . Any real root (in the usual sense) of f is a F-virtual root of f . Any multiple real root (in the usual sense) of any F-derivative of f is also a virtual root of f . The virtual multiplicities are counted as follows:

• the multiplicities of events appearing along a same x-value are added,

• the multiplicity of a simple root of f counts one,

• the multiplicity of a simple F-virtual non real root (i.e. not a multiple root of a F-derivative of f ) counts two,

• the multiplicity of a root of f of order k counts k,

• the multiplicity of a multiple F-virtual non real root c which is a root of order k of a derivative of f counts k if k is even, and otherwise k + s1s2 where s1 and s2 are the signs at c of g d-m+1 and g d-m-k .

The Generalized Budan-Fourier theorem implies that f admits d F-virtual roots counted with multiplicities. Moreover the following result holds.

Theorem 2.1 ( [8]

). The ordered sequence of F-virtual roots of a sparse polynomial f depend continuously on the coefficients of f .

Generic case

In this subsection we assume a condition (FP), generically satisfied.

Definition 5. With the previous notations, let f be a monic sparse polynomial. It satisfies condition (FP) if and only if: each of its F-derivatives has simple roots, and all these roots are pairwise distinct. A monic sparse polynomial satisfying this condition will be called a (FP)-polynomial.

It is easy to see that the F-Budan table B of a (FP)polynomial f also has the following two features.

• For 0 ≤ i ≤ d, if ai is positive (resp. negative) then the number of rectangles on the row Li is odd (resp. even).

• Let (l + 1) be the number of rectangles of the top row L d , then l ≤ d and d -l is an even number 2p. There are l + p + 1 same-color-connected components of B.

Each non first rectangle of Li, i > 0 is connected on the left to a rectangle of the same color of the row Li-1.

Definition 6. We call augmented F-virtual root of f the pair (y, k) formed by a F-virtual root of f and the integer k such that g d-k vanishes at y.

Multiple roots

In the general case of a sparse polynomial the condition (FP) is not necessarily satisfied, because the g d-i may have multiple roots. To keep the previous two nice features we proceed as follows. We now decompose the row L d-i by a possibly smaller number of rectangles by replacing two adjacent rectangles with the same color by their union (i.e. forgetting the multiple positive roots of g d-i with even order). Then the F-Budan table B of f looks like the Budan table of a (FP)-polynomial and we can define similarly the augmented F-virtual root of f to be the pair (y, k) formed by a F-virtual root of f and the integer k such that y is a positive roots of g d-k with odd order of multiplicity; such that (y, k) is the rightmost edge of a same-color-connected component of B.

Truncated F-Budan table

With the previous notations, let f be a monic sparse polynomial. We analyze the properties of a sub-table P := P (f, a, b, u, v) of its F-Budan table B. P is delimited on the x axis by two real numbers a and b which are not root of a F-derivative of f , a < b, and on the second coordinate by two integers u and v such that 0 ≤ u < v ≤ d.

Let us denote by W (x) := W (f, u, v)(x) the function giving the number of sign changes in the sequence formed by the F-derivatives g k , with u ≤ k ≤ v evaluated at x. Let l1 (resp. l2) be the number of real roots of gu (resp. gv) between a and b.

Let h1 := W (a) + l1 and similarly h2 := W (b) + l2. Notice that h1 counts the number of sign changes along the left-lower corners of the rectangle; similarly h2 counts the number of sign changes along the right-upper corners of the rectangle.

Proposition 2. With the previous notations, h2 -h1 is an even number, we denote it by 2p. Then the sub-table P has l2 +p same-color-connected components (not bounded on the right), the top row of P has l2 + 1 rectangles (their l2 right ends indicate the l2 real roots of gv between a and b); and the p other ends of the same-color-connected components indicate the F-virtual non real roots of gv in P (hence Fvirtual non real roots of f ).

The proof is purely combinatorics and is exactly the same as the one given in [START_REF] Galligo | Budan Tables of Real Univariate Polynomials[END_REF] for the usual derivatives and the usual Budan tables.

Discretized Budan table

We can discretize a truncated F-Budan via intersections with grids. In the illustrations, to be clearer, we replace the sign + by a gray solid box and the sign -by a black empty box.

ILLUSTRATIONS AND EXAMPLES

We first provide a picture (Figure 1) of the (truncated) F-Budan table of a low degree polynomial f1 to illustrate the concept: we consider a polynomial of degree 7 with a multiple real root and another multiple virtual root. We truncated in order to only keep the degrees between u = 3 and v = 7; and the interval [0, ∞] Notice that the rightmost edges of some rectangles are aligned. We see one gray connected component and two black connected components, (plus a gray component not bounded to the right). We observe 6 sign changes on the leftmost column and 0 sign changes on the rightmost column, 0 roots for gv in the interval and 3 roots with sign changes for gu; hence h1 = 6 and h2 = 0. As predicted by the theorem the variation (here 6) equals twice the number of connected components not arriving to the top row, here 3 (two black and one gray).

We then consider the Budan table (Figure 2) of a generic polynomial, notice that the rectangle are not aligned. We see two black connected components, (plus a gray component not bounded to the right). So there are two virtual non real root. We count 4 sign changes on the leftmost column and 0 sign changes on the rightmost column. Moreover the lower and upper polynomials have no real roots in the interval. As predicted by the theorem the variation (here 4) equals twice the number of connected components not arriving to the top row.

Then we consider the reciprocal polynomial of the sparse

ROOT FINDING ALGORITHMS AND EX-PERIMENTS

Here we present the main feature of our root finding algorithm, we made a prototype implementation in Maple.

Strategy of computation

We will use a subdivision method with inclusion/exclusion tests relying on generalized Budan Fourier counts for the two polynomials f and its reciprocal Rf . Let us first compare the positive virtual roots of f and Rf .

Rf (x) = x N f (1/x) hence the real roots of Rf are the reciprocal of the real roots of f with the same multiplicity. However if a is a real root of f but not of f , we have

(Rf ) (1/a) = N a -N +1 f (a) -a -N +2 f (a) = = N a -N +1 f (a) = 0. If a is a real root of f but not of f , we have (Rf ) (1/a) = N (N -1)a -N +2 f (a) + (2 -2N )a -N +3 f (a) + a -N +4 f (a), so (Rf ) (1/a) = a -N +2 (N -1)(N f (a)-2af (a)).
Therefore (Rf ) (1/a) may vanish but it is not likely. And similarly for other higher derivatives. This is also applies to F-derivatives.

Hence we can expect that if some a is a F-virtual root of f and 1/a is a F-virtual root of Rf then a will be a real root of f . In any case, if we look for the real roots of f we can exclude the reciprocal of the intervals which do not contain any F-virtual root of Rf . Then we will have to check that the remaining intervals does not contain any F-virtual non real root.

For a later step of the algorithm, we will collect in a set B the "small" intervals such that generalized Budan Fourier counts for the two polynomials f and its reciprocal Rf returns 2. This indicates either two close real roots or a virtual root for each of the two polynomials. We will use a Newton like process to narrow the intervals and make a decision. That purpose requires ultimately a separation bound and a control of the quadratic convergence.

We decompose the algorithm into a preprocessing relying on a "small" number of bissection steps, a processing which mix bisections and Newton like steps and a post processing which deals with the intervals in B (i.e. returning 2).

Subroutines

FDeriv

Our approach uses the F-derivatives of a input sparse polynomial f with d + 1 monomials. The function FDeriv(f, d) computes the (ordered) sequence g formed by the d + 1 Fderivatives of f .

sv

The function sv(f, u, v) counts the number of sign variations in the terms (numbered between u and v) of the ordered list of coefficients of f . u and v are integers with 0 ≤ u ≤ v ≤ d. It also returns the corresponding list of signs.

Count

Our algorithmic method is based on partial Budan Fourier counts. The function Count(g, a, u, v) counts the number of sign variations in the terms (numbered between u and v) of a ordered list of polynomials g, evaluated at a. So a is a positive real number, u and v are integers with 0 ≤ u ≤ v ≤ d. It also returns the corresponding list of signs.

Notice that Count(g, 0, u, v) is not valid, it is replaced by sv(f, u, v) which plays the same role.

Trunc

Our algorithm is based on the location of the augmented virtual roots in R × [0, d], by a kind of quad-tree method which aims to diminish both the real interval and the integer one. Given two lists of signs, the function Trunc(L,M) computes the numbers of sign changes and the index when the difference of numbers of sign changes between the two lists becomes greater than 1, starting from below.

Reciprocal

Our algorithm uses the reciprocal of f to separate the real from the non real F-virtual roots. The function Reciprocal(f ) computes the reciprocal polynomial of f , which has the same number of monomials.

Bound

In some cases we need to certify that a polynomial h does not vanish on a small interval [a, b], this is done by the function Bound(f ), relying on interval arithmetic.

Halley

We will need a function computing a Newton like step. Since with sparse polynomials, usual Newton approximations "near" zero can be unstable, we propose to use Halley approximation process, which uses the second derivative and gives an approximation of order 3. More precisely for a polynomial h at a point a, letting b := h(a), c := h (a), e := h (a) the increment is given by: b c -be 2c .

Preprocessing

The first step of the preprocessing, computes sv(f, 0, d) then Count(g, i, 0, d for the integers i < M , for some bound M defined by the context, till we find 0 or 1 or 2, call i0 this maximal integer, and similarly for Rf , and j, call j0 this maximal integer. The second step proceed for each 1 ≤ i ≤ i0 to bisections with exclusions (resp. selection in a set A) of intervals which returns 0 to one of the two tests for f and Rf . And similarly for j.

At the end of this preprocessing, we have three sets: A which contains isolating intervals for some positive real roots of f ; B which contains intervals returning 2 to the generalized Budan Fourier counts for the two polynomials f and Rf ; E which contains intervals returning at least 2 and more than 2 to the two generalized Budan Fourier counts (they will be subdivided during the processing step).

Processing

During this step we will not only subdivide the intervals of E but also the range of integers [0, d], so we replace each intervals I in E by a product I × [k1, k2] and initialize k1 := 0, k2 := d.

Instead of performing a bisection of I by the middle, we perform the 2 following steps which aims bounding the clusters of augmented F-virtual roots.

1) Cutting the bottom and refining: For a chosen I × [k1, k2] in E, we first compute the lower degree k + 1 such that the generalized Budan Fourier count BF (g d-k+1 (I) becomes greater or equal to 2. Therefore g d-k admits a simple root on I and all its F-derivatives have one or zero (simple) root on I. To achieve a good convergence, we propose to perform two Newton like steps from each edge and a bissection (as usual in numerical recipes, or follow [START_REF] Abbott | Quadratic interval refinement for real roots[END_REF], to avoid to leave the interval or encounter a cycle, since we cannot certify convexity). Then update the sets A, B and E as explained above.

Notice that an approximation provides a decimal number α , then for any derivative h, the sign of h(α) can be exactly computed. Compare with [START_REF] Zhang | A New Method for Real Root Isolation of Univariate Polynomials[END_REF].

2) Cutting the top: If for some I × [k1, k2] in E the total multiplicities of the cluster of F-virtual roots in I, detected by the changes in the signs variations, is greater than k2 -k1, it means that the cluster should be divided at least in two parts. Starting from the top, a probable good cutting integer is the the value k3 where the partial difference of signs variations W (g, u, v) on I (see Section 2) pauses. So we perform a same sign test; if it succeeds, we delete I ×[k1, k2] from E, then add I ×[k1, k3] and I × [k3 + 1, k2] in E.

We stop either when E is empty or if the sizes of all remaining intervals I are smaller than a separation bound (to be given together with the input).

Post processing

We consider all elements I × [k1, k2] in B, which returns 2 to both generalized Budan Fourier counts. Then the picture of both F-Budan tables either look like the one pictured in Figure 4, or there are two (close) real roots.

We determine a degree k > 0 such that for an interval I = [a , b ] included in I, g d-k+1 keeps a constant sign on I and g d-k has one simple root in I , then check if the corresponding generalized Budan Fourier count returns 1. We use Newton like procedures to compute I from I.

Finally check that all the augmented virtual roots of f (or Rf ) have been well processed.

Experiments

The illustrative example

Consider as input the sparse polynomial f given as illustrative example in section 1, with d = 49. We denote by g the sequence of 50 F-derivatives of f and by Rg the sequence corresponding to the reciprocal Rf of f . A very fast computation gives:

sv(f, 0, d) = 24; Count(g, 1, 0, d) = 3; Count(Rg, 1, 0, d) = 5; Count(g, 2, 0, d) = 0; Count(Rg, 2, 0, d) = 1.
This means that f admits in R+, 24 F-virtual roots counted with multiplicities (it is of course the same number for Rf but they need not be the same real numbers). Among them 21 are between 0 and 1, and three are between 1 and 2. Respectively, 19 F-virtual roots counted with multiplicities of Rf are between 0 and 1, four are between 1 and 2, and one is greater than 2. Considering the bijection between the real roots defined by the reciprocal, this implies that f has one real root between 0 and 0.5 and at most four real roots between 0.5 and 1.

After only 6 bissection steps, and without Newton steps, we isolate the three real roots of f between 1 and 2 in Together with the root of f between 0 and 0.5 (reciprocal of the one of Rf greater than 2), we can now certify that f has only 8 positive real roots. We use the subroutine Halley applied 10 times (starting from left and right edges) to get the following approximations: [0.1666668837, 0.6909172229, 0.9618369266, 0.9897489318, 0.9977283470, 1.020705838, 1.026238398, 1.063606662].

Other examples

We made other experiments with higher degrees and number of monomials. For the approximations we used big-floats with 50 digits. sv(f, 0, d) = 5; Count(g, 1, 0, d) = 1; Count(Rg, 1, 0, d) = 4; Count(g, 2, 0, d) = 0; Count(Rg, 2, 0, d) = 0. After 1 bissection steps on [START_REF] Abbott | Quadratic interval refinement for real roots[END_REF][START_REF] Basu | Algorithms in real algebraic geometry[END_REF], we obtain one positive real roots approximated by x1 := 1.0312. After 10 bissection steps on [0.5, 1] the preprocessing diminish the interval but fails to isolate any other root and the processing starts with a := 0.599609375, b := 0.60009765625, such that Count(g, a, 0, d) = 5 ; Count(Rg, a -1 , 0, d) = 0;

Count(g, b, 0, d) = 1 ; Count(Rg, b -1 , 0, d) = 4.
This means that in [a, b] there are between 0 and 4 real roots of f . Moreover the list of signs of g evaluated at a, resp. b are

[-1, 1, -1, 1, -1, 1] , resp [-1, -1, -1, -1, -1, 1].
As we can see, there is a root of g [START_REF] Basu | Algorithms in real algebraic geometry[END_REF] in [a, b] it is approximated with one step of Newton-Halley. We get bb := 0.600000000000000000019563263224; then Count(g, bb, 0, d) = 2; Count(Rg, bb -1 , 0, d) = 3. This means that there is a real root of f in [bb, b] and up to 3 real roots in [a, bb]. The root in [bb, b] is approximated, using 10 steps of Newton-Halley, by x2 := 0.6000005. Moreover the list of signs of g [START_REF] De | Nouvelle méthode pour la résolution des équations numériques d'un degré quelconque[END_REF], g [START_REF] Bochnack | Real Algebraic Geometry[END_REF], g [START_REF] Bembe | A: Virtual roots of real polynomials and fractional derivatives[END_REF] evaluated at bb is [1, 1, 1], so there is a root of g [START_REF] Bembe | A: Virtual roots of real polynomials and fractional derivatives[END_REF] in [a, bb], it is approximated with 10 steps of Newton-Halley. We get aa := 0.59999999998452259; then Count(g, aa, 0, d) = 4; Count(Rg, aa -1 , 0, d) = 1. This means that there is one real root of f in [a, aa], and up to 2 real roots in [aa, bb] or a virtual non real root. The root in [a, aa] is approximated, using Newton-Halley, by x3 := 0.59999943. Since bb -aa is small (about 10 -11 ), an early detection is checked using the subroutine Bound (interval arithmetic), it did not work neither with f nor with Rf (too many cancellations). Then we check the signs of g [START_REF] Bochnack | Real Algebraic Geometry[END_REF] (and the other derivatives of f , resp Rf ) around aa (resp aa -1 ), letting aa1 := aa -10 -20 and aa2 := aa + 10 -20 ; we get: Count(g, aa1, 0, d) = 4; Count(Rg, aa1 -1 , 0, d) = 1, Count(g, aa2, 0, d) = 2; Count(Rg, aa2 -1 , 0, d) = 1. This means that there is a F-virtual non real root of f in [aa1, aa2].

Therefore f admits only 3 positive real roots, approximated by x1 := 1.0312, x2 := 0.6000005 and x3 := 0.59999943 and a F-virtual non real root (it is a root of the second derivative of f ) approximated by aa := 0.59999999998452259.

GENERAL FEWNOMIALS

In [START_REF] Coste | Generalized Budan-Fourier theorem and virtual roots[END_REF], the concept of f -derivatives is generalized to functions which are not polynomials but which behave similarly, called fewnomials. For instance, a finite sum of monomials and exponentials multiplied by monomials.

Example 1. f := -2 x + 3 x 2 -x 3 + x 5 + e x + 5 e x x -4 x 2 e x + 3 e x x 3 -2 e x x 4 One can attach to such a function f , a sequence of positive functions over R+ denoted by fi and a finite sequence of Fderivatives gi of f such that the last one is 0. More precisely the i-th differentiation operator Di satisfies Di(h) := (h/fi) .

Therefore the sparse polynomials and the F-derivatives considered in the previous sections are a special case of fewnomials and their F-derivatives.

In the previous example, the sequence of fi is [1, 1, ..., 1, e x , 1, 1, ...]. We get g10 := f then deriving as usual g9 := f , ..., g4 := -449 e x -733 e x x -310 x 2 e x -45 e x x 3 -2 e x x 4 then we divide by e x , then we derive as usual to get eventually g0 := -48.

Note that in this case the number of F-derivatives (here 10) is not equal to the number of terms (here 9).

All our constructions (F-Budan tables and trees, augmented F-virtual roots, discretizations, etc.) and even the strategy of the root isolation algorithm could be generalized to fewnomials. This will be the subject of a future work.

CONCLUSION

In this paper we described an algorithmic realization of the improved generalized Budan-Fourier count (relying on the concept of F-derivatives) for the case of sparse polynomials. We illustrated it with a step by step description on examples, and emphasized that sparsity was always preserved. The example were computed with a prototype implementation which needs to be developed further.

Our description and illustrative examples suggest that for very sparse polynomials, our new approach can become competitive with Descartes or Sturm-based solvers. A tentative asymptotic complexity analysis indicates that this could be already the case when N > d 4 t, t being the maximal bit-size of the coefficients. In a future work, we plan to study the influence of the complex non real roots, near the real axis, on the generalized Budan-Fourier count.

  each row Li is the union of a set of open rectangles (possibly infinite), separated by vertical segments. We color in black the rectangles corresponding to negative values of g d-i , and in gray the rectangles corresponding to positive values.

Figure 1 :Figure 2 :

 12 Figure 1: A truncated table with multiple roots

Figure 3 :

 3 Figure 3: a discretized truncated table

Figure 4 :

 4 Figure 4: a Two truncated table

[ 1 .

 1 015625, 1.0234375], [1.0234375, 1.03125], [1.0625, 1.125]. After only 5 bissection steps, and without Newton steps, we isolate the four real roots of f between 0.5 and 1 in [0.5, .75], [.9375, .96875], [.984375, .9921875], [.9921875, 1].

Example 1 :

 1 d = 100, N = 10000 the integer coefficients are chosen randomly with mean 0 and variance d i . We got: sv(f, 0, d) = 49; Count(g, 1, 0, d) = 7; Count(Rg, 1, 0, d) = 4; Count(g, 2, 0, d) = 0; Count(Rg, 2, 0, d) = 0. After 13 bissection steps on [1, 2], we got tree isolating intervals for real roots of f : [1.00390625, 1.0078125], [1.000976562, 1.001953125], [1.000488281, 1.000976562] After 10 bissection steps on [0.5, 1], we got tree isolating intervals for real roots of f : [0.96875, 0.984375], [0.998046875, 0.9990234375], [0.9995117188, 0.9997558594]. So in total 6 positive real roots for f . Example 1bis: d = 100, N = 100000 the integer coefficients are chosen randomly with mean 0 and variance d i . We got: sv(f, 0, d) = 49; Count(g, 1, 0, d) = 3; Count(Rg, 1, 0, d) = 4; Count(g, 2, 0, d) = 0; Count(Rg, 2, 0, d) = 0. After 9 bissection steps on [1, 2], 8 bissection steps on [0.5, 1], we found 5 positive real roots approximately 0.99831299795; 0.999564942443394; 1.00088846858; 1.00131900658 and 1.00433128542457. Example 2: d = 100, N = 10000 the integer coefficients are chosen randomly with mean 0 and variance 1000. We got: two positive real roots one in each interval [0.5, 1] and [1, 2], approximately 0.9995297658 and 1.000014911. Example 2bis: d = 100, N = 10000 the integer coefficients are chosen randomly with mean 0 and variance 1000. We got: After 13 bissection steps on [1, 2], three positive real roots approximately 0.9745463; 1.00005 and 1.0001103. Example 3: d = 5, N = 100, we consider the Mignotte like polynomial: x 100 -625 x 4 +1500 x 3 -1350 x 2 +540 x-81.

  table truncated for 0.8 < x < 1; we chose an equidistributed grid with 200 values between 0.8 and 1. It allows to "guess" the truncated F-Budan table. (This can be certified by a computation). We can count 19 sign changes on the leftmost column and 4 sign changes on the rightmost column. Since there are no sign change on the first row, we expect 19 -4 = 15 contributions of the same-color-connected components. It is what we get. Indeed we see 3 real roots and 6 F-virtual non real roots (each contributes 2), hence 3 + 2 × 6 = 15. The grid coordinates of the 6 F-virtual non real roots are: [870, 22], [900, 34], [949, 37], [951, 16], [953, 7], [955, 3].

Acknowledgments

We thank the anonymous reviewers for their comments and suggestions. The first author was partially supported by Spanish organizations: IMI(UCM), UCM (Grupo 910444) and MEC (MTM2011-22435). The second author was partially supported by the contract MathAmSud (11MATH-04-Complexity-Deterministic and probabilistic complexity of algorithms for solving equations) and by the European Marie Curie network SAGA.

* Partially supported by Spanish organizations: IMI(UCM), UCM (Grupo 910444) and MEC (MTM2011-22435).

† and INRIA Mediterrannée, Galaad project team.


Myriam Rakho
email: rakho@univ-mlv.fr

Éric Laporte
email: eric.laporte@univ-mlv.fr

Matthieu Constant
email: matthieu.constant@univ-mlv.fr

A new semantically annotated corpus with syntactic-semantic and cross-lingual senses

Keywords: cross-lingual Word Sense Disambiguation, sense inventory, data annotation

In this article, we describe a new sense-tagged corpus for Word Sense Disambiguation. The corpus is constituted of instances of 20 French polysemous verbs. Each verb instance is annotated with three sense labels: (1) the actual translation of the verb in the english version of this instance in a parallel corpus, (2) an entry of the verb in a computational dictionary of French (the Lexicon-Grammar tables) and (3) a fine-grained sense label resulting from the concatenation of the translation and the Lexicon-Grammar entry.

Introduction

Word Sense Disambiguation (WSD) is the task of automatically identifying the correct sense of a polysemous word in particular contexts. WSD is an intermediate NLP task, and thus some key factors in designing the disambiguation strategy depend on the final application, among them the sense inventory definition. One common practice in recent multilingual WSD is to use the actual translations of the polysemous words in a parallel corpus as sense labels. Another approach, less experimented, has appeared recently which uses the entries of the polysemous words in a computational lexicon as sense labels. The level of sense granularity in those two approaches may not be sufficient for multilingual WSD when they are used individually. In both cases, some sense labels may be to coarse-grained or too fine-grained for the source language (SL) or for the target language (TL).

In this paper, we address the problem of identifying an appropriate and effective WSD sense inventory for machine translation (MT) applications. As suggested by Ide and Wilks (2006), we propose to combine evidence from the translations and from the entries in a computational lexicon to determine the polysemous word senses. For that purpose, we have built a new semantically annotated corpus for 20 French polysemous verbs (section 2). In this corpus, every verb instance is tagged with 4 sense labels:

(1) its corresponding entry in a computational lexicon in which sense distinctions are based on syntactic-semantic evidence, the Lexicon-Grammar tables (denoted as LG), a computational dictionary for French in which the senses of the words are determined on the basis of syntactic and semantic evidence

(2) its actual translation in a parallel corpus (TRSL)

(3) a fine-grained sense label which is concatenation of the LG entry and the translation (LG#TRSL)

(4) and a class of sense labels: all the fine-grained senses that have the same 'LG' part (i.e. all the possible translations of its LG sense tag)

Translational sense inventories

TL oriented sense inventories for multilingual WSD are usually built-up from parallel multilingual corpora. The translations of the polysemous words are obtained by automatic word alignment of the source and target versions of a corpus. Word senses are either single translations or clusters of translations. The best example of using such a sense inventory is the Cross-Lingual WSD task in the SemEval-2 (Lefever and Hoste, 2009) and in the forthcoming SemEval-3 exercises. The test datasets were then manually annotated by native speakers with manually built clusters of TL translations.

Advantages. From the theoretical point of view, this method makes sense both in terms of motivations and in terms of ressources' availability. On one hand, the senses are well-motivated : they are completely applicationoriented, the senses are differentiated only when they are lexicalized with different words in the TL. And since the sense inventory is extracted from the corpus, the senses are attested in the datasets (Edmonds and Kilgariff, 2002). On the other hand, there is no need for predefined sense inventories and the annotated corpora can be built automatically, which is one great benefit for this approach.

Drawback. From the computational point of view, the drawback of this approach arises from the fact that the sense are differentiated on the basis of cross-linguistic evidence whilst the task of WSD itself consists in identifying the correct sense of a word by using 'distributional' evidence from its context, typically syntactic and semantic information. Cross-lingual sense distinctions do not necessarily correspond with distributional sense distinctions. So assigning the same cross-lingual sense label to contexts with different distributional characteristics (contexts that represent different SL senses) affects the homogeneity of the description of this sense in terms of linguistic features. This leads to an increase in the task difficulty.

For example, two senses of the French verb comprendre are used in Nous comprenons votre inquiétude and in Les personnes qui commettent des fraudes doivent comprendre qu'elles seront poursuivies. Both occurrences of this verb can be translated to English as understand :

We understand your concerns and People need to understand that if they commit fraud they will be prosecuted (respectively). So, besides the translation, a WSD system would need more information in order to annotate correctly those two occurrences.

Lexicon-style sense inventories

A novel approach to sense inventory definition for WSD have been proposed by Abend et al. (2007), Chen and Di Eugenio (2010) and Brown et al. (2011). They experimented WSD as the task of classifying verb instances into their entries in VerbNet (Kippler-Schuler et al., 2007), the largest verb lexicon currently available for English. VN extends Levin's (1993) verb classification both in coverage and in the verbs' description. It is the most similar ressource to the LG tables. Those experiments reported results that overcome the state-ofthe-art of WSD with cross-lingual sense distinctions.

Advantages. The senses here are characterized exclusively by means of the syntactic and semantic characteristics of the SL contexts in which they are use. And since the task of WSD is to identify the correct meaning by using typically this kind of information about the context, this approach is more convenient, from the computational point of view.

For example, in the two sentences of the example of section 2.1, the two senses would be described by 2 SCFs : when used in the first sense, the verb selects a direct object (votre inquiétude) or a subjonctive clause complement whilst it selects an indicative clause complement (qu'elles seront poursuivies) in the second sense. Modeling such kinds of information in a feature space representation that would be used to train a WSD system can be done by using a syntactic parser.

Drawback.

Sense distinctions based on contextual information in the SL may be too coarse-grained. Gale et al. (1993) illustrate this kind on semantic ambiguity with the English verb 'wear' which is translated to Japanese with 5 different words depending of what part of the body is involved.

A new semantically annotated corpus for WSD

As a remedy to the deficiences of the cross-lingual and the lexicon-style sense labels, we have constructed a new corpus for 20 French polysemous verbs. First, we have built 4 different sense inventories for every verb : the list of its actual translations in a parallel corpus, its entries in the Lexicon-Grammar tables, and two sense inventories automatically generated by combining the two firsts. Then each verb instance have been assigned 4 sense labels, one from every sense inventory.

In the 2 next subsections, we describe the 20 polysemous verbs and the construction of their corpora. The 4 following subsections describe our 4 sense inventories and our method for data annotation.

Corpus construction

We have built a corpus for the 20 French polysemous verbs listed in the table 1 below. Those verbs have been selected on the basis of their polysemy during the ARCADE campaign (2000) for the evaluation of multilingual word alignment systems. arrêter, comprendre, conclure, conduire, connaître, couvrir, entrer, exercer, importer, mettre, ouvrir, parvenir, passer, porter, poursuivre, présenter, rendre, répondre, tirer, venir For the construction of the corpus, we have used the EuroParl-Intersection corpus (Koehn, 2005), a multilingual corpus in which every sentence is aligned with its translations in 6 different languages. We have aligned the French (our SL) and the English (our TL) versions of this corpus at the word level with the GIZA++ tool (Och and Ney, 2003). And then, from the French version, we have extracted all the contexts in which one of the 20 polysemous verbs occurs along with their translation in the English version.

With GIZA++, a single token can be aligned with a sequence of one or more TL tokens but the inverse is not allowed (i.e. aligning a sequence or SL tokens with a TL token). So we have performed two word alignments : one from SL to TL (fr-en) and one from TL to SL (en-fr). And we have eliminated all the couples of contexts in which the TL word aligned with the polysemous verb in the enfr alignment did not appear in the words aligned with it in the fr-en alignment. For example, the following sentence is a context of the verb comprendre :

(2) Fr: Les personnes commettant des fraudes doivent comprendre qu'elles seront poursuivies. En: People need to understand that if they commit fraud they will be prosecuted.

The fr-en and en-fr alignments have provided, respectively, the couples (comprendre -understand) and (understand -comprendre). So understand has been considered as a possible translation of comprendre. In another context of comprendre, the two alignments have provided the couples (comprendre -find) and (incomprehensible -comprendre pas). So find has been considered as a non valid translation of comprendre.

After that, the translations have been validated manually.

The translational sense inventory

Sense inventory. We have built for every polysemous verb a translational sense inventory : its TL translations obtained from the word alignment of its SL and TL contexts.

Data annotation.

Annotating the corpora with this sense inventory was done automatically and validated manually. For example, the following occurrence of the verb comprendre has been assigned the label understand :

(3) Fr: C'est inadmissible et je comprends l'impatience des personnes qui exigent le remplacement de ces instruments par un procureur européen commun. En: It is simply too bad, and I can well understand why people are becoming impatient and demanding that we have a common European Public Prosecutor's Office instead.

The lexicon-style sense inventory

Sense inventory. We have also built a lexicon-style sense inventory by using the Lexicon-Grammar tables, which is currently one of the major sources of syntactic lexical information for the French language.

The Lexicon-Grammar is organised into a series of tables, each of them grouping lexical items which share a certain number of defining features. The verbs belonging to the same table form a syntactically and semantically coherent class. The underlying assumption in the Lexicon-Grammar (LG) is that entry distinctions correspond to sense distinctions. The verb entries are described in terms of syntactic and semantic features. Each verb has as many entries in the LG tables (sometimes in the same table) as it has different possible senses. For the data annotation, we have denoted a verb entry as {V,C}_table_entry where the C (or V) letter means that the verb is in a table that contains idiomatic expressions (or not, resp.), table is the name of a table and entry is the unique identifier of the verb in this table .   For example, the French verb comprendre [understand, comprise]

The fine-grained sense inventory

Sense inventory. We have generated two new sense inventories by merging automatically the translations and the LG entries. For every context in the corpus we have concatenated its LG entry and its translation labels in the form of LG#translation. Data annotation. The example of section 2.2 have been labeled as V_12_17#understand.

The clustered fine-grained sense inventory

Sense inventory. The labels from the third sense inventory have also been clustered automatically by LG entry : all sense labels involving the same LG entry (i.e. all its possible translations) belong to the same cluster. Data annotation. The contexts have been automatically assigned the same cluster as their label from the third sense inventory.

The clustered fine-grained sense inventory

Conclusion

We have built a new sense tagged corpus with 4 sense inventories based on different kinds of evidence. First, we have annotated our corpus with a sense inventory in which sense distinctions are based on cross-lingual evidence: the TL translations. The level of granularity in such sense inventory may not be appropriate for NLP applications. As a solution, we have annotated our corpus with a second sense inventory in which sense distinctions are based on syntactic-semantic evidence: the LG entries. This sense inventory also poses a problem of sense granularity. So we have combined those two sense inventories into two new sense inventories that combine cross-lingual and syntactic-semantic evidence for sense distinction. In the 3 rd sense inventory, each LG sense is split into as many fine-grained senses as it has possible translations, and each TL translation is split into as many fine-grained senses as it has possible corresponding SL senses (LG entries). Finally, from this 3 rd sense inventory, we have built a 4 th one by clustering automatically the TL translations that correspond to the same LG entry.

Table 1 :

 1 The test French polysemous verbs

  has 9 entries in 9 different tables. The 9 examples above illustrate them. The data annotation with this sense inventory was manual. The example above (section 2.2) was labeled V_12_17 : a non idiomatic expression, the 17 th entry in table 12.

	Ce livre comprend dix chapitres
	This book comprises ten chapters
	(8) V_32R3_178
	Max comprend (cette langue + l'anglais)
	Max understands this language
	(9) V_38LR_48
	Le garçon comprend le service dans la note
	The boy includes the service in the note
	(10) V_38R_54
	Max a compris cette remarque comme une
	plaisanterie
	Max has understood this remark as a joke
	(11) V_31H_124
	Max se comprend quand il dit cela
	Max knows what he is trying to say
	(12) C_c7_49
	$ne comprendre$ rien
	to have no clue
	Data annotation.
	(4) V_6_73
	Max a compris qu'Ida était coupable à cet
	indice
	Max has understood that Ida was guilty from
	this indication
	(5) V_10-46
	Faire ce travail comprend pour Max qu'il
	nettoie tout
	To make this work includes for Max that he
	cleans everything
	(6) V_12_17
	Max comprend qu'Ida ne vienne pas
	Max understands that Ida does not come
	(7) V32NM_26

Table 2 :

 2 Table 1 is a statistic description of the sense tagged corpus: the sample size and the number of senses in each sense inventory for each word. Target words samples size and number of senses in each of their 3 first sense inventories

					Num
		Num	Num	Num	LG#TRS
	Target words	samples	LG	TRSL	L
	arrêter	2033	12	150	242
	comprendre	8240	8	183	308
	conclure	3488	5	79	122
	conduire	2114	10	96	145
	connaître	5786	14	158	238
	couvrir	2183	16	85	128
	entrer	2325	6	107	189
	exercer	1851	4	86	120
	importer	2778	5	71	101
	ouvrir	2656	17	127	253
	parvenir	7469	3	152	185
	porter	3301	20	219	495
	poursuivre	5354	5	154	219
	rendre	6731	14	177	347
	tirer	2163	19	102	160
	venir	7369	12	120	306
	Overall mean	3837	11	129	222

We have annotated a corpus with those 4 sense inventories for 20 French polysemous verbs and we plan to create a similar corpus for 20 French polysemous nouns and 20 adjectives.

Omri Abend, Roi Reichart and Ari Rappoport. 2008


Sandrine Blazy
email: sandrine.blazy@irisa.fr

Roberto Giacobazzi
email: roberto.giacobazzi@univr.it

Towards a formally verified obfuscating compiler

This paper extends the idea of specializing modified interpreters for systematically generating obfuscated code. By using the Coq proof assistant we specify some elementary obfuscations and prove that the resulting distorted interpreter is correct, namely it preserves the intended semantics of programs. The paper shows how the semantic preservation proofs generated and verified in Coq can provide a measure of the quality of the obfuscation. In particular we can observe that there is a precise corresponding between the potency of the obfuscation and the complexity of the proof of semantics preservation. Our obfuscation can be easily integrated into the CompCert C compiler, providing the basis for a formally verified obfuscating compiler which can be applied to any C program.

I. INTRODUCTION

Code obfuscation is emerging as a key asset in security by obscurity, in particular for intellectual property protection and for hiding secrets (e.g., keys or watermarks) in source or compiled code [START_REF] Collberg | Watermarking, tamper-proofing, and obduscation-tools for software protection[END_REF]. Results on the impossibility of perfect and universal obfuscation, such as [START_REF] Barak | On the (im)possibility of obfuscating programs[END_REF], did not dishearten researchers and practitioners in developing methods and algorithms for hiding sensitive information in programs (see [START_REF] Collberg | Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection[END_REF] for a comprehensive survey). In particular, in contrast with cryptography which provides provably secure certificates, the lack of a provably secure obfuscation method has pushed the interest in designing obfuscating algorithms that resist to attacks for a sufficient amount of time to keep valid the secret until a new version of the same software is released. Among the grand challenges in code obfuscation addressed in [START_REF] Collberg | Toward digital asset protection[END_REF], the systematic and possibly automatic generation of obfuscated code plays a key role. This is largely due to the necessity of producing highly diversified code in a relatively small range of time, in order to foil any attempt to break code security. In this context, software diversity [START_REF] Cohen | Operating system protection through program evolution[END_REF] in conjunction with code obfuscation may result in a winning strategy for code protection, providing different immunity to hide vulnerabilities and enforcing that each instance of the code must be attacked separately, dramatically increasing the effort required for hackers to develop automated attack tools [START_REF] Collberg | Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection[END_REF]. Successful obfuscation should therefore implement meaningful diversity, and be able to generate diversified obfuscated code quickly enough for comparative evaluation.

Recently in [START_REF] Giacobazzi | Obfuscation by partial evaluation of distorted interpreters[END_REF], the authors introduced a systematic and automatic method for generating diversified and obfuscated code by partial evaluation of distorted interpreters. The idea is based on the fact that obfuscating is making an approximate (abstract) interpreter imprecise (incomplete) [START_REF] Giacobazzi | Hiding information in completeness holes -new perspectives in code obfuscation and watermarking[END_REF]. Program understanding is indeed deeply connected with the notion of interpretation. Human in Man-At-The-End (MATE) attacks or automatic program analysis tools employed in reverse engineering are all based on interpreting program execution (control and data flow) in order to understand its behavior and extract its properties. Therefore, obfuscating is distorting the attacker in order to deceive its interpretation. In [START_REF] Giacobazzi | Obfuscation by partial evaluation of distorted interpreters[END_REF] this is implemented by designing a distorted interpreter for the given programming language such that when it is partially evaluated with respect to the input program P it returns a transformed program Q which is semantically equivalent to P yet inheriting the programming style of the distorted interpreter. Interpreter distortion can be done by making residual in the specialization process sufficiently many interpreter operations to defeat an attacker in extracting sensible information from transformed code. In particular, the distortion is in such a way that a given attacker, which is an abstract interpreter (see [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]), loses information in analyzing Q [START_REF] Giacobazzi | Hiding information in completeness holes -new perspectives in code obfuscation and watermarking[END_REF]. The use of abstract interpretation provides a model for the attacker which is parametric on its ability to extract properties about program behavior, i.e., its precision. This approach has the advantage of specifying code protection by obfuscation as a two player game that turns around the notion of interpretation: The attacker is an approximate interpreter that is devoted to extract properties of the behavior of a program and the defender disguises sensitive properties by distorting code interpretation, making the attacker blind.

In this paper we go beyond this construction and specify both the standard (attacking) and the distorted (protecting) interpretation underlying a given obfuscation strategy inside a theorem prover. We consider Coq [START_REF]The Coq proof assistant[END_REF], [START_REF] Leroy | Formal certification of a compiler back-end or: programming a compiler with a proof assistant[END_REF] as proof assistant, providing a formal language to write mathematical definitions, executable algorithms, and theorems together with an environment for semi-interactive development of machinechecked proofs. The advantage of this approach is twofold: (1) it is possible to generate a provably correct distorted interpreter that, once specialized, will return an obfuscated program which is semantically equivalent to the original one [START_REF]Formal verification of a realistic compiler[END_REF], and (2) the proof of correctness encodes precisely the efforts that an attacker has to make in order to de-obfuscate the program. We show this by three simple examples dealing with data-obfuscation [START_REF] Drape | Specifying imperative data obfuscations[END_REF] and layout obfuscation by variable renaming in a simple imperative language called IMP. We observe that the while the structure of the equivalence proof in the case of layout obfuscation is straightforward, this is Arithmetic expr.: a ::= id not the case in data-obfuscation. In particular the structure of the lemmas necessary for proving semantics equivalence between source and obfuscated code corresponds precisely to the deep understanding of the de-obfuscation strategy, which is straightforward in the case of layout obfuscation by variable renaming. It is therefore possible to map obfuscating algorithms and techniques into proofs in Coq, in such a way that the more complex is the proof of semantics equivalence and the more potent is the obfuscation. The results presented in this paper are in this perspective preliminary towards the development of a formally verified obfuscating compiler based on the idea of obfuscating programs by distorting interpreters.

variable identifier | n integer constant | a 1 + a 2 addition | a 1 -a 2 subtraction | a 1 * a 2 multiplication | a 1 /

II. SYNTAX AND SEMANTICS OF IMP

IMP [START_REF] Winskel | The formal semantics of programming languages: an introduction[END_REF] is a classical small imperative language. It consists of arithmetic and boolean expressions, and statements. Its syntax is given in figure 1.

The dynamic semantics of IMP is written using a bigstep operational style. The semantics is defined by the 3 following judgements with respect to a memory M mapping variables into values. The semantics rules are given in figures 2 (evaluation of expressions) and 3 (execution of statements).

⊢ M, a : v (evaluation of arithmetic expressions) ⊢ M, b : v (evaluation of boolean expressions) ⊢ M, s ⇓ M ′ (execution of statements)
In the following, for functions returning "option" types, ⌊x⌋ (read: "some x") corresponds to success with return value x, and / 0 (read: "none") corresponds to failure. x ? denotes an optional occurrence of x.

Values:

v ∈ Z ∪ Bool Memory:

M ::= id → v ? map from variables to values Update: M[id → v] = M ′ update M with value v for id Arithmetic expressions: ⊢ M, n : n (1) M(id) = ⌊v⌋ (2) ⊢ M, id : v ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 (3) ⊢ M, a 1 + a 2 : v 1 + v 2 ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 (4) ⊢ M, a 1 -a 2 : v 1 -v 2 ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 (5) ⊢ M, a 1 * a 2 : v 1 * v 2 ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 v 2 ̸ = 0 (6) ⊢ M, a 1 / a 2 : v 1 /v 2
Boolean expressions:

⊢ M, TRUE : true (7) ⊢ M, FALSE : false (8) ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 v 1 = v 2 (9) ⊢ M, a 1 == a 2 : true ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 v 1 ̸ = v 2 (10) ⊢ M, a 1 == a 2 : f alse ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 v 1 ≤ v 2 (11) ⊢ M, a 1 <= a 2 : true ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 v 1 > v 2 (12) ⊢ M, a 1 <= a 2 : f alse ⊢ M, a : v (13) ⊢ M, ! a : negb(v) ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 (14) ⊢ M, a 1 && a 2 : v 1 &v 2
⊢ M, skip ⇓ M (15) ⊢ M, a : v (16) ⊢ M, (id = a) ⇓ M[id → v] ⊢ M, s 1 ⇓ M 1 ⊢ M 1 , s 2 ⇓ M 2 (17) ⊢ M, (s 1 ; s 2 ) ⇓ M 2 ⊢ M, b : true ⊢ M, s 1 ⇓ M ′ (18) ⊢ M, if b then s 1 else s 2 ⇓ M ′ ⊢ M, b : false ⊢ M, s 2 ⇓ M ′ (19) ⊢ M, if b then s 1 else s 2 ⇓ M ′ ⊢ M, b : false (20) ⊢ M, while(b)s ⇓ M ⊢ M, b : true ⊢ M, s ⇓ M 1 (21) ⊢ M, while(b)s ⇓ M 1
Fig. 3. Big-step semantics for IMP consists only in obfuscting its arithmetic expressions. In the same way, obfuscating a statement consists only in obfuscating its expressions.

A. A first distorted semantics for IMP

As all integer values are modified by the obfuscation, obfuscated values are stored in memory. Thus, a distorted semantics is required to evaluate obfuscated programs (in an obfuscated memory). The distorted semantics associated to the obfuscation on integer constants is defined by the 3 following judgements. They use values and memories that are defined on top of figure 5.

⊢ M, a ̸ : v (distorted evaluation of arithmetic exp.) ⊢ M, b ̸ : v (distorted evaluation of boolean exp.) ⊢ M, s ̸ ⇓M ′ (distorted execution of statements)
The distorted semantic rules are detailed in figure 5. The only difference with respect to the IMP semantics is in the evaluation of binary expressions. In a binary arithmetic expression, the binary operator is first applied to both deobfuscated values, then the resulting value is obfuscated. In a binary boolean expression, as integer values are obfuscated, these values must be deobfuscated before applying any binary operator comparing integer values. Boolean values are not obfuscated, and thus they do not need to be deobfuscated.

Exactly as in the standard semantics, the execution of statements relies on the evaluation of arithmetic and boolean expressions.

B. Semantic preservation

The following theorems state that the integer obfuscation preserves the semantics of arithmetic expressions: given a Arithmetic expression obfuscation:

O aexp (n) = O val (n) O aexp (id) = id O aexp (a 1 ⊙ a 2 ) = O aexp (a 1 ) ⊙ O aexp (a 2 ) ⊙ ∈ {+, -, * , /} Boolean expression obfuscation: O bexp (TRUE) = TRUE O bexp (FALSE) = FALSE O bexp (a 1 • a 2 ) = O aexp (a 1 ) o O aexp (a 2 ) • ∈ {==, <=} O bexp (b 1 && b 2 ) = O bexp (b 1 ) & O bexp (b 2 ) O bexp (!(b)) = !O bexp (b) Statement obfuscation: O stmt (SKIP) = SKIP O stmt (id = a) = (id = O aexp (a)) O stmt (s 1 ; s 2 ) = O aexp (s 1 ) ; O aexp (s 2 ) O stmt (if (b) then s 1 = if (O bexp (b)) then else s 2 ) O stmt (s 1 ) else O stmt (s 2 ) O stmt (while (b) s) = while (O bexp (b)) O stmt (s)
D mem . Thm 1: ⊢ M, a : v ⇒ ⊢ O mem (M), O aexp (a) ̸ : O val (v)
Reciprocally, given a memory M and an expression a, if a evaluates to a value v wrt. M in the distorted semantics, then in the standard semantics, the corresponding deobfuscated expression evaluates to the corresponding deobfuscated value in the corresponding deobfuscated memory.

Thm 2: ⊢ M, a ̸ : v ⇒ ⊢ D mem (M), D aexp (a) : D val (v)
Let us note that we could have written the two previous theorems as the following theorem. In the sequel of this paper, we will use theorems such as the following one to state the semantic preservation of an obfuscation.

Thm 3: ⊢ M, a : v ⇔ ⊢ O mem (M), O aexp (a) ̸ : O val (v)
In the same way, both of the following theorems state that the integer obfuscation preserves the semantics of boolean expressions and statements.

Thm

4: ⊢ M, b : v ⇔ ⊢ O mem (M), O bexp (b) ̸ : O val (v) Thm 5: ⊢ M, s ⇓ M ′ ⇔ ⊢ O mem (M), O stmt (s) ̸ ⇓O mem (M ′ )
The proof that the integer obfuscation preserves the semantics proceeds classically by induction on the execution relation. This proof relies on the following intermediate lemmas. The first lemma relates a memory and its corresponding obfuscated Arithmetic expressions:

⊢ M, n ̸ : n (22) M(id) = ⌊v⌋ (23) ⊢ M, id ̸ : v ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 (24) ⊢ M, a 1 + a 2 ̸ : O val (D val (v 1 ) + D val (v 2 )) ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 (25) ⊢ M, a 1 -a 2 ̸ : O val (D val (v 1 ) -D val (v 2 )) ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 (26) ⊢ M, a 1 * a 2 ̸ : O val (D val (v 1 ) * D val (v 2 )) ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 v 2 ̸ = 0 (27) ⊢ M, a 1 / a 2 ̸ : O val (D val (v 1 )/D val (v 2 ))
Boolean expressions:

⊢ M, TRUE ̸ : true (28) ⊢ M, FALSE ̸ : false (29) ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 D val (v 1 ) = D val (v 2 ) (30) ⊢ M, a 1 == a 2 ̸ :true ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 D val (v 1 ) ̸ = D val (v 2 ) (31) ⊢ M, a 1 == a 2 ̸ : f alse ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 D val (v 1 ) ≤ D val (v 2 ) (32) ⊢ M, a 1 <= a 2 ̸ :true ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 D val (v 1 ) > D val (v 2 ) (33) ⊢ M, a 1 <= a 2 ̸ : f alse ⊢ M, a ̸ : v (34) ⊢ M, ! a ̸ : negb(v) ⊢ M, a 1 ̸ : v 1 ⊢ M, a 2 ̸ : v 2 (35) ⊢ M, a 1 && a 2 ̸ : v 1 &v 2 Statements: ⊢ M, skip ̸ ⇓M (36) ⊢ M, a ̸ : v (37) ⊢ M, (id = a) ̸ ⇓M[id → v] ⊢ M, s 1 ̸ ⇓M 1 ⊢ M 1 , s 2 ̸ ⇓M 2 (38) ⊢ M, (s 1 ; s 2 ) ̸ ⇓M 2 ⊢ M, b ̸ : false (39) ⊢ M, while(b)s ̸ ⇓M ⊢ M, b ̸ : true ⊢ M, s ̸ ⇓M 1 (40) ⊢ M, while(b)s ̸ ⇓M 1
(id) = ⌊v⌋ ⇔ O mem (M)(id) = ⌊O val (v)⌋
The next lemmas state that the sequencing between an update in memory and an obfuscation (resp. a deobfuscation) can be modified without changing memory.

Lm 7:

O mem (M[id → v]) = O mem (M)[id → O val (v)] Lm 8: D mem (M[id → v]) = D mem (M)[id → D val (v)]
It is worth noting the structure of intermediate lemmas 6-7. They specify precisely the commuting property of obfuscation and de-obfuscation with respect to the main semantic operators and constructions of IMP (viz., memory, variable substitution etc.). The understanding of these properties correspond indeed precisely to the understanding of how the obfuscated program is constructed out of its source version, and it is in this perspective the core of any de-obfuscating interpretation.

IV. VARIABLE ENCODING

The second obfuscation is also a data-obfuscation as introduced in [START_REF] Drape | Specifying imperative data obfuscations[END_REF] and it is defined in figure 6. In each expression of a program, it replaces each occurrence of any variable id by the arithmetic expression id * n, where n is a constant such that n > 0. The inverse (deobfuscation) function replaces an arithmetic expression a by the arithmetic expression a/n. Thus, in arithmetic expressions, only variables are obfuscated. Boolean expressions are obfuscated as in the previous obfuscation, thus the corresponding function is not shown in the figure .  In statements, only assign statements are obfuscated differently (compared to the first obfuscation). In an assign statement such as id = a, the expression a is obfuscated (i.e. each occurence of each variable id is replaced by id * n) and then the resulting expression is deobfuscated (i.e. the expression is divided by n). Thus, the expression a remains unchanged after the obfuscation only when there is only one occurrence of a single variable in a. The left hand side of the assign statement is never obfuscated.

A. Semantic preservation

No distorted semantics is required to evaluate obfuscated expressions or to execute obfuscated programs: the semantics preservation theorems rely only on the standard semantics of IMP. As a consequence, another difference with respect to the previous obfuscation is in both of the following main theorems related to expressions: the value of an obfuscated expression is also the value of the original expression.

Moreover, the proof of the theorem related to boolean expressions is exactly the same as the proof of the corresponding theorem in the first obfuscation. As the specification language of Coq is a higher-order functional language (and logic), the Coq development is modular, and some proofs can be directly reused.

Thm 9: ⊢ M, a : v ⇔ ⊢ O mem (M), O aexp (a) : v Thm 10: ⊢ M, b : v ⇔ ⊢ O mem (M), O bexp (b) : v
The theorem stating that the obfuscation of statements preserves the semantics is the same as for the first obfuscation.

Thm 11:

⊢ M, s ⇓ M ′ ⇔ ⊢ O mem (M), O stmt (s) ⇓ O mem (M ′ )
Elementary obfuscation:

n ∈ Z + O var (id) = n * id D aexp (a) = a/n Arithmetic expr. obfuscation: O aexp (n) = n O aexp (id) = O var (id) O aexp (a 1 ⊙ a 2 ) = O aexp (a 1 ) ⊙ O aexp (a 2 ) ⊙ ∈ {+, -, * , /} Statement obfuscation: O stmt (SKIP) = SKIP O stmt (id = a) = (id = D aexp (O aexp (a))) O stmt (s 1 ; s 2 ) = O stmt (s 1 ) ; O stmt (s 2 ) O stmt (if (b) then s 1 ) = if (O bexp (b)) then O stmt (s 1 ) else s 2 else O stmt (s 2 ) O stmt (while (b) s) = while (O bexp (b)) O stmt (s)
Fig. 6. Variable encoding: a first obfuscation of variables Moreover, the only intermediate lemmas that are required to prove the semantic preservation are those previously used for the first obfuscation. Thus, no new intermediate lemma is required here. This means that the two obfuscations are indeed equivalent from the point of view of the necessary intermediate lemmas in order to prove the equivalence of the source and obfuscated code. Moreover, we can observe that the second obfuscation is slightly better than the first one, because the main theorem for expressions is not the expected theorem.

V. LAYOUT OBFUSCATION: RENAMING VARIABLES

Layout obfuscation is considered a straightforward obfuscation strategy [START_REF] Collberg | Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection[END_REF]. It deals with the way code (variables and statements) are written and it is, under this perspective, relatively easy to de-obfuscate. Given an obfuscation function O rename : ident → ident, this obfuscation renames in every expression every occurrence of a variable identifier id into O rename (id). The O rename function is reversible. Its inverse function is called D rename . We thus have the following axiom called Axm 2: ∀v,

D rename (O rename (v)) = v.
The obfuscation is detailed in figure 7. As in the first obfuscation, the only obfuscations of a boolean expression or a statement that is not an assignment are the obfuscations of arithmetic expressions. Thus, the corresponding functions are similar to those of figure 4, and they are not shown on figure 7.

A. A second distorted semantics for IMP

Variable renaming requires a distorted semantics that is defined on figure 8. Its judgements are those of the previous distorted semantics defined in figure 5. However both semantics are different. Here, only the evaluation of a variable and Arithmetic exp. obfuscation: the execution of assignments are distorted to express that the variable is deobfuscated before accessing the memory.

O aexp (n) = n O aexp (id) = O rename (id) O aexp (a 1 ⊙ a 2 ) = O aexp (a 1 ) ⊙ O aexp (a 2 ) ⊙ ∈ {+
⊢ M, id : v ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 (43) ⊢ M, a 1 + a 2 : v 1 + v 2 ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 (44) ⊢ M, a 1 -a 2 : v 1 -v 2 ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 (45) ⊢ M, a 1 * a 2 : v 1 * v 2 ⊢ M, a 1 : v 1 ⊢ M, a 2 : v 2 v 2 ̸ = 0 (46) ⊢ M, a 1 / a 2 : v 1 /v 2 Assign statements: ⊢ M, a ̸ : v (47) ⊢ M, (D rename (id) = a) ̸ ⇓M[id → v]
More precisely, the value of a renamed variable is the value of the deobfuscated variable. In the same way, executing an assignment updates the value of the deobfuscated variable. As in the standard semantics, the evaluation of a boolean expression relies on the evaluation of an arithmetic expression, and the execution of other statements relies on the evaluation of its expressions. Thus, the corresponding rules are not shown in the figure.

B. Semantic preservation

Only variable occurences are renamed. The memory is not obfuscated. Thus, the semantic preservation follows from the three following theorems.

Thm 12: ⊢ M, a : v ⇔ ⊢ M, O aexp (a) ̸ : v Thm 13: ⊢ M, b : v ⇔ ⊢ M, O bexp (b) ̸ : v Thm 14: ⊢ M, s ⇓ M ′ ⇔ ⊢ M, O stmt (s) ̸ ⇓M ′
No intermediate lemma is required to prove the above theorems. Only the axiom Axm 2 defined previously is required. In this perspective, the Coq proof assistant does not need extra knowledge in order to prove equivalence of the obfuscated code relatively to the source one. This formally justifies the intrinsic simplicity of variable renaming with respect to the more sophisticated data-obfuscations developed above.

VI. CONCLUSION AND FUTURE WORKS

In this paper, we have formally defined the semantics of a simple imperative language as well as three elementary obfuscations on this language. The idea is simple: use Coq as a standardized proof assistant and provide within Coq a proof of equivalence between source and obfuscated programs. The comparison between the proofs provided by different obfuscation methods gives a deep understanding of their relative potency and effectiveness.

For two of these obfuscations, we have formally defined a dedicated distorted semantics that foils the attacker. We also have formally verified using the Coq proof assistant that our obfuscations preserve the semantics of programs, and we have given the intermediate lemmas that were required for these proofs. Interestingly, these lemmas, as constructed within the Coq proof assistant, specify precisely the intended steps necessary for reversing the obfuscation. Therefore by comparing the structure of the proofs of equivalence generated within Coq it is possible to devise a qualitative measure for the potency of the obfuscating transformation.

Our Coq development is modular, and therefore different obfuscations can be combined in order to generate new obfuscations. As future work, we intend to formalize more obfuscations and to reuse parts of our distorted semantics and of our proofs. In particular we are interested in mixing elementary transformations in order to design more complex obfuscations as the composition of simpler ones. This would be particularly effective when context sensitive transformations, i.e., transformations that depend upon the structure of data and control flow of the program, are combined. This would result in a highly intricate control/data flow of the obfuscated code, yet keeping semantics equivalence. Moreover, it is relatively straightforward to extend our approach to the obfuscation for the entire C language, by adapting proofs to the semantics of the C language within the formally verified CompCert C compiler [START_REF] Blazy | Mechanized semantics for the Clight subset of the C language[END_REF]. CompCert is formally verified using Coq. This means that the executable code it produces is proved to behave exactly as prescribed by the semantics of its corresponding source C program. In this case, a machine 32-bit integers instead of integer value belonging to Z, should be considered. Once our obfuscations will be integrated into CompCert, we will thus have for free a semantic preservation theorem between an executable program and its corresponding obfuscated program.

Fig. 2 .

 2 Fig. 2. Big-step semantics for IMP

Fig. 4 .

 4 Fig. 4. Integer encoding

Fig. 5 .

 5 Fig. 5. Distorted semantics associated to integer constants obfuscation

Fig. 7 .

 7 Fig. 7. Variable renaming: a second obfuscation of variables Arithmetic expressions: ⊢ M, n : n (41) M(D rename (id)) = ⌊v⌋ (42)

Fig. 8 .

 8 Fig. 8. Distorted semantics associated to the renaming of variables