Laure Gonnord

Nicolas Halbwachs

Nicolas Halbwachs Verimag

Nicolas Halbwachs}

Abstract acceleration in Linear relation analysis

Keywords: Program analysis, linear relation analysis, polyhedra, widening, acceleration. Reviewers: reviewer1, reviewer2

Introduction

Linear Relation Analysis [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF] (LRA) is one of the very first applications of abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. It aims at computing an upper approximation of the reachable states of a numerical program, as a convex polyhedron (or a set of such polyhedra). It was applied in various domains like compile-time error detection [START_REF] Dor | Cleanness checking of string manipulations in C programs via integer analysis[END_REF], program parallelization [START_REF] Irigoin | Semantical interprocedural parallelization: An overview of the PIPS project[END_REF], automatic verification [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF][START_REF] Henzinger | Hytech: A model checker for hybrid systems[END_REF] and formal proof [START_REF] Bjorner | Verifying temporal properties of reactive systems: A STeP tutorial[END_REF][START_REF] Bjorner | Automatic generation of invariants and intermediate assertions[END_REF].

Like any approximate verification method, LRA is faced with the compromise between precision and cost. Since its relatively high cost restricts its applicability, any situation where the precision can be improved at low cost must be exploited. One source of approximation in LRA is widening, an operation that ensures the termination of iterative computations, by extrapolating an upper approximation of their limits.

Improving the precision of the result of widened iterations has motivated so many works that we will devote a whole section to their survey. Some authors propose better widening operators, while others consider the way the widening is applied. The first track raises the question of "what is a better widening?". The fact that one single application of a widening operator gives smaller results does not necessarily mean that its repeated application will involve a convergence towards a more precise limit. Moreover, such "more precise" widenings, and the use of many proposed application policies -like delaying the wideningare likely to slow down the convergence, by increasing the number of necessary iterations.

These remarks led us to look at situations where the widening can obviously be improved -in the sense that it involves a faster convergence towards a better limit -at low cost with respect to the cost of usual polyhedra operators. A source of inspiration are the so-called "acceleration techniques" proposed by several authors [START_REF] Boigelot | Symbolic verification with periodic sets[END_REF][START_REF] Wolper | Verifying systems with infinite but regular state spaces[END_REF][START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Finkel | An algorithm constructing the semilinear post* for 2-dim reset/transfer vass[END_REF]7]. These works consist in identifying categories of loops whose effect can be computed exactly. Roughly speaking, the effect of a simple loop, guarded by a linear condition on integer variables, and consisting of incrementations/decrementations of these variables can be computed exactly as a Presburger formula. These methods have the advantage of giving exact results. Now, because they are exact, they are restricted to some classes of programs (e.g., "flat counter automata", i.e., without nested loops). Moreover, the exact computation with integer variables has a very high complexity (2EXP). So the applicability of these methods is somewhat limited.

In this paper, we investigate on the use of acceleration methods in LRA, in complement to widening. Of course, when the effect of a loop can be computed exactly (and at low cost) there is no need to approximate it. Now, since we want to integrate these results in LRA, only the exact abstract effect of the loop is necessary, that is the convex hull of the reachable states during or after the loop. This means that we won't use expensive computations in Presburger arithmetic. Moreover, we only look for an improvement of standard LRA: wherever an acceleration is possible, its application will improve the results, but the resulting method is not restricted to those programs where acceleration applies everywhere.

The paper is organized as follows: After a reminder of the principles of LRA (Section 2), Section 3 and Section 4 surveys the existing works about widening and acceleration techniques. Our proposal is introduced by a motivating example in Section 5. Then, Section 6 addresses the trivial case of a single loop where variables are just incremented with constants, and defines the notion of abstract acceleration. In Section 7, we consider the case of several translation and reset loops. We are then able to describe the mechanisms that we implemented in our tool Aspic (Section 8). In Section 9, some experimental results are described, before giving some conclusions. x ≤ 100? x := x + 1 y := y + 1

x ≤ 100?x := x + 2 Then, we can attach with each control point k a polyhedron P k , which is an upper approximation of R k , as follows:

P k = if k = k init then ⊤ else (k ′ ,g,a,k)∈T a ♯ (P k ′ ⊓ g ♯ )
Iterative computations: We are left with a system of fixpoint equations (P k = F k (P 1 , ...P k , ...)) k∈K whose least solution can be computed by iteration from P k = ⊥, ∀k. Of course, this computation will raise the problem of termination. Starting the iterative resolution, we get:

Step Obviously, at step i we will get P 1 = {0 y x 2i -2 -y}, P 2 = {2 x + y 2i, 0 y x}, and the iterations will continue until P 1 intersects {x 101}. Performing this extrapolation at once is the role of the widening operator.

3 Widening in LRA: state of the art

Principles

According to [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], a widening operator on polyhedra is a binary operator ∇ such that • ∀P, Q, P ⊔ Q ⊆ P∇Q • (chain condition) for any sequence P 0 , P 1 , . . . of polyhedra, the sequence Q 0 = P 0 , Q i = Q i-1 ∇P i is not strictly increasing. Let (P k = F k (P 1 , ...P k , ...)) k∈K be a system of fixpoint equations. A widening operator is used to ensure the convergence of iterative computations of fixpoints as follows: Let K ∇ be a subset of K, such that each loop in the program graph contains at least one control point in K ∇ . Then, for each k ∈ K, define F ∇ k by F ∇ k (P 1 , ...P k , ...) = P k ∇F k (P 1 , ...P k , ...) if k ∈ K ∇ F k (P 1 , ...P k , ...) otherwise Then, the iterative computation of the least solution of the system P k = F ∇ k (P 1 , ...P k , ...) k∈K converges after a finite number of steps towards a solution (P ∇ k ) k∈K which is an upper approximation of the least solution of the initial system.

Standard widening

The very first widening operator over polyhedra was proposed in [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]: P 1 ∇P 2 is defined to be the polyhedron whose system of constraints is made of the constraints of P 1 satisfied by P 2 . Moreover, ⊥∇P = P for all P. Since the set of constraints of P 1 ∇P 2 is included in the set of constraints of P 1 , the widening cannot be applied indefinitely without convergence (chain condition).

This initial operator has the drawback that its result depends on the form of the systems of constraints. For instance, in our Example 1, if k 1 is the widening point, at step 2 we have to compute {x = 0, y = 0}∇{0 y x 2 -y}, i.e., {0 x 0, 0 y 0}∇{0 y x 2 -y} which gives simply {0 x, 0 y}. Now, if we rewrite the first system of constraints into the equivalent system {0 y x 0}, the widening evaluates to {0 y x}, which is much more precise. This is why [START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF] proposed a better operator, often referred to as standard widening: it consists of keeping for P 1 ∇P 2 not only the constraints of P 1 satisfied by P 2 , but also the constraints of P 2 mutually redundant with some constraint of P 1 in the system of constraints of P 1 .

In the example before, P 1 is defined by the system of constraints {0 x 0, 0 y 0} and the system of generators V = {(0, 0)}, R = ∅. In the system of constraints of P 2 , {0 y x 2 -y}, y x is saturated by the unique vertex of P 1 , (0, 0), so it is mutually redundant with any constraint of P 1 , and is kept in the widening.

Example 1 (continued): Using the standard widening in our example, we get the following iterations which converge at step 3:

Step 0 1 2 3 P 0 ⊥ ⊤ ⊤ ⊤ P 1 ⊥ {x = y = 0} {0 y x} {0 y x} P 2 ⊥ {x + y = 2, 0 y x} {2 x + y 202, 0 y x 102} {2 x + y 202, 0 y x 102} P 3 ⊥ ⊥ {0 y x, x 101} {0 y x, x 101}

Descending sequence

The first way of improving the results of the widened sequence is the general descending/narrowing method, proposed as early as in [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. It is guaranteed that the solution (P ∇ k ) k∈K is a post-fixpoint of the exact function (F k ) k∈K , i.e., ∀k ∈ K, F k (P ∇ 1 , . . . , P ∇ k , . . .) ⊆ P ∇ k If, for some k, this inclusion is strict, one can improve the solution by iterating the exact function from (P ∇ k ) (i.e., continuing the iterations without widening). These additional iterations are not guaranteed to terminate (unless a narrowing operator is used [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]), but each iterate is a correct approximation of the least fixpoint, meaning that the iterations can safely be stopped at any step.

Example 1 (end): It is the case in our simple example, since

F 1 (P ∇ 0 , P ∇ 2 ) = {0 y x 102, x + y 202} ⊂ P ∇ 1
Continuing the iterations without widening, we get one more iteration which provides a fixpoint and cannot be improved further:

Step

0 1 2 3 P 0 ⊥ ⊤ ⊤ ⊤ P 1 ⊥ {x = y = 0} {0 y x} {0 y x 102, x + y 202} P 2 ⊥ {x + y = 2, 0 y x} {2 x + y 202, 0 y x 102} {2 x + y 202, 0 y x 102} P 3 ⊥ ⊥ {0 y x, x 101} {0 y 202 -x, 101 x 102}
There were two main tracks for reducing the imprecision due to the widening: The first one investigates better widening operators, while the second one consists in proposing widening application strategies.

Improving the widening operator

Parma widening

[6] proposes a general framework to design new widening operators from an existing one. They use the notion of "limited growth" to guarantee the termination of the computations:

P 1 P 2 de f =                    if dim P 2 > dim P 1 or codim(P 2 ) > codim(P 1 )
or ♯cons(P 1 ) > ♯cons(P 2 ) or ♯cons(P 1 ) = ♯cons(P 2 ) and ♯V 1 > ♯V 2 or ♯cons(P 1 ) = ♯cons(P 2 ) and

♯V 1 = ♯V 2 and χ(R 1 ) >> χ(R 2 )
In other words, P 1 P 2 in one of the following cases: • The dimension of P 2 (i.e., the dimension of the least subspace containing P 2 ) is strictly greater than P 1 's dimension; • The codimension of P 2 (the dimension of the largest subspace strictly included in P 2 ) is strictly greater than P 1 's codimension; • The number of constraints of P 1 is strictly greater than the one of P 2 ;

• The number of constraints of P 1 is the same as the one of P 2 , and the number of vertices of P 1 is strictly greater than the one of P 2 ; • P 1 and P 2 have the same number of constraints and vertices, and the multisets χ(R i ) of the non null coordinates of P i 's rays verify χ(P 1 ) >> χ(P 2 ) (multiset classic ordering). This definition guarantees that a sequence (P i ) i∈N where for all i, P i P i+1 is finite ( is a well-founded strict ordering). So, the operator ∇ ′ defined by

P 1 ∇ ′ P 2 = P 1 ⊔ P 2 if P 1 P 2 P 1 ∇P 2 otherwise
where ∇ is the standard widening, is also a widening (the operator proposed in [6] is slightly more complicated), and for any P 1 , P 2 , P 1 ∇ ′ P 2 ⊆ P 1 ∇P 2 .

So, one application of the new widening gives a more precise result. However, there is no guarantee that the limit of the widened sequence will be more precise: most experimental results show an improvement, but there are also counter-examples. Moreover, the cost of the analysis can increase significantly, because the convergence is generally slower.

Limited widening

This technique, called "widening up to" in [START_REF] Halbwachs | Delay analysis in synchronous programs[END_REF][START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF] and "widening with thresholds" in [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], consists in precomputing a set U of constraints that are likely to be invariants in a widening location (e.g., the negation of the exit condition of a "for" loop), and in keeping in P 1 ∇P 2 all the constraints in U which are satisfied by both P 1 and P 2 . In [START_REF] Halbwachs | Delay analysis in synchronous programs[END_REF], the set U is computed, at a given widening point, as the set of all conditions that permit to come back to this control point, by propagating the exiting condition on the global loops. The main drawback of this method is that propagating the exit condition of all loops has an exponential cost. In general, only the preconditions of the exiting transitions are computed.

Example 2: To illustrate the use of this heuristic, we show in Figure 2 an example taken from [START_REF] Halbwachs | Delay analysis in synchronous programs[END_REF]: it models the speedometer of a car, which counts the number t of received "seconds" (time elapsed), the number d of received "meters" (distance covered), and the number s of meters received each second (instantaneous speed). It is assumed that (1) the car stops within 4 seconds, (2) the car crashes into a wall after 10 meters, and (3) the maximum speed is 2 meters per second. The goal is to show that the car stops before crashing, i.e., that the control point k 4 is not reachable.

t := t + 1 t ≤ 2 → s := 0; v ≤ 1, d ≤ 8 → v := v + 1; d := d + 1 Figure 2: Car example Let's choose U k 2 = {s 2, d 9
, t 3} as limiting constraints at the widening point k 2 (these are the postconditions of the guards of the transitions looping on k 2 ). Then, after the first iteration, we have P (1) 2 = {d = 0; t = 0; v = 0}, and at the second iteration we have to compute

P (2) 2 = P (1) 2 ∇{0 d = s 1; 0 t 1; t + d 1}
The standard widening would give P (2) 2 = {0 s = d; 0 t; }, but all the constraints in U k 2 are satisfied by both operands of the widening, so the limited widening gives P (2) 2 = {0 s = d 2; 0 t 3}. At third iteration, we get

P (3) 2 = P (2) 2 ∇{0 s d 2t + s; t 3; d 2} = {0 s d 2t + s; t 3; d 2}
which is a fixpoint, and from which we get P 4 = ⊥ as expected. Notice that the constraint d 2t + s in P (3) 2 is the "speed constraint", which is the key property for this example and is missed by the standard widening.

Widening with landmarks

A similar idea is developed in [START_REF] Simon | Widening Polyhedra with Landmarks[END_REF], which proposes to compute a set of inequalities that are not satisfied while staying in the loop. Unlike the limited widening, this set of constraints is computed dynamically: the computation of the invariant associated to one control point depends on the incoming transitions, and each of these transitions can have a empty contribution. The proposed widening takes into account the guards of these incoming empty transitions, in order to guess when they will be enabled.

In practice, with each widening point is associated a set of landmarks representing a set of non satisfiable inequalities when the control is inside the associated strongly connected subcomponent: these landmarks are of the form < c, d 1 , d 2 > where c is a (non satisfied) constraint, d 1 is the Euclidean distance from the current polyhedron to this constraint, d 2 is the previous distance which is strictly smaller. The design of the widening operator is changed in order to take these landmarks into account: the assumption is that the distance follows an arithmetical law, so we can estimate the number of steps necessary to reach the constraint c; then the algorithm performs an extrapolation of the result of m steps, where m is the minimum of these numbers of steps associated with all considered constraints c .

The main advantage of this method is that it can take some non convex guards like i 0 into account. The drawback is that the dynamic computation of the landmarks is costly, because the computation of the distances makes use of linear programming.

Guiding the widening by a care set

In [START_REF] Wang | Using counterexamples for improving the precision of reachability computation with polyhedra[END_REF], the authors use counterexamples of the property to prove, in order to improve the precision. In fact, they consider the LRA classic process which consists of successive applications of forward and backward iterations. If a forward iterator does not manage to prove the goal formula ψ, then a backward iteration is performed, starting from the polyhedra obtained so far, intersected with ¬ψ. The authors propose to use some information during the backward analysis to get some new constraints that must be avoided in the next forward iteration. Then they propose to use this information in one of the following two ways:

• the first one consists in using the negation of each constraint as an "up-to" constraint, and use the classic limited widening operator. • the second one is to use an extrapolation operator -which does not guarantee the terminationinstead of widening. This extrapolation of P with respect to Q under C is defined by the following algorithm (P,Q,C are polyhedra, P ⊆ Q, C is the "care set", so P ∩ C = ∅ and Q ∩ C = ∅):

-Build a new polyhedron P ′ by dropping from P each constraint c not satisfied by Q, and whose removal does not make P ′ intersect the care set (i.e., such that P \ {c} ∩ C ∅ ). -From Q, drop any constraint c ′ not satisfied by P ′ , and return the obtained polyhedron. The authors claim that the result doesn't intersect the care set C, and is generally smaller than P∇Q. The first solution has the advantage to increase the precision while always guaranteeing the termination. However, this method is guided by a proof goal, and then is only useful in verification. Our goal is to discover better invariants in the general case. This method can also be combined with ours.

Widening strategies

Delaying the application of the widening operator

An obvious way for improving the precision of the limit of the widened sequence is to delay the application of the widening: during the first m steps, the exact function is applied, then the widening is applied to enforce the convergence. The greater the parameter m, the more precise is the limit. For instance, in our Example 1, with the first very rough widening proposed in [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] (cf. Section 3.2), if the widening is applied at once, we get only

P 1 = {x = y = 0}∇{0 y x 2 -y} = {x 0, y 0}
but if it is applied only one step later, we get

P 1 = {0 y x 2 -y}∇{0 y x 4 -y} = {0 y x}
i.e., the result provided by the standard widening without delay. This delaying strategy was proposed in [START_REF] Halbwachs | Delay analysis in synchronous programs[END_REF][START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]. A variant is the loop unrolling technique used in [START_REF] Goubault | Static analyses of the precision of floating-point operations[END_REF][START_REF] Putot | Static analysis-based validation of floating-point computations[END_REF]. Of course, this technique may increase significantly the cost of the analysis, since on one hand it involves additional iterations, but also because the first exact steps of computation generally produce complex polyhedra, which would be simplified by the widening.

New control path

The widening technique assumes some regularity in the behavior of the program: the first iterations in a loop are assumed to allow the widening operator to predict the behavior of further iterations. However, this regularity hypothesis is clearly violated when a path in the loop becomes feasible only after some iterations: the effect of taking this path cannot be predicted before it is taken at least once. As a consequence, when a new path of a strongly connected component becomes feasible at some iteration of the analysis, specific strategies should be applied:

• [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] simply applies least upper bound instead of widening;

• [START_REF] Halbwachs | Delay analysis in synchronous programs[END_REF] proposes to extrapolate the result from the first non empty polyhedron: basically, instead of computing P (n+1)

k = P (n) k ∇F k (P (n) ), one computes P (n+1) k = P (1)
k ∇F k (P (n) ). None of these strategies endangers the termination, since the allowance of a new path can only happen a finite number of times.

Lookahead Widening

The approach proposed in [START_REF] Gopan | Lookahead widening[END_REF][START_REF] Gopan | Guided static analysis[END_REF] tends to subsume both the limited widening and the new path strategy. The main idea is to make a complete analysis (increasing and decreasing) by loop phase. A phase is a period where no new path is being activated.

Intuitively, after a first step of the analysis of a strongly connected component of the control graph, the part of this SCC that has been found feasible is considered alone, and a full -ascending and descending -sequence is computed on this subgraph. Then, from the obtained results, new paths are added if they are found feasible, and a full analysis is performed on this extended graph, and so on, until no new path is found.

The lookahead widening is not guaranteed to give more precise results, but experiments show that it often does, at the price of some additional complexity. It is a valuable method since it can easily be combined with other approaches.

Acceleration techniques for exact computations

Another track of research concerns the exact computation of the reachable states of programs with integer variables, the sets of states being characterized by Presburger formulas. Although some authors in this track also use widening techniques [START_REF] Bultan | Symbolic model checking of infinite state systems using Presburger arithmetic[END_REF]20], most of these works aim at computing reachable states exactly, when possible. For that, the notion of "acceleration" has been introduced, to compute the effect of a loop. For instance, the reachable states at the entry of the loop x:= x0; y:=y0; while x<=100 do {x:=x+2; y:=y+3} can be characterized by the Presburger formula

∃k 0 s.t. x = x0 + 2k ∧ y = y0 + 3k ∧ ∀k ′ , (0 k ′ < k) ⇒ (x0 + 2k ′ 100).
Let us recall some decidability results for the iteration of some classes of transitions, and then describe how they are used in reachability analysis.

Theoretical results

Several results have been obtained in the past 15 years:

• In [START_REF] Boigelot | Symbolic verification with periodic sets[END_REF], the authors use periodic sets in order to represent the reachability sets of integer programs: the tuple (∆, δ, P, q) where ∆, P are (integer) matrices and δ, q are vectors, represents the set { x ∈ Z n ; ∃ k ∈ Z n , such that x = ∆ k + δ and P k q}. Then the authors give an algorithm to compute the exact effect of affine guarded transitions (A x B → x := C x + D) with integer constants on a given input periodic set, but only for the transitions where C 2 = C. • [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] and [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] use an automaton encoding of sets to compute the iteration of a Presburger set by an affine guarded function verifying ∃p, C 2p = C p . In §6.6, we will come back to this algebraic characterization. • [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Comon | Timed automata and the theory of real numbers[END_REF] only consider guards of the form y j #y i + c, where # ∈ {=, <, }, and y i are primed or non primed variables (output and input variables). The actions are of the form x ′ = Cx + d. They give a constructive procedure to compute a Presburger formula on x, x ′ which is true if and only if x ′ ∈ τ * (x). But this procedure has a very high complexity and has not been implemented.

Application to reachability analysis

These results are then used for reachability analysis in the following ways:

• In the Lash tool [START_REF] Lash | [END_REF], the user designates which loops should be accelerated. Then the analysis is performed forward. Termination is not guaranteed but if the analysis succeeds, the result is the exact reachability set. • In [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF], the author's prototype detects if some loop is accelerable, and if so, adds the corresponding meta-transition which subsumes the effect of the whole loop. In the case of two nested loops, the termination is not guaranteed, except for the special case where the internal loop is deterministic, that is, the number of its iterations is completely determined by the initial values of the variables. • The Fast [START_REF]FAST[END_REF] tool uses the UBA (automata to encode integer sets, [START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs -approximation et accélération -implémentation dans l'outil Fast[END_REF]) representation to accelerate Presburger sets. In practice, if all the transitions in the graph loops have a finite associated monoid (see §6.6), then the authors use an enumeration of restricted linear regular expressions (i.e., words of the form u * 1 u * 2 . . . u * p with u i words on the transition alphabet) to enumerate loop paths [9,[START_REF] Bardin | Vers un model checking avec accélération plate de systèmes hétérogènes[END_REF]. If the procedure terminates, then it returns exactly the set of reachable states. It has been shown [9] that the programs for which this procedure terminates are exactly the counter automata that are Lflatable, i.e., such that there exists an equivalent automaton (with respect to the reachability sets) that is flat (i.e., without nested loops). This condition is undecidable. This algorithm has been improved, concerning the enumeration of class paths, and the management of some kinds of nested loops by the union reduction ( [START_REF] Bardin | Vers un model checking avec accélération plate de systèmes hétérogènes[END_REF]). In the Fast tool, the user can provide some help by using graph strategies. All these methods are based on the fact that accelerating single loops is sometimes enough to compute the reachability set. In the general case, there are loops that cannot be accelerated, and above all, general programs contain nested loops that cannot be flattened. In conclusion, these methods have the advantage of being exact. But they involve computations of high complexity in Presburger arithmetic. Moreover, they are restricted to some classes of programs, and cannot be straightforwardly integrated with general methods like LRA.

Motivating example: the gas burner

To motivate our contribution, let us start with a classical example of hybrid system, the "leaking gas burner" [START_REF] Chaochen | A calculus of durations[END_REF]: whenever the gas burner leaks, it is always fixed within 10 seconds, and the minimum interval between two leakages is 50 seconds. The standard modelling of this system is by a linear hybrid automaton [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF][START_REF] Henzinger | Hytech: A model checker for hybrid systems[END_REF] (see Fig. 3). Let us recall the behavior of this model: 3 continuous variablest, counting the absolute time, ℓ counting the global leaking time, and x counting the time elapsed since the last event -are initialized to 0, and initially the gas burner is leaking. In the leaking location, all the variables evolve continuously with unit derivatives: they all count time, as long as the invariant x 10 is satisfied; at any time during this delay, the gas burner can be fixed, in which case the automaton enters the location "not leaking", and x is reset to 0; in the "not leaking" location, the variable ℓ doesn't change (its derivative is 0), while the other two count time; the automaton may go back to the "leaking" location only when x 50.

LRA was extended in [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF][START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF] to deal with such linear hybrid automata. The abstract semantics of discrete transitions is standard. To deal with the continuous evolution of variables in a given location, the "time elapse" operator on polyhedra was introduced: let D be a polyhedron representing the domain of variable derivatives in a given location; let I be the polyhedron representing the invariant attached to the location. Assume the location is entered while the variable values belong to some polyhedron P. Then, the set of variable values which can be reached during the stay in the location is

{x + td | x ∈ P, d ∈ D, t 0} ∩ I
which can be computed as (Pր{V, R}) ∩ I, where (V, R) is a system of generators of D: one adds as rays to P the vertices and rays of D, and intersects the result with the invariant.

In Fig. 4, we represent the projection onto the variables t and ℓ of the successive polyhedra computed when analyzing the hybrid automaton of the gas burner:

• At step 1, the "leaking" control point is reached with the unique point {t = ℓ = 0}, and the time elapse operator gives the segment {0 t = ℓ 10}. Thus, the "not leaking" control point is reached with the polyhedron {0 t = ℓ 10}, and the time elapse operator gives the polyhedron {0 ℓ 10, t ℓ}. • At step 2, the contribution of the return transition from "not leaking" to "leaking" is the polyhedron {0 ℓ 10, t ℓ + 50} (in dark in the bottom-left figure), then the time elapse operator is applied, then the convex hull with the preceding polyhedron is computed, and finally the widening operator provides {0 ℓ t, t 6ℓ -50}. If we propagate we find the same polyhedron for the "not leaking" location, and we stop. Notice that the results are the exact convex hulls of the reachable points. Now let us consider a discrete version of the gas burner, where continuous variables are replaced by counters (Fig. 5): in the L(eaking) location, the 3 variables are incremented as long as x 9. In the N(on leaking) location, only t and x are incremented.

L

x := 0; t := 0; ℓ := 0 Let us apply the classical LRA to this automaton: In L, we get first t = ℓ = 0, then t = ℓ = 1 (with no contribution back from N), so the convex hull is {0 t = ℓ 1}, and the widening provides {0 t = ℓ}. The complete analysis terminates with

τ 1 : x ≤ 9 → N τ 2 : true → true → x := 0 x ≥ 50 → x := 0 x := x + 1 t := t + 1 x := x + 1 t := t + 1 ℓ := ℓ + 1
P L = {0 x ℓ, ℓ t} P N = {0 x, 0 ℓ; x + ℓ t}.
This result is much less precise than in the continuous case, and is not improved by the descending sequence. To obtain better results, we should delay the widening for at least 60 iterations (to get the same invariant as for the hybrid version). Of course, delaying the widening in such a way is expensive; moreover it is rather ad-hoc, and it would not work if the constants of the problem were replaced by some symbolic parameters.

This example shows that the analysis can give much better results on a hybrid automata than on the corresponding discrete counter automata. The obvious reason is the availability of the "time elapse" operator, which plays the role of a specialized exact widening operation. A result of the following sections will be to detect that the effect of the single loops in the counter automaton of Fig. 5 can be computed exactly, so that these loops can be treated as single transitions, exactly as it is done by using the time elapse operator on hybrid automata. In other words, instead of analyzing the automaton of Fig. 5, we will apply the standard analysis to the automaton of Fig. 7, where τ ⊗ 1 , τ ⊗ 2 denote the operations subsuming the effect of the two single loops in the initial automaton. In this standard analysis, the two single loops will be accelerated, but the widening is still applied, e.g., at L, because of the remaining global loop.

L L ′

x := 0; t := 0; ℓ := 0 The rest of the paper is devoted to identifying the loops and sets of loops that can be "accelerated" in that way. We will consider first single loops, i.e., self-looping transitions around a control state.

τ ⊗ 1 N N ′ τ ⊗ 2 true → x := 0 x ≥ 50 → x := 0
6 Single loops 6.1 Some definitions and first remarks

Let (K, k init , T ) be a program. Definition 1 A loop of size p around a control point k ∈ K is a sequence of transitions (k, τ 1 , k 1 ) → (k 1 , τ 2 , k 2 ) → . . . → (k p-1 , τ p , k). A single loop is a loop of size 1, (k, τ, k).
In this section, we consider the acceleration of single loops. We restrict ourselves to transitions with affine guards and affine assignments: τ : A x B → x := C x + D. Such a transition can be expressed as a function from

Q n to Q n : τ : x → if A x B then C x + D else x
Let P 0 be a polyhedron, we want to characterize the effect of any number of applications of τ on P 0 , i.e., to compute τ

* (P 0 ) = { x | ∃i ∈ N, ∃ x 0 ∈ P 0 , x = τ i ( x 0 )}
or, if, for each x 0 , we define the sequence (x ℓ ) ℓ 0 by

x ℓ = C ℓ x 0 + ℓ-1 j=0 C j D: x ∈ τ * (P 0 ) ⇔ ∃ x 0 ∈ P 0 , ∃i ∈ N, such that x = x i and ∀ j ∈ [0, i -1], A x j B.
In general, obtaining a general expression for C ℓ is too expensive, and the quantification over i and j cannot be computed. So, let us look at some cases where the computation is possible; in such cases, the loop will be said to be accelerable:

• [59] considers the same kind of loops, and shows that their termination is decidable. The method uses algebraic characterization of the C matrix, but does not provide any loop invariant.

• In [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF], the class of linear functions λ x.C x + D such that the cardinal of {C ℓ , ℓ ∈ N} is finite is pointed out to be accelerable. But the upper-bound that is given is too large, and as far as we know, the complexity of finding whether a monoid generated by a matrix is finite or not is an open problem (it is known to be decidable [START_REF] Halava | Decidable and undecidable problems in matrix theory[END_REF]). • The case where C 2 = C is interesting, since it covers the loops which increment or decrement variables by constants, and/or set variables to constants. • The simplest case is when C = I (the identity matrix), i.e., when all variables are incremented or decremented by constants. We call such loops translation loops and we first consider this simple case.

Abstract acceleration of a translation function

Let us consider a translation τ : A x B → x := x + D. First we distinguish the case where τ is not applied at all from the other applications: τ * (P 0 ) = P 0 ∪ τ + (P 0 ). To apply τ an arbitrary positive number of times, it is enough that the guard -since it is convex -be satisfied at the first and last applications of the function:

x ∈ τ + (P 0 ) ⇔ ∃i ∈ N * , ∃ x 0 ∈ P 0 , x = x 0 + iD ∧ A x 0 B ∧ A( x 0 + (i -1))D) B.
We are faced with an arithmetic problem: the exact effect of the loop is defined with i ∈ N * , but there is no way to compute simply it by elementary operations on polyhedra. To avoid this, we decide to introduce the notion of dense abstract acceleration, which is defined as follows:

Definition 2 Let τ : A x B → x := x + D be a translation. We call dense abstract acceleration of τ the function τ ⊗ : P 0 → P 0 ⊔ τ ⊕ (P 0 ) with

x ∈ τ ⊕ (P 0 ) ⇔ ∃i ∈ Q + , ∃ x 0 ∈ P 0 , x = x 0 + iD ∧ A x 0 B ∧ A( x -D) B.
τ ⊕ (P 0 ) is a polyhedron which can be easily computed by means of usual operations on polyhedra:

Proposition 1 Let τ : A x B → x := x + D. Then: τ ⊕ (P 0 ) = (P 0 ∩ {A x B}) ր {D} ∩ {A( x -D) B}.
This proposition is illustrated in Figure 8, where g stands for the guard A x B.

Proof The fact that, in Definition 2, ∃x 0 ∈ P 0 ∩ g, ∃i ∈ Q + , such that x = x 0 + iD, exactly expresses that x ∈ (P 0 ∩g) ր {D}, by definition of a ray. The last intersection with {A( x-D) B} results straightforwardly from the guard.

The abstract dense acceleration τ ⊗ (P 0 ) is guaranteed to contain τ * (P 0 ), but generally it is only an overapproximation of the convex hull of τ * (P 0 ), as shown by the following example:

Example 1 Let τ : {x 11} → x := x + 2 with P 0 = {x = 0}.
The exact convex hull of τ * (P 0 ) is {0 x 12}, while the above definition gives τ ⊗ (P 0 ) = P 0 ⊔ {x = 0} ր (1) ∩ {x 13} = {0 x 13}. However, the next example shows that, because of arithmetics, the exact behavior of variables can be complex, so computing the exact convex hull is not realistic.

Example 2 Let P 0 = {0 x = 2y 4} and τ : y 3 → y := y + 2, x := x + 1. Figure 9 shows the effect of the successive applications of τ to points in P 0 . On this figure, we can see that τ * (P 0 ) (in dark) is quite irregular, due to arithmetics. The light part shows the difference between τ ⊗ (P 0 ) and τ * (P 0 ). In the particular case of Example 1, the Omega algorithm ( [START_REF] Pugh | The omega test: a fast and practical integer programming algorithm for dependence analysis[END_REF]), which uses integer linear programming, would give the exact result, and thus its convex hull. In the general case, the linear programming algorithms give better results in the case where the program deals with integer variables. Indeed, the projection algorithm in the Omega test uses the projection of one integer variable on polyhedra intersected with a lattice (here the word lattice is used for Z n ), and thus cannot be used in our general context.

The gas burner example with abstract acceleration

Applying the results of the section 6.2 to the example of Fig. 5 and??, we obtain the following expressions for the acceleration of τ 1 and τ 2 :

τ ⊗ 1 (P) = P ր D L ⊓ {x 10} and τ ⊗ 2 (P) = P ր D N
where D L = (1, 1, 1) and D N = (1, 1, 0) are the translation vectors of the translation loops around control points L and N, respectively.

• Step 1.

P 1 L = {x = t = ℓ = 0} ր D L ⊓ {x 10} = {0 x = t = ℓ 10}. Then, P 1 N = τ ⊗ 2 [x := 0](P 1 L ) = {ℓ + x = t, ℓ 10, 0 ℓ t}. • Step 2.
-Location L: We compute the contribution [x := 0] P 1 N ⊓ {x 50} , then the convex hull with P 1

L , to obtain P ⊔ L = {x = 0, 0 6ℓ t, ℓ 10}. Then, we apply the widening operator:

P 1 L ∇τ ⊗ 1 (P ⊔ L )
, and we obtain P 2 L = {6ℓ t + 5x, 0 x 10, x ℓ}. -Location N: A similar computation without widening provides: P 2 N = {6ℓ + x t + 50, ℓ + x t, 0 l, 0 x}.

•

Step 3 shows the convergence. We have obtained in 3 steps the same invariants as in the hybrid version, without delaying the widening. Let us notice that the expressions of τ ⊗ 1 and τ ⊗ 2 compute the exact effect of the loops because variables are incremented by one at each time.

Abstract acceleration of a translation/reset function

If τ is a translation combined with some reset, that is, τ can be rewritten in the following way:

τ : A x B →        y := y + D y (translated variables) z := D z (reset variables)
, where x = y z

we can obtain a similar definition and algorithm for τ ⊗ (P 0 ). Indeed, a translation/reset behaves like a translation of vector D y 0 if the number i of loop iterations is strictly greater than 1. So we compute the acceleration of P 1 = τ(P 0 ), thanks to the fact all points in τ(P 0 ) satisfy Z = D z .

Definition 3 τ ⊗ : P 0 → P 0 ⊔ τ ⊕ (τ(P 0 )) with:

τ ⊕ : P 1 → x | ∃i ∈ Q + , ∃ x 1 ∈ P 1 , g( x 1 ) ∧ g x - D y 0 , x = x 1 + i D y 0 .
Proposition 2 Let τ : A x B → x := C x + D with C a diagonal matrix with only 1 and 0 on the diagonal. Then:

τ ⊕ (P 1 ) = P 1 ∩ {A x B} ր D y 0 ∩ g X - D y 0 .

The finite monoid class

In this section, we consider a transition τ : A x B → x := C x + D, where the matrix C verifies ∃p, C 2p = C p . We have already seen in section 4 that [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] and [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] obtain acceleration results for this particular class of transitions. Let's show that, in this case, we are able to compute an over-approximation of τ * (P 0 ) by using a reduction to translation/reset functions.

Lemma 1 Let τ : A x B → x := C x + D be a guarded affine transition with ∃p 1, C 2p = C p . Then the computation of τ * (P 0 ) can be reduced, in polynomial time in p and n (the size of C), to the computation of the iterated image of p polyhedra by an affine guarded transition τ ′ whose matrix C ′ verifies C ′2 = C ′ , i.e., is a projection matrix.

Proof Let P ′ = τ * (P 0 ) = P 0 ⊔ P 1 . . . ⊔ P p-1 ⊔ P p ⊔ . . . then we can write:

P ′ = P 0 ⊔ τ p (P 0 ) ⊔ τ 2p (P 0 ) ⊔ . . . ⊔ P 1 ⊔ τ p (P 1 ) ⊔ τ 2p (P 1 ) ⊔ . . . ⊔ . . . ⊔ P p-1 ⊔ τ p (P p-1 ) ⊔ . . . .
Then we remark that x has an image by τ p if and only if the condition:

A x B ∧ A(C x + D) B ∧ . . . ∧ A C p-1 x + C p-2 + C p-3 + . . . + I D) B is verified.
Finally, if we write

C ′ = C p , B ′ =                    B B -AD B -A (C + I D) . . . B -A (C p-1 + . . . + I)D                    , A ′ =                    A AC AC 2 . . . AC p-1                    and D ′ = (C p-1 + C p-1 + . . . I)D, we have τ ′ : A ′ x B ′ → C ′ x + D ′ ,
and finally:

P ′ = 0 i p-1 P p with P p = τ ′ * (P p ).
So we are led to the computation of p polyhedra images by the affine guarded transition τ ′ which verifies C ′2 = C ′ . The computation of the new transition is independent of P 0 and costs 4p matrix multiplications. Let us notice that the size of the guard of τ ′ is p times the one of the guard of τ.

Lemma 2

The case where C 2 = C can be polynomially reduced to the case of a diagonal matrix with only 0s and 1s on the diagonal.

Proof If C 2 = C then C is a projection matrix so we can move to a base adapted to this projection. We compute fixpoints of C (classically, the kernel of C -I), and the points that have a null image (kernel of C). These vectors constitute an (invertible) matrix Q such that Q -1 CQ is diagonal with only 0s and 1s on the diagonal. Then, we are able to compute the modified guard, D and P 0 . Each operation costs O(n 3 ).

Finally, we obtain:

Proposition 3 Let τ : A x B → x := C x + D be an affine guarded transition verifying ∃p, C 2p = C p and P 0 an input polyhedron. Then we compute an overapproximation of τ * (P 0 ) by reducing it to p computations of abstract accelerations of translation/reset.

Proof Immediate from lemmas 1 and 2 and the results of the two previous subsections.

Conclusion of the section

The previous subsections have shown that we can compute overapproximations of a whole class of loops, containing swap loops, translation, translation/reset, and some kind of rotations. Let us point out the fact that our algebraic condition is equivalent to the one of [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] ("Is there a power C p of C which is diagonalizable and which eigenvalues are in the {0, 1} set ?") and also of [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] ("is the multiplication monoid < C >= {I, C, C 2 , . . .}) finite ?"). Deciding one of these questions can be done in O(n 4 ) where n is the size of C. But p can be very large:

Proposition 4 [START_REF] Miller | The maximum order of an element of a finite symmetric group[END_REF] A power p such that C 2p = C p can be very big. More precisely, the maximum of such p verifies ln(p max ) ∼ √ n ln(n).

This result influences the algorithm implementation. In [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF], such a decision algorithm for finding p is implemented, and the author uses the result to compute the desired (precise) acceleration. In [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF][START_REF] Bardin | Vers un model checking avec accélération plate de systèmes hétérogènes[END_REF], the authors propose semi-algorithms that terminate if and only if the associated monoid is finite, but do not decide if it is the case. In our case, we decided to search for a such p up to a constant (generally 3 or 4). This choice comes from the fact that for larger p, the computation becomes both too expensive and too unprecise (because of the p -1 convex hulls performed at the end of the computation).

Multiple loops

In this section, we address the case of multiple single loops around the same control point (Fig. 10), and we focus on translation and translation/reset functions.

Combined Translation loops

We first consider the case of transition loops τ i : g i → x := x + D i . We give some theoretical results concerning this case, and we give an algorithm to compute efficiently a precise over-approximation of the convex hull of reachable states.

x 0 D 1 g 2 g 1 D 2 x 0 g 2 g 1 D 1 D 2
Figure 11: More complex behaviors First remarks: When there are multiple loops around the same control point, the computed polyhedra become more complex. Even in the case of combined translations, the successive applications of the transitions may introduce non convexity and/or complex oscillations. Consider Fig 11, where we take P = {x 0 } and we apply a succession of τ 1 and τ 2 actions, when possible (the guards are the half-spaces that are delimited by the deep lines). The left-hand Figure shows a non convex behavior, the right-hand one shows oscillations. This last example shows that the acceleration results of section 6 cannot be applied in the general case because the graph is not flat (the successive applications of τ * 1 , then τ * 2 , then τ * 1 never reach a fixpoint).

The problem to compute (τ 1 + τ 2 + . . .) * (P 0 ) is known to be hard, as shown by the previous works on acceleration and also the results obtained for Piecewise Constant Derivative (PCD) systems ([3]). Such a system (in dimension 2) is drawn in Figure 12. The space is divided into polyhedral regions, and a vector is associated to each region. The direction of the trajectory of one point in a region is given by the associated vector, and changes as soon as a frontier is crossed. Consequently, as the computation of the successive iterations of the τ i translation functions on the entry polyhedron P 0 can be reduced to reachability in a PCD, our problem is still undecidable in this case.

In this section, we consider the case of two translations. The successive applications of (an over approximation of) τ * 1 , then τ * 2 , then τ * 1 and so on, is not guaranteed to terminate.

A first proposition, partitioning the graph

In [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF], we proposed to compute in one step all points that are reachable while continuously satisfying both g 1 and g 2 :

Definition 4 τ • 1,2 (P 0 ) is composed of all x that can be obtained from P 0 ∩ g 1 ∩ g 2 by "rationally" applying the two translations τ 1 and τ 2 while staying in g 1 ∩ g 2 :

x ∈ τ • 1,2 (P 0 ) iff ∃ x 0 ∈ P 0 ∩ g 1 ∩ g 2 , ∃ x 1 , x 2 . . . , x ℓ ∈ g 1 ∩ g 2 , ∃ x ′ 1 , x ′ 2 . . . , x ′ ℓ ∈ g 1 ∩ g 2 , ∃i 1 , i 2 , . . . , i ℓ , i ′ 1 , i ′ 2 , . . . , i ′ ℓ ∈ Q + , such that x = x ′ ℓ , and x j = τ i j 1 ( x ′ j-1 ), x ′ j = τ i ′ j
Remark 1 Since we compute in the lattice of closed convex polyhedra, we will in fact compute the closure of this preceding set, i.e., the set of all limits of sequences of points staying in g 1 ∩ g 2 and resulting from a sequence of rational applications of τ 1 and τ 2 . This closure will also be noted τ • 1,2 (P 0 ) henceforth. The following proposition gives an algorithm to compute (the closure of) τ • 1,2 (P 0 ): Proposition 6 Let τ i : g i → x := x + D i , (i = 1, 2), then:

• if there exist x ∈ P 0 ∩ g 1 ∩ g 2 , and ε > 0 such that x + εD 1 ∈ g 1 ∩ g 2 , or x + εD 2 ∈ g 1 ∩ g 2 (i.e., there is at least one point of P 0 from which one of the two transitions can be rationally applied while staying in g 1 ∩ g 2 ), then:

τ • 1,2 (P 0 ) = ((P 0 ∩ g 1 ∩ g 2 ) ր {D 1 , D 2 }) ∩ g 1 ∩ g 2 . • otherwise τ • 1,2 (P 0 ) = P 0 ∩ g 1 ∩ g 2 . Proof Let P l = ((τ 1 + τ 2 ) • (P 0 )) et P r = ((P 0 ∩ g 1 ∩ g 2 ) ր {D 1 , D 2 }) ∩ g 1 ∩ g 2 .
• P r ⊆ P l is obvious.

• P l ⊇ P r :

D 1 D 2 x 0 x g 1 g 2
Figure 13: Proof draw Let x ∈ P r . Then there exists k 1 , k 2 ∈ Q + , and

x 0 ∈ P 0 ∩ g 1 ∩ g 2 such that x = x 0 + k 1 D 1 + k 2 D 2 .
The hypothesis of the proposition implies that x 0 (or one point in its neighborhood) satisfies ∃i 0 > 0, x 0 + i 0 D 1 ∈ P 0 ∩ g 1 ∩ g 2 . Then let us define

x 1 = x 0 + i 0 D 1 + i 0 k 1 k 2 D 2 .
By construction x 1 belongs to the segment [ x 0 , x] and thus, since both x and x 0 satisfy g 1 ∩ g 2 , so does x 1 (by convexity). We also have xx 1 < xx 0 . By iterating the process, we obtain a sequence of x i s which converges to x (dark line on figure 13). x being the limit of points of τ • 1,2 (P 0 ), it belongs to the closure of τ • 1,2 (P 0 ).

Remark 2

The first condition on P 0 ∩ g 1 ∩ g 2 comes from the fact that there must be one (rational) application of τ 1 or τ 2 to initialize the successive iterations. This condition is easy to check by taking N 1 a normal vector to g 1 , then the condition is equivalent to N 1 .D 2 > 0 (scalar product).

CFG partitioning Now we can partition the control-flow graph in order to use the previous results. The idea is to separate the cases where both transitions are enabled from those where each transition is enabled alone. This operation on the CFG, illustrated in figure 14, consists in:

• creating new control points q 1 , q 2 , q 12 . All valuations reaching q 1 (respectively q 2 , q 12 ) will satisfy g 1 ∧ ¬g 2 (resp. g 2 ∧ ¬g 1 , g 1 ∧ g 2 ).

• creating the transition for the initialization of these new control points, from q 0 (ε is the identity action). • creating ending transitions from q 1 , q 2 , q 12 to q ′ , with empty transitions (ε on the figure).

• creating single loops around q 1 and q 2 , taking into account the location invariant. For instance, around q 1 , the transition (q 1 , (pre(g 1 ∧ ¬g 2 , a 2 ), a 1 ), q 1 ) is created (where pre(g, a) stands for the precondition of g according to a). For q 12 we add the loop τ • 1,2 .

• creating the new transitions between these new control points. For instance, on the figure 14, the transition µ 1,2 denotes the transition (q 1 , (pre(g 2 ∧ ¬g 1 , a 1 ), ε), q 2 ). Remark 3 The complement ¬g 2 of a polyhedron g 2 is not necessarily a polyhedron, but a union of polyhedra. We can then create a new transition for each element of this union.

q 0 q τ 1 τ 2 q 0 q 12 q 1 q 2 q ′ τ • 12 τ ′ 1 τ ′ 2 ε ε ε µ 1→2 g 1 ∧ g 2 → ε g 1 ∧ ¬g 2 → ε ¬g 1 ∧ g 2 → ε true → ε
After this partitioning, we use the classic LRA strategy, in fact the new partitioned graph has more loops, so new strongly connected sub-components. In particular, q 1 , q 2 and q 12 are new widening points. We can replace however τ 1 and τ 2 by their acceleration, which strongly reduces the number of iterations.

In practice, this partitioning is not realized, because of the induced combinatorial explosion in case of many loops. A first heuristic consists in computing an approximate solution of the system P = P 0 ⊔ τ • 1,2 (P) ⊔ τ ⊗ 1 (P) ⊔ τ ⊗ 2 (P), using the widening operator if necessary. Experimentally, it often happens that

P = P 0 ⊔ τ • 1,2 (P 0 ) ⊔ τ ⊗ 1 (P 0 ) ⊔ τ ⊗ 2 (P 0
) is already a post-fixpoint, in which case the widening is not applied. Of course, it is one strategy among others, we could compute for instance

P = P 0 ⊔ τ • 1,2 (P 0 ) ⊔ τ ⊗ 2 (τ ⊗ 1 (P 0 )) ⊔ τ ⊗
1 (τ ⊗ 2 (P 0 )) or other combinations, as the Fast tool does ( [7]).

Example 3 Let us come back to the example of Fig. 1, which can be considered as the CFG of Fig. 15.a. We can compute τ 15.c) Then we compute the following polyhedra:

• 1,2 ({x = y = 0}) = {(0, 0)} ր {(1, 1), (2, 0)} ∩ {x 100} = {0 y x 100} (see Fig.
• τ ⊗ 1 (τ • 1,2 (P 0 )) = {0 y 100, y x, x 102} • τ ⊗ 2 (τ • 1,2 (P 0 )) = {0 y x y + 100}
The convex hull of these polyhedra is {0 y x 102, y + x 202}, which is stable by any application of τ 1 or τ 2 , so we have reached a post fixpoint. We are then able to propagate the information to control point k 3 , for which we get the polyhedron {0 y 202x, 101 x 102}. So, we obtain in only one iteration the same results that we got with widening and descending sequence in §3.3.

A direct algorithm

A second possibility is to directly compute an over-approximation of (τ 1 + τ 2 ) * . We will see that we can compute directly some over-approximations without dealing with integer arithmetic. Then we propose an algorithm to deal with all cases.

First results:

k 1 k 0 k 2
x ≥ 101?

x ≤ 100? τ 2 :

x := x + 1 y := y + 1

x ≤ 100?

x := x + 2 τ 1 :

x := y := 0

(τ 1 + τ 2 ) * (P 0 ) =                    P 0 if P 0 ∩ g 1 = ∅ and P 0 ∩ g 2 = ∅ P 0 ր {D 1 } if P 0 ∩ g 2 = ∅ and P 0 ր {D 1 }) ∩ g 2 = ∅ P 0 ր {D 2 } if P 0 ∩ g 1 = ∅ and P 0 ր {D 2 }) ∩ g 1 = ∅ P 0 ր {D 1 , D 2 } otherwise P 0 g 1 g 2 D 1 g 2 P 0 D 2 g 1 D 2 (b) (a)
Figure 16: Illustration of Proposition 7

Proof Let P be (τ 1 + τ 2 ) * (P 0 ). If P 0 ∩ g 1 = ∅ and P 0 ∩ g 2 = ∅, then P = P 0 . Let us now suppose that P 0 ∩ g 1 = ∅ and P 0 ∩ g 2 ∅ (Figure 16). Since D 2 is a ray of g 2 , each point of P 0 ∩ g 2 ր D 2 belongs to P. Then, since P is convex, each point of P 0 ր D 2 belongs to P (Figure 16.(a)). Now, there are two possibilities:

• if P 0 ր {D 2 } ∩ g 1 = ∅,
there are no more points. This is the case of Fig. 16.(a).

• if P 0 ր {D 2 } ∩ g 1 ∅ (Fig. 16.(b)), and the ray D 1 should be added, again because of the convexity of P.

Proposition 8 If D 2 is a ray of both polyhedra g 1 and g 2 , then (τ 1 + τ 2 ) * (P 0 ) = τ * 1 (τ * 2 (P 0 )).

Proof Let us show that τ 1 and τ 2 can commute in the following way:

∀X 0 ∈ R n , ∀p i ∈ N, τ p 1 2 τ p 2 1 (τ p 3 2 (X 0 ) = τ p 2 1 (τ p 1 +p 3 2 (X 0 ))
Let us name L the left expression and R the right one. Then:

• If p 1 = 0, or p 2 = 0 ,or p 3 = 0 then L = R.
• Else, suppose p 1 , p 2 , p 3 0 and let X = L. As p 2 0, the left expression implies that τ p 3 2 (X 0 ) = X 0 + p 3 D 2 satisfies g 1 . As D 2 is a ray of g 1 , we get: ∀i ∈ {0, . . . , p 1 }, g 1 (X 0 + p 3 D 2 + iD 2 ), so g 1 (τ p 1 +p 3 2 (X 0 )). The left expression also implies that, for all i ∈ {0 . . . , p 2 -1}, τ p 3 2 + iD 1 satisfy g 1 , so as D 2 is a ray of g 1 ,

∀i ∈ {0, . . . , p 2 -1}, g 1 X 0 + (p 1 + p 3 )D 2 + iD 1 ,
and then all the τ 1 applications in R are valid and X = R.

Thus any point obtained as a combination of τ 1 and τ 2 applications can be also obtained by a combination where all the applications of τ 2 are made before τ 1 ones, which means (τ 1 + τ 2 ) * (P 0 ) ⊆ τ * 1 (τ * 2 (P 0 )). Let us notice that this equality is valid even if P 0 ∩ g 2 = ∅, because in this case τ * 2 (P 0 ) = P 0 .

This expression gives a simple algorithm to compute an over approximation in this case by using the simple ones obtained in the previous section. We have a similar result for τ 1 by permuting g 1 and g 2 and D 1 and D 2 on the previous proposition.

Algorithm 1 Let P 0 be the entry polyhedron. Then:

1. If D 1 is a ray of g 1 and D 2 a ray of g 2 , then (cf. proposition 7):

• If P 0 ∩ g 1 = ∅ and P 0 ∩ g 2 = ∅ then return P 0 . • Else, if P 0 ∩ g 2 = ∅, compute P 1 = P 0 ր {D 1 }, then -if P 1 ∩ g 2 = ∅, return P 1 , -else return P 0 ր {D 1 , D 2 }. • Else if P 0 ∩ g 1 = ∅, compute P 2 =ր {D 2 }, then -if P 2 ∩ g 1 = ∅, return P 2 , -else return P 0 ր {D 1 , D 2 }. • Else return P 0 ր {D 1 , D 2 }. 2. If D 2 is
a ray of both g 1 and g 2 , then: (cf. Figure 17.(a))

• Compute P 2 = (P 0 ∩ g 2 ) ր {D 2 } (applications of τ 2 first). • Compute P 21 = (P 2 ∩ g 1 ) ր {D 1 } ∩ post(g 1 , D 1 ).
• Return P 0 ⊔ P 2 ⊔ P 21 (the dotted polyhedron). 3. If D 1 is a ray of both g 1 and g 2 , then (symmetric case of item 2):

• Compute P 1 = (P 0 ∩ g 1 ) ր {D 1 } (applications of τ 1 first).

• Compute P 12 = (P 1 ∩ g 2 ) ր {D 2 } ∩ post(g 2 , D 2 ).
• Return P 0 ⊔ P 2 ⊔ P 12 . 4. In all other cases (see Figure 17 • If P 2 ∩ g 1 ⊆ P 1 then let P 21 = ∅ else P 21 = (P 2 ∩ g 1 ) ր {D 1 } ∩ post(g 1 , D 1 ) (empty set in Fig. 17.(c)). • Compute P ′ = P 0 ⊔ P 1 ⊔ P 2 ⊔ P 21 ⊔ P 12 . If this polyhedron is stable by τ 1 and τ 2 , then return P ′ (Fig. 17.(b)). Else, iterate like in classic LRA, i.e., take as P 0 the polyhedron P 0 ∇ C P ′ ⊔τ 1 (P ′ )⊔ τ 2 (P ′ ) with with C = {post(g 1 , D 1 ), post(g 2 , D 2 )}), and restart the algorithm. (This example is depicted in Fig 17 .(c)) where P 0 is reduced to one point and g 1 = ¬g 2 , P ′ is the dashed polyhedron, which is not stable, and the result is finally obtained by applying widening).

Remark 4

The expressions for cases 2 and 3 are included in the expression of case 4. If the first test is false, we then use the fourth sub-algorithm to compute the desired polyhedron. rays of the guards g 1 = g 2 = {x 100}. So, we compute:

• P 1 = {0 x y 101}.

• P 2 = {y = 0, 0 x 102}.

• P 12 = {0 x 102, x y, 0 y 100}.

• P 21 = {y = 0, 0 x 101}.

• The convex hull is {0 y x 102, x + y 202}. This set is stable under the applications of τ 1 or τ 2 , we do not need any widening application.

The p loops case We adapt the previous algorithm to the p loop case:

1. For all i ∈ [1, p], we compute

P i = (P 0 ∩ g i ) ր {D i } ∩ post(g i , D i ).
2. For all i, j if P i ∩ g j ⊆ P j let P i, j = ∅ else P i, j = (P i ∩ g j ) ր {D j } ∩ post(g j , D j ) 3. Then, let

P ′ = P 0 ⊔ i P i ⊔ i, j i P i, j .
4. If P ′ is stable by each τ i , return P ′ , else start again with P ′ ∇ C i∈ [1,p] τ i (P ′ ) with C = {post(g 1 , D 1 ), post(g 2 , D 2 ), . . . , post(g p , D p )}.

Combined Translation-Reset loops

In this section, we give some partial results concerning the combination of translation and translation/reset. The Figure 18 subsumes our notations. We decompose our variable vector into two components x = ( y, z). In the first loop, all the variables are translated while in the second only the variables denoted by y are translated, and the variables z are reset to 0 (the case of reset to a constant c is very similar).

Remark 5 Without loss of generality, we can assume that P 0 satisfies z = 0, since it is the case after the first application of τ r .

Simple reset

We first study the case of a translation τ 1 combined with a simple reset τ 2 (i.e., no variables y).

Proposition 9 (Simple reset) Let τ 1 : g 1 → x := x + D 1 and τ 2 : true → z := 0 and assume P

0 ⊆ g 1 ∩ { z = 0}. Then, if we note d 1 = D 1 ↓ { z = 0} the projection of D 1 on z = 0, P 0 ր {D 1 , d 1 } ∩ post(g 1 , D 1 )
is an over approximation of (τ 1 + τ r ) * (P 0 ). Proposition 10 (simple reset with guards) Let τ 1 : g 1 → x := x + D 1 and τ 2 : g r → z := 0 and d 1 = D 1 ↓ { z = 0}. We also assume P 0 ⊆ g 1 ∩ { z = 0}, then, let P ′ = P 0 ր {D 1 } ∩ post(g 1 , D 1 ):

• if P ′ ∩ g r = ∅ then P ′ is an overapproximation of (τ 1 + τ r ) * (P 0 ).

• else P 0 ր {D 1 , d 1 } ∩ post(g 1 , D 1
) is an overapproximation of (τ 1 + τ r ) * (P 0 ).

P 2 P 21 g 1 D 1 D 2 g 2 P 0 (a) g 2 g 1 D 2 D 2 D 1 P 2 P ′ P 1 P 0 (b) g 1 g 2 post(g 1 , D 1 ) post(g 2 , D 2 ) D 1 D 2 P 12 P P 0 (c)

Reset with translation

A first result Now let us consider the case where D r 0 does not belong to the plane (D 1 , d 1 ). The consequence is that some variables (called y) are translated by the second loop out of the plane (D 1 , d 1 ). In the sequel, we first suppose that g r = true, and also that g 1 is of the form z K (parallel to the hyperplane z = 0, see remark 6). Moreover, and without loss of generality, we assume that P 0 ⊆ {z = 0} ∩ g 1 , that D 1 lies in the subspace y = 0 and D r lies in the subspace z = 0 (see Fig. 21).

Then the variables behave as follows:

• (Fig. 21.a) From a point x 0 satisfying g 1 ∧(z = 0), we can apply both τ 1 or τ r . From x 0 , the translation τ 1 can be applied at most k max times, where k max is the least of all quantities ⌊K z i /D 1z i + 1⌋, for all z i reset variables (on the figure, k max = 2). At any time, τ r can be applied, as its guard is always true; in this case, variables z are reset (projection onto the subspace z = 0) and a translation according to the vector D r is performed in the subspace {z = 0}. Thus, after k applications of τ 1 (0 k k max ) followed by one application of τ r , the current point is defined by x = x 0 + kd 1 + D r with d 1 = D 1 ↓ [z = 0] as before. • (Fig. 21.b) From the points reached so far, the same succession of some (at most k max ) applications of τ 1 followed by one application of τ r can occur. • Finally, we get the whole reachable domain shown in Fig. 21.c, which is the polyhedron with vertices x 0 , x 0 + k max D 1 and rays D r , k max d 1 + d r . We obtain the proposition:

(a) (b) 1 3 7 τ 1 τr τ 1 τr 2z > x → 2z x → (x, z) := (0, 0) x := x + 1 z := z + 1 z := 0 z = 10 → z 9 → (x, z) := (0, 0) x := x + 1 z := z + 1 z := 0
• If P 0 ր {D 1 } does not intersect g 1 : (z K), then P 0 ր {D 1 , d 1 , D r } is a convex overapproximation of (τ 1 + τ r ) * (P 0 ). • Else let k max = ⌊K/D 1z + 1⌋, then P 0 ր {D 1 , D r , k max d 1 + D r } ∩ post(g 1 , D 1
) is a convex overapproximation of (τ 1 + τ r ) * (P 0 ).

Remark 6 In contrast with the example of Fig. 20.(b), if the guard g 1 is not of the form z K, the variable behaviour can be non linear, as shown in Fig. 6, one border of the reachable region is then a parabola. A more general algorithm The previous result can be extended to more general cases:

x ≥ 2z → x := x + 1 z := z + 1 y := y + 1 τ 1 τ r true → z := 0 y := y + 1 (x, y, z) := (0, 0 , 0) x0 Z
• If P 0 is not included in { z = 0}, we first compute P ′ 0 = τ r (τ ⊗ 1 (P 0 )), which is included in { z = 0}. • The next proposition will deal with more general conditions for g r .

Proposition 12 [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] Let τ 1 , τ r of the form: τ 1 : ( z K 1 ) → x := x + D 1 and τ r : ( z ⊲⊳ K r ) → y := y + D r ; z := 0 where ⊲⊳ ∈ { , =, }. Assume K 1 > 0 and D 1 • u z > 0 (i.e., D 1 is not a ray of g 1 ). Let k max1 = ⌊K 1 /D 1z + 1⌋, d 1 = D 1 ↓ [z = 0], and k maxr = ⌊K r /D 1z + 1⌋. We also assume then P 0 ⊆ g 1 ∩ { z = 0}. Then let P ′ be the polyhedron computed with the following algorithm:

• if ⊲⊳ is " " then -if K r < 0 then (τ r is never applied) P ′ = P 0 ր {D 1 } ∩ post(g 1 , D 1 ) -if K r > K 1 then P ′ = P 0 ր {D 1 , D r , D r + k max1 d 1 } ∩ post(g 1 , D 1 ) -if K 1 K r > 0 then P ′ = P 0 ր {D 1 , D r , D r + k maxr d 1 } ∩ post(g 1 , D 1 ) • if ⊲⊳ is "=" then -if K 1 K r > 0 and ∃k, K r = kD 1 z then P ′ = P 0 ր {D 1 , D r + kd 1 } ∩ post(g 1 , D 1 )
else (τ r never applies) P ′ = P 0 ր {D 1 } ∩ post(g 1 , D 1 )

• if ⊲⊳ is " " then -if K r > K 1 and K r > 0 then (τ r never applies) P ′ = P 0 ր {D 1 } ∩ post(g 1 , D 1 ) -if K 1 K r 0, then P ′ = P 0 ր {D 1 , D r + k max1 d 1 , D r + k maxr d 1 } ∩ post(g 1 , D 1 )
Dealing with undeterministic transitions Some benchmarks pointed out the need for undeterministic affectations. The semantics of counter automata has been extended with a special operation x ′ =? who basically encodes that every information on x is lost. The expressivity power of the input language is increased, as all affine transitions, that is, transitions of the form Q(x, x ′ ) with Q a polyhedron, can now be encoded, as shows lemma 3.

Lemma 3 A general transition with affine relations can be encoded as the sequence of two extended affine transitions.

Proof Let t = (k, Q, k ′ ) be a general affine transition (Q is a polyhedron of size 2n. Let z be a vector of n fresh variables and k new a new control point. Then, the transition t is equivalent to the combination of t 1 and t 2 , where:

• t 1 = (k, true, a 1 , k new ) with a 1 ( x, z) = ( x, (?) n ); • t 2 = (k new , g 2 , a 2 , k ′ )
where g 2 ( x, z) = true iff ( x, z) ∈ Q (affine guard) and a 2 ( x, z) = ( z, z) (projection). In other words, the affine relation is encoded in the guard of the second transition. As an illustration, on figure 23, the transition on the left is equivalent to the pair of transitions on the right. Detecting and preprocessing accelerable loops. During the first phase of the analysis the transition functions are preprocessed, an internal structure encodes the type of the action (identity, translation, translation reset, idempotent transition, . . . ), of the guard (always true, simple, complex, . . . ), and if the transition is accelerable, and other useful informations that can be precomputed (postconditions, rays to add, . . . ).

k k ′ 3 ≤ 2x ′ + 7x ≤ 19 2y ≤ 42 k k new k ′ z :=? x ′ := z 2y ≤ 42 3 ≤ 2z + 7x ≤ 19
The control structure of the automaton is modified in order to deal with accelerable loops:

• The unique single loop case (a unique circuit around the head of the strongly connected subcomponent) is dealt with as follows: if the loop is accelerable, then the control point is split into two points, related with a meta-transition, as shown by Fig. 24. This splitting for single loops aims at suppressing the widening at control point q. At q split , the computed polyhedron is τ ⊗ (P 0 ). • The multiple single loop case. For multiple single loops, we also decide to split the control point, as shown in Fig. 25. Multiple loops can be dealt with in two ways:

-If we have only partial acceleration results, we introduce a return identity edge, which creates a new loop, so a widening node must be chosen among q and q split . -If complete acceleration results are available, which means that the multiple loops can be accelerated all together, this return arc is not necessary. This case is similar to the single loop one. • The complex loop case. We deal with this case by (possibly) precomputing the meta transitions associated to the circuits that are detected by the Tarjan algorithm. We compute the associated transformation backward, by composing actions and computing preconditions of guards. For instance, let us consider the following circuit: (q, τ 1 , q 1 )(q 1 , τ 2 , q) with q 1 : x 7 → x := x + 1 and q 2 : x 4 → x := x + 3. In this case, we compute the transition q 2 • q 1 : x 4 → x := x + 4, and it is accelerable, thus we add a meta-transition over the control point q. Both initial transitions are kept in order to preserve the semantic of the CFG. The main drawback of this approach is that not every circuit are detected, in particular in the case where two parallel circuits exists on the same control point (Fig. 26). The detection of every circuit is however too expensive.

q Figure 26: "Parallel" circuits

The choice of widening nodes: Since the first phase modifies the graph structure, the computation of widening control points is done afterwards. Bourdoncle's strategy [START_REF] Bourdoncle | Efficient chaotic iterations strategies with widening[END_REF] has been modified as follows: if the head q of a strongly connected subcomponent has been split (with the creation of q split ), then q split is chosen as a widening point, instead of q. The reason is that it is better to widen at a control point where the most precise information has been collected. Experiments show that widening after acceleration is a good heuristic.

Experimental results

In this section we present some experiments driven with our Aspic tool. These results show that the method we have proposed gives interesting results in terms of precision and efficacity.

Other approaches to compute invariants

Avoiding widening Some authors study specific cases where a (least) fixpoint can be precisely computed without widening. In the lattice of intervals, the problem is studied in [START_REF] Su | A class of polynomially solvable range constraints for interval analysis without widenings and narrowings[END_REF], [START_REF] Costan | A policy iteration algorithm for computing fixed points in static analysis of programs[END_REF] and [START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF]. [START_REF] Sankaranarayanan | Constraint-based linear relations analysis[END_REF] proposes a direct method to solve polyhedra fixpoint equations through the use of Farkas lemma and quantifier elimi-nation. In general, the problem is that these works don't clearly identify the cases where these techniques work.

Using SMT solvers A comparaison to methods using SMT solvers ( [55], [START_REF] Tiwari | Generating box invariants[END_REF], [START_REF] Tiwari | Constraint-based approach for analysis of hybrid systems[END_REF]) is in progress.

Toy examples

For the toy examples, we compared our method (column "Aspic" in tables) with the following ones:

• Classic Linear Relation Analysis, without widening upto, without the new path algorithm, with two widenings: the standard widening ( [START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF]) and the one proposed in [6]. The first analysis is implemented in Aspic and the StInG tool ( [56]) can deal with both of them. The results can be found in column Hal79/BHRZ03. On the toy examples, the invariants are the same. • The algorithm [START_REF] Sankaranarayanan | Constraint-based linear relations analysis[END_REF], which is implemented in StInG (column named "STING"). Aspic provides a translator from the Fast language to the input language of StInG. • The classical LRA with or without widening upto, with the new path algorithm. It has been done

with the Aspic tool (column Ch79-v2) • The LRA with "lookahead widening", which is also implemented in Aspic. The results can be found in column called "lookahead". • The Fast tool, that implements the exact acceleration techniques described in Section 4. The Fast version we used does not give the fixpoint, but only some information on the accelerated loops. The benchmarks give only an estimation of the computing time. The description of the automata can be found in Aspic homepage 1 . We present only the results obtained with the different methods on a relevant control point in Fig 27 and28. No computation time is given because all these analyzes are instantaneous, at the exception of the gas burner and the car analysis with the Fast tool (we stopped these two analysis after 15 min because the Presburger automata were too big at this time (more than 8000 states in each case).

On these examples, we can notice that Aspic often manages to infer more precise invariants than the other tools. When the classic LRA (column CH79-v2) gives the same result, it needs the new path heuristic and the widening upto, and needs more steps to converge, as can be shown in Figure 29. In this last

+ x3 + x4 + x7 = p2, x1 + x2 + x4 + x5 + x6 = p1, . . .} GB {0 x ℓ t} idem ch79 idem Aspic T rain1          d = 9 20 b b s + 20                         . . . 11 b 1 b -s 20 . . .                idem BHRZ03 S impleCar 0 s d 0 t idem BHRZ03 idem Aspic Car 0 s d 0 t idem BHRZ03 idem Aspic Apache1 idem Aspic idem Aspic idem Aspic Goubault1b idem Aspic idem Aspic idem Aspic Goubault2b { j -i <= 25, j 175} {. . . i > 150} idem Aspic wcet1 j k, k 10 2k a, 0 a 2k + 5 BJRZ03 + j 10 idem BHRZ03 wcet2 idem Aspic idem Aspic idem Aspic dummy1 {0 t 0 t} idem CH79 idem CH79 dummy4 {3t = 3t 0 + z, z 0} idem Aspic idem Aspic dummy6 {t + 2a 4} a 6 0 t + a -2 0 t 4 t + 2a ax0          t0 = j, 1 t0, 1 i n -1 < t0 n -1 < i          idem BHRZ03 idem BHRZ03 t4x0 t0 = j, 1 t01 i idem BHRZ03 idem BHRZ03
Figure 27: The toy examples with different methods (1)

These automata communicate with each other by means of shared variables. An ad-hoc product is then performed, which takes the different possible schedulings into account. The result is an interpreted automaton that encodes all the possible behaviors. The final goal is to check trace inclusion between two such automata. On figure 30, we show a result of such a product. We remark that these automata have no nested loops, the only loops coming from "elapsing of simulation time".

The main limitation of this method is the size of the generated automata. This is why people use existing verification tools in order to discard unreachable states and transitions. Our tool can compute an over approximation of reachable states, and thus can cut off unreachable parts in the resulting product.

A translation of the generated MicMac automata (product) to the Fast format has been given by J. Cornet [START_REF] Cornet | Formalizing systemc transactionlevel models of systems-on-chip : a component-based approach[END_REF]. The first experiments on toy examples have shown that Aspic permits to make the analysis in a reasonable time and with non trivial results, as we can seen in Fig. 31.

Name/Method

Lookahead Faster ASPIC On each example, we give the number of locations and transitions of the generated automaton, then the number of accelerated loops; then the number of the locations/transitions potentially reachable given by Aspic, and then the analysis time. The results given by the IF tool [START_REF] Bozga | IF-2.0: A validation environment for component-based realtime systems[END_REF][START_REF] Bozga | Real Time Systems 1: Modeling and verification techniques, chapter Modeling and Verification of Real Time Systems Using the IF Toolbox[END_REF] are exact -since IF deals with timed automata -, but the analysis time can be very long (see the last two examples) and the analysis splits the control, so tracing back the results to the source automaton is more difficult.

Hal79a idem Aspic OK          i + 2 j 204 i 104, 0 j 2 j i          Hal79b idem Aspic OK 0 y x 102 x + y <= 202 S P {x2 + x3 + x4 + x7 = p2, x1 + x2 + x4 + x5 + x6 = p1, . . .} GB {0 x ℓ t} > 15min                6ℓ t + 5x 0 x 10 x ℓ 0 ℓ                T rain1 idem BHRZ03 OK idem BHRZ03 S impleCar          0 s d s 4 0 t          > 15min          0 s 4 s d d 4t + s          Car          0 s d s 2 0 t          OK                0 s 2 s d d 2t + s t 3                Apache1 idem Aspic OK c < tk_sz, 0 c Goubault1b idem Aspic OK i + 2 j = 21 j 8, 6 j Goubault2b idem CH79V2 OK(4s) j 175, i < 177, 98 j wcet1 idem CH79V2 OK(4s) 0 2k a 2k + 5 3k < 10i + 10, k 5i wcet2          5 < k1 20 3k1 . . .          OK(4s)                k = 5, j = 10, i = 5 2k1 a 0 k1 a 2k1 + 5                dummy1 idem Aspic OK 0 t 0 t t 0 + 10 dummy4 idem Aspic OK 3t = 3t 0 + z 0 z 56 dummy6 idem CH79V2 OK 4 t + 2a 16 -2 t -a 1 ax0 idem CH79V2 > 3min t0 = j, 1 t0 i n -1 < t0 t4x0 idem CH79V2 > 3min          t0 = j, 1 i, t0 <= n + 1, i <= n + 1, 1 t0         
Programs with lists [START_REF] Bouajjani | Programs with lists are counter automata[END_REF] proposes a translation of programs manipulating lists to counter automata. This translation is made by making abstraction of lists by some "list segments", all the elements of which having the same behaviour. This modeling is often too rough, so some counters are generated in order to take the lists sizes into account. The tool [START_REF] L2ca | [END_REF] implements this algorithm from programs with lists to the Fast format. Aspic thus permits to verify some properties on program with lists. For the time being, the translation induces several intermediate control points, and the Fast tool does not manage to deal with such programs in the absence of strategy. In many cases, Aspic permits to verify the non reachability of the error states in a reasonable time. However, the generated automata does not involve complex numerical properties for now.

Conclusion

When experimenting standard Linear Relation Analysis on various examples, two phenomena become rapidly evident:

1. There is a significant class of programs where the analysis finds the most precise information, i.e., the least abstract fixpoint; 2. On the other hand, it is much more difficult to get precise results about other programs which, however, have an obviously linear behavior: the "discrete derivative" of some variablesi.e., their average variation with respect to loop counters -is constant, or bounded by constants. This paper explains the former phenomenon, and proposes some solutions to the later one.

We first performed an extended review of the existing proposals in order to improve the results of widened iterations. The message, here, is that while being a heuristic technique, the widening should be applied with some principles in mind. Particularly, the fact that one application of a widening operator is more precise than with another operator, does not ensure that the limit of the iterations will be more precise. Another conclusion, that we used afterwards, is that using only two successive terms of the iteration is often a too strong limitation: looking at the program, i.e., at the way one term is computed from the previous one, can pay off in defining widening strategies.

After this survey of the background, we looked at cases where the least abstract fixpoint should be computable. While being strongly influenced by results of exact acceleration, we decided to stay in the framework of abstract interpretation, because, on one hand, we strongly believe that simplifying sets and formulas is the key to acceptable performances, and on the other hand, we want to keep general applicability: if the exact fixpoint cannot be computed, an extrapolated approximation should still be provided.

We first identified the simple translation loops, which explain the first phenomenon, where standard LRA provides precise results. On this kind of loops, our abstract acceleration computes the result without iteration, thus improving the efficiency w.r.t. classical methods. The second phenomenon often appears when the limitations on derivatives are expressed by means of counter limitations, i.e., by combining translations and resets in loops. We have also studied this case, and identified many situations where the abstract effect of the loop can be computed almost exactly. In these situations, our analysis is more precise, and generally more efficient than existing methods.

Figure 1 :

 1 Figure 1: A simple "program"

Example 1 :

 1 Let us consider the "program" of Fig. 1. The corresponding system of abstract equations is P 0 = ⊤ P 1 = [(x, y) := (0, 0)](P 0 ) ⊔ P 2 P 2 = [(x, y) := (x + 2, y)](P 1 ⊓ {x 100}) ⊔ [(x, y) := (x + 1, y + 1)](P 1 ⊓ {x 100}) P 3 = P 1 ⊓ {x 101}

1 s = 2 ?s := s + 1 t

 121 0; d := 0; s := 0 d = 9?d := d + = 3?t := t + 1

Figure 3 :

 3 Figure 3: Hybrid automaton of the gas burner

Figure 4 :

 4 Figure 4: Analysis of the hybrid gas burner

Figure 5 :

 5 Figure 5: Discrete automaton of the gas burner

Figure 6 :

 6 Figure 6: Behaviour of the discrete gas burner

Figure 7 :

 7 Figure 7: The "accelerated" automaton of the gas burner

Figure 9 :

 9 Figure 8: Adding ray algorithm

τ 1 τ 2 Figure 10 :

 210 Figure 10: Multiple single loops

Figure 12 :

 12 Figure 12: A PCD in dimension 2

Figure 14 :

 14 Figure 14: Partitioning the GFC among guards

Figure 15 :

 15 Figure 15: Example with two translations

  .(b) and 17.(c)):• Compute P 1 = (P 0 ∩ g 1 ) ր {D 1 } ∩ post(g 1 , D 1 ). (a segment starting from the point P 0 in Fig.17

  .(c), a light dashed polyhedron in Fig. 17.(b)) • Compute P 2 = (P 0 ∩ g 2 ) ր {D 2 } ∩ post(g 2 , D 2 ) (empty in Fig. 17.(c)). • If P 1 ∩ g 2 ⊆ P 2 then let P 12 = ∅ else compute P 12 = (P 1 ∩ g 2 ) ր {D 2 } ∩ post(g 2 , D 2 ) (P 12 is empty in Fig. 17.(b)).

Example 4

 4 Let us consider again our example 3 (Fig 15). None of the vectors D 2 =

Figure 17 : 0 Figure 18 :Figure 19 : 1 and d 1 = 1 0 .

 170181910 Figure 17: Illustrations for Algorithm 1

1 D 1 zFigure 20 :Figure 21 :

 112021 Figure 20: Two loops with simple reset, and the convex hull of reachable states

  Figure 22: A parabolic behaviour

Figure 23 :

 23 Figure 23: Affine relations encoded with extended affine function

q x ≤ 10 →Figure 24 :

 1024 Figure 24: The unique single loop case

Figure 25 :

 25 Figure 25: The multiple single loops case

Figure 28 :

 28 Figure 28: The toy examples with different methods (2)

Figure 30 :

 30 Figure 30: Two MicMac automata and their product

1 2 . 2 3

 122 Convex polyhedra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Operations on polyhedra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.3 Models of programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.4 The analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Widening in LRA: state of the art 4 3.1 Principles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Standard widening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.3 Descending sequence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.4 Improving the widening operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.4.1 Parma widening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.4.2 Limited widening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.4.3 Widening with landmarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.4.4 Guiding the widening by a care set . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.5 Widening strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.5.1 Delaying the application of the widening operator . . . . . . . . . . . . . . . . . . 8 3.5.2 New control path . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.5.3 Lookahead Widening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

  table, we used proof goals and compare the behaviour of classical LRA, Lookahead widening and LRA with acceleration. We indicate the minimum delay used for proving the goal, and the number of global iterations. This table shows the efficiency of Aspic in terms of iteration number. The macro states (in white) are locations where the process can give back the control to the scheduler.

	Name/Method	Ch79/BHRZ03		STING	CH79 v2
	Hal79a	0 j 2 j i		idem BHRZ03	0 j 2 j i 104
	Hal79b S P	{0 y x} {x2	idem BHRZ03	{0 y x 102}
	Example	Proof Goal	CH79_v2		Lookahead	Aspic
	swap	da db + 1	delay = 4/6it	delay = 4/7it	delay = 1/1it
	subway b s ⇒ s -b 29 GB 6ℓ t + 50	delay = 1/5it delay = 63/65it delay = 63/66it delay = 1/5it delay = 20/23it delay = 1/4it
	wcet1	3k 10i + 10	delay = 11/12it delay = 10/12it delay = 1/4it
	wcet2	20 k1	delay = 37/39it delay = 37/40it delay = 5/8it
		Figure 29: Some examples with proof goals
	9.3 Application to other areas
	Reachability analysis on MicMac automaton In [25], the authors propose a new automata formalism
	to encode SystemC processes. SystemC [50] is a C++ library used to describe and simulate systems on
	chips, handled as asynchronous compositions of components, managed by a simulation scheduler. For each
	component, a "Micmac automaton" is generated, in which two kinds of states are distinguished:

• The micro states (in black) represent locations where the process owns the control (in SystemC, the scheduling is not preemptive); •

Verimag Research Report n o TR-2010-10

( x j ), j = 1..ℓ. Verimag Research Report n o TR-2010-10

http://laure.gonnord.org/pro/aspic/benchmarks.html

This work has been partially supported by the APRON project of the "ACI Sécurité Informatique" of the French Ministry of Research. Laure

Abstract Acceleration in Linear Relation Analysis

Laure Gonnord, Nicolas Halbwachs if K r < 0 then P ′ = P 0 ր {D 1 , D r , D r + k max1 d 1 } ∩ post(g 1 , D 1 )

Then P ′ is a precise overapproximation of (τ 1 + τ r ) * (P 0 ).

Remark 7

If D 1 •u z < 0 with the notations of Proposition 12, g 1 is always true, then the overapproximation becomes P 0 ր {D 1 , d 1 , D r } An algorithm for a combination of translation and translation/reset Algorithm 2 -Else: * If D 1 is a ray of g 1 or the z in g 1 are not of the form z K 1 , then return P 0 ր {D 1 , d 1 , D r }∩ post(g 1 , D 1 ). * Else, apply proposition 12.

, and P 1r = τ r (P 1 ∩ g r ) we reduce the case into the preceding one. We compute the result P 2 , then P ′ = P 0 ⊔ P 1 ⊔ P 2 ⊔ P 1r . If this polyhedron is stable under τ 1 and τ 2 , return P ′ else continue classical LRA iterations with P 0 ∇ C P ′ with C = {post(g 1 , D 1 )}.

Proposition 13 This algorithm computes an overapproximation of (τ 1 + τ r ) * (P 0 ).

Aspic tool implementation

In this section, we briefly describe our prototype tool Aspic (Accelerated Symbolic Polyhedral Invariant Computation), which implements most of the techniques proposed in this paper.

Aspic is implemented over a fixpoint generic analyzer called Analyseur ( [START_REF]ANALYSER[END_REF]), developed by B. Jeannet at Inria. This tool performs a fixpoint analysis, provided an encoding of the control flow graph and an implementation of the abstract lattice of properties. We chose the polyhedral library NewPolka ( [49]).

Aspic takes as input the textual automata input format of the tool Fast ( [7]). A Fast file is composed of two parts:

• A "model", which contains a textual description of a unique counter automaton: numerical variables, control points and transition functions consisting of a source, a destination, a numerical guard (possibly non convex) and an affine action over the numerical variables. • A "strategy", which defines "regions", and computation objectives. In contrast with the tool Fast itself, our tool only needs an initial region; an "error region" is only optional, and no additional information is required. The Aspic input language grammar can be found in Appendix.

Classical Linear Relation Analysis. The Aspic tool makes a forward accessibility analysis, which aims at discovering some polyhedral invariants at each program control point. If an error region is defined (a formula over numerical variables and control points), the goal is transformed into a non accessibility problem by creating new bad states and new transitions; if, after convergence, all the bad states are associated an empty polyhedron, the goal is proved, otherwise the result is inconclusive.

The analysis is performed through the strategy of strongly connected subcomponents given in [START_REF] Bourdoncle | Efficient chaotic iterations strategies with widening[END_REF]. The decomposition is precomputed at the beginning of analysis by a variant of Tarjan algorithm [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF].

Abstract Acceleration in Linear Relation Analysis


Automatic Detection of Borrowings in Lexicostatistic Datasets

A Workflow for Automatic Linguistic Reconstruction JohannMattis List, Steven Moran, Jelena Prokić

In historical linguistics, two models are traditionally used to describe language history: the family tree model [START_REF] Schleicher | Die ersten Spaltungen des indogermanischen Urvolkes[END_REF]) and the wave theory [START_REF] Schmidt | Die Verwantschaftsverhältnisse der indogermanischen Sprachen[END_REF]. Although both models are often treated as if they were opposing theories of language history, the models are in fact complementary; one emphasizes the temporal aspects of language evolution and the other emphasizes its spatial aspects. Although the idea to combine both models within a single framework have been put forward (Schuchard 1900(Schuchard [1870]], Southworth 1964), it was not until recently that phylogenetic networks were proposed as a formal model to capture both the temporal (vertical) and the spatial (horizontal) aspects of language history. A phylogenetic network is hereby understood as a network containing an explicit time dimension and explicit vertical edges. It consists of a reference tree (backbone) and lateral edges indicating the degree of contact between the taxa or also between internal nodes (ancestor languages) of the tree.

In recent times, many new methods that automatize major steps of the comparative method have been proposed, ranging from pairwise and multiple phonetic alignment [START_REF] Kondrak | A new algorithm for the alignment of phonetic sequences[END_REF][START_REF] Prokić | Multiple string alignments in linguistics[END_REF], List 2012a), via automatic cognate detection [START_REF] Turchin | Analyzing genetic connections between languages by matching consonant classes[END_REF][START_REF] Steiner | A pipeline for computational historical linguistics[END_REF][START_REF] List | Beyond Phylogeny: Quantitative diachronic explanations of language diversity[END_REF]), up to automatic phylogenetic reconstruction [START_REF] Gray | Languagetree divergence times support the Anatolian theory of IndoEuropean origin[END_REF][START_REF] Atkinson | How old is the IndoEuropean language family? Illumination or more moths to the flame?[END_REF]). The problems of phylogenetic network reconstruction and automatic borrowing detection, however, have only rarely been addressed [START_REF] Nelsonsathi | Networks uncover hidden lexical borrowing in IndoEuropean language evolution[END_REF].

In this talk, we present a new, general workflow for automatic linguistic reconstruction. In contrast to previous approaches, we explicitly address the problem of automatic borrowing detection by employing a modified version of the method for the automatic reconstruction of phylogenetic networks by [START_REF] Nelsonsathi | Networks uncover hidden lexical borrowing in IndoEuropean language evolution[END_REF]. This method infers borrowings in sets of cognate words proposed for a given set of languages by searching for those cognate words whose distribution is not in concordance with a given reference tree. We modified the original method in such a way that it now is possible to map the lateral connections inferred by the method onto geographical maps. As a result, the areal component of language history, which is largely neglected in all pure treebased applications, can now be explicitly modeled. It enables the researches to detect linguistic areas of an intensive language contact, thus providing a useful tool for quantitative approaches in areal linguistics.

We illustrate our workflow with the Dogon comparative lexical spreadsheet from the Dogon Languages Project [START_REF] Heath | Dogon comparative lexical spreadsheet[END_REF], a freely available dataset that includes 20 Dogon languages and several dialects. Dogon languages are spoken in Mali and have until recently been poorly described. The current Dogon linguistic situation is unclear, as is the internal structure of the Dogon family at its lower branches. The position of Dogon relative to other African languages families is also unclear, due to its unusual typological characters in a sea of West African languages (e.g. Dogon does not have noun classes or the same word order as languages in this area). The Dogon Languages Project has also begun genealogical studies with the comparative data, thus providing an "oldfashioned" analysis with which to compare our statistical approaches.