Peter Schrammel
email: peter.schrammel@inria.fr

Pavle Subotic
email: pavle.subotic@it.uu.se

Logico-Numerical Max-Strategy Iteration ⋆

Keywords: Verification, Static Analysis, Abstract Interpretation, Strategy Iteration

Strategy iteration methods are used for solving fixed point equations. It has been shown that they improve precision in static analysis based on abstract interpretation and template abstract domains, e.g. intervals, octagons or template polyhedra. However, they are limited to numerical programs. In this paper, we propose a method for applying max-strategy iteration to logico-numerical programs, i.e. programs with numerical and Boolean variables, without explicitly enumerating the Boolean state space. The method is optimal in the sense that it computes the least fixed point w.r.t. the abstract domain; in particular, it does not resort to widening. Moreover, we give experimental evidence about the efficiency and precision of the approach.

Introduction

This paper deals with the verification of safety properties about logico-numerical programs, i.e., programs manipulating Boolean and numerical variables. Verification of such properties amounts to checking whether the reachable state space is contained in the invariant specified by the property.

Classical applications are safety-critical controllers as found in modern transport systems. In such systems the properties to be proved depend on the relationships between the numerical variables of the system. The Boolean state space can be large, especially when analyzing programs written in data-flow languages like Lustre [START_REF] Caspi | LUSTRE: a declarative language for real-time programming[END_REF] and Scade 4 where the control structure is encoded in Boolean (or finite-type) variables.

Abstract interpretation. The reachability problem is undecidable for this class of programs, so analysis methods are not complete. Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is a classical method with guaranteed termination for the price of an approximate analysis result. The key idea is to over-approximate sets of states S by elements S ♯ of an abstract domain. A classical abstract domain for numerical invariants in ℘(R n ) is the domain of convex polyhedra P ol(R n ) [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. An approximation S ♯ of the reachable set S is then computed by iteratively solving the fixed point equation S = S 0 ∪ post(S) in the abstract domain. To ensure termination when the abstract domain contains infinitely ascending chains, one applies an extrapolation operator called widening, which induces additional approximations.

Strategy iteration. Strategy (or policy) iteration methods [START_REF] Costan | A policy iteration algorithm for computing fixed points in static analysis of programs[END_REF][START_REF] Gaubert | Static analysis by policy iteration on relational domains[END_REF][START_REF] Adjé | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis[END_REF][START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF][START_REF] Gawlitza | Precise relational invariants through strategy iteration[END_REF][START_REF] Gawlitza | Abstract interpretation meets convex optimization[END_REF] are a way to solve the above fixed point equation without the need for a widening operator. The main idea of these methods is to iteratively approximate the least fixed point of S = F (S) by fixed points of "simpler", more efficiently computable semantic equations S = F (i) (S), induced by so-called strategies, such that a fixed point of F is guaranteed to be found after a finite number of iterations. Depending on whether the least fixed point is approached from above or below, the methods are called min-or max-strategy iteration respectively.

These techniques are applied to template domains, i.e., abstract domains with a priori fixed constraints for which constant bounds are determined during the analysis. Linear templates generate so-called template polyhedra [START_REF] Sankaranarayanan | Scalable analysis of linear systems using mathematical programming[END_REF], which subsume classical domains like intervals [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF], zones [START_REF] Miné | A new numerical abstract domain based on difference-bound matrices[END_REF] and octagons [START_REF] Miné | The octagon abstract domain[END_REF]. However, these methods are restricted to numerical programs.

Handling Boolean variables. The difficulty in dealing with logico-numerical programs is that Boolean and numerical variables tightly interact in their evolution.

The classical method to handle Boolean variables in an abstract-interpretationbased analysis is to explicitly unfold the Boolean control structure by enumerating the Boolean state space and to analyze the numerical variables on the obtained control flow graph using a numerical abstract domain: however, this raises the problem that the analysis becomes intractable already for small to medium-sized programs because the number of control locations grows exponentially with the number of Boolean variables.

Therefore we have to consider an implicit, i.e. symbolic, treatment of Booleans: -A naive approach is to encode Booleans as integers ∈ {0, 1}. The advantage is that max-strategy iteration can be used "as is" by adding template constraints for those Booleans. Though, such an analysis will yield very rough approximations because commonly used abstract domains can only describe convex sets, whereas Boolean state sets are usually highly non-convex. -Logico-numerical abstract domains aim at abstracting state sets of the form ℘(B p × R n ). One way of representing such sets stems from composite model checking [START_REF] Bultan | Symbolic model checking of infinite state systems using Presburger arithmetic[END_REF] which combines Bdds and Presburger formulas. Domains combining Bdds and numerical abstract domains like polyhedra have been proposed for example by Jeannet et al [START_REF] Jeannet | Dynamic partitioning in analyses of numerical properties[END_REF] and Blanchet et al [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]. -Other (not abstract-interpretation-based) approaches rely on SAT-modulotheory solvers, for example the k-induction-based verification tool Kind [START_REF] Hagen | Scaling up the formal verification of lustre programs with smt-based techniques[END_REF].

In this paper we follow the approach of using logico-numerical abstract domains.

Contributions. Our contributions can be summarized as follows:

1. We describe a novel method for computing the set of reachable states of a logico-numerical program based on max-strategy iteration that avoids the enumeration of the Boolean state space. The technique interleaves truncated Kleene iterations in a logico-numerical abstract domain and numerical maxstrategy iterations. The method is optimal, i.e. it computes the least fixed point w.r.t. the abstract semantics. 2. We give the results of an experimental evaluation: We show that our logiconumerical max-strategy iteration gains one order of magnitude in terms of efficiency in comparison to the purely numerical approach while being almost as precise. Moreover, these are the first experimental results of applying maxstrategy iteration to larger programs.

Organisation of the article. §2 gives an introduction to abstract interpretation with template domains and max-strategy iteration. §3 describes the main contribution, the logico-numerical max-strategy iteration algorithm. §4 presents experimental results, and finally §5 concludes.

Preliminaries

Program model. We consider programs modeled as symbolic control flow graphs over a state space Σ:

Definition 1. A symbolic control flow graph (CFG) is a directed graph L, R, ℓ 0 where
-L is a finite set of locations, ℓ 0 ∈ L is the initial location, and

-(ℓ, R, ℓ ′ ) ∈ R define a finite number of arcs from locations ℓ ∈ L to ℓ ′ ∈ L with transition relations R ⊆ Σ 2 .
An execution of a CFG is a possibly infinite sequence

(ℓ 0 , s 0 ) → R (ℓ 1 , s 1 ) → . . . where ∀k ≥ 0 -ℓ k ∈ L, s k ∈ Σ -(ℓ k , s k ) → R (ℓ k+1 , s k+1 ) if R(s k , s k+1 )
In the case of affine programs, Σ = R n and the relations R(x, x ′ ) are conjunctions of linear inequalities. Fig. 1 A program property we want to prove is for instance the invariant 0 ≤ x ≤ 100.

Abstract interpretation with template polyhedra

Template polyhedra [START_REF] Sankaranarayanan | Scalable analysis of linear systems using mathematical programming[END_REF] are polyhedra the shape of which is fixed by a so-called template. The domain operations can be performed efficiently with the help of linear programming (LP) solvers. We will use the following notations: R = R ∪ {-∞, ∞}; the operators min, sup, ≤, etc are point-wisely lifted to vectors.

Template polyhedra abstract domain. A template polyhedron is generated by a template constraint matrix, or short template, T ∈ R m×n of which each row contains at least one non-zero entry.

For example, 1 -1 is a template constraint matrix of intervals for a system with a single variable x. It represents the constraints

x ≤ d 1 ∧ -x ≤ d 2 , i.e. x ∈ [-d 2 , d 1 ].
The set of template polyhedra P T generated by T is

{X d | d ∈ R m } with X d = {x | x ∈ R n , Tx ≤ d}.
An abstract value is represented by the vector of bounds d. The analysis tries to find the smallest values of d representing a fixed point of the semantic equations. ⊤ and ⊥ are naturally represented by the bound vectors ∞ and -∞ respectively. We state the definitions of the domain operations5 :

-Concretization:

γ x T (d) = {x | x ∈ R n , Tx ≤ d}, d ∈ R m -Abstraction: α x T (X) = min{d ∈ R m | γ x T (d) ⊇ X}, X ⊆ R n -Join: d ⊔ x T d ′ = max(d 1 , d ′ 1 ), . . . , max(d m , d ′ m ) -Image:
The templates may vary from location to location: let us denote T ℓ the template in location ℓ and d ℓ the corresponding vector of bounds. Then the post-image by a transition relation R of transition (ℓ, R, ℓ ′ ) in a CFG is defined as follows:

R ♯ (d ℓ ) = sup{T ℓ ′ x ′ | T ℓ x ≤ d ℓ ∧ R(x, x ′ )}
i.e., given the bounds d ℓ corresponding to the template T ℓ it returns the bounds corresponding to T ℓ ′ .

Reachability analysis. Let R j ℓ,ℓ ′ denote a transition relation in the set of transitions from ℓ to ℓ ′ . We will view d alternatively as the concatenated vector of the bound vectors of all locations and the map L → R m which assigns a vector of bounds d ℓ to each location ℓ:

d(ℓ) = d ℓ . d 0 = λℓ. ∞ for ℓ = ℓ 0 -∞ for ℓ = ℓ 0 denotes
the initial values of the bounds. The set of abstract reachable states represented by the bounds d is computed by:

lfp λd. d 0 ⊔ x λℓ ′ . R j ℓ,ℓ ′ ∈R R j ℓ,ℓ ′ ♯ (d ℓ )

Max-strategy iteration

Max-strategy iteration [START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF][START_REF] Gawlitza | Precise relational invariants through strategy iteration[END_REF][START_REF] Gawlitza | Precise interval analysis vs. parity games[END_REF][START_REF] Gawlitza | Computing relaxed abstract semantics w.r.t. quadratic zones precisely[END_REF][START_REF] Gawlitza | Solving systems of rational equations through strategy iteration[END_REF] is a method for computing the least solution of a system of equations M of the form δ = F (δ), where δ are the template bounds, and F i , 0 ≤ i ≤ n is a finite maximum of monotonic and concave operators R n → R; in our case they are affine functions. The max-strategy improvement algorithm for affine programs is guaranteed to compute the least fixed point of F , and it has to perform at most exponentially many improvement steps, each of which takes polynomial time.

Semantic equations. The equation system M is constructed from the abstract semantics of the program's transitions:

for each ℓ ′ ∈ L : δ ℓ ′ = max {d 0 ℓ ′ } ∪ { R ♯ (δ ℓ ) | (ℓ, R, ℓ ′ ) ∈ R}
with d 0 and R ♯ (d ℓ ) as defined above in §2.1.

Note that we use δ for denoting the vector of bound variables appearing in syntactic expressions, and d for the vector carrying the actual bounds. δ ℓ,i is the bound variable corresponding to the i th line of the template in location ℓ.

Example 2 (Semantic equations).

Using the template constraints

1 -1 x ≤ d ℓ,1 d ℓ,2
in locations ℓ, the equation system for location ℓ 1 of the example in Fig. 1 consists of one equation for each template bound variable of which the arguments of the max operator are the initial value -∞ and one expression R ♯ for each of the three incoming arcs:

ℓ0 ℓ1 ℓ2 x ′ = 5 x ≤ 9 ∧ (x ′ = x+1) x ≥ 10 ∧ (x ′ = x) x ≤ 0 ∧ (x ′ = x) x ≥ 1 ∧ (x ′ = x-1)
Fig. 1: CFG of an affine program

δ 1,1 = max        -∞, sup{ x ′ | x ≤ δ 0,1 ∧ -x ≤ δ 0,2 ∧ x ′ = 5 }, sup{ x ′ | x ≤ δ 1,1 ∧ -x ≤ δ 1,2 ∧ x ≤ 9 ∧ x ′ = x+1 }, sup{ x ′ | x ≤ δ 2,1 ∧ -x ≤ δ 2,2 ∧ x ≤ 0 ∧ x ′ = x }        δ 1,2 = max        -∞, sup{ -x ′ | x ≤ δ 0,1 ∧ -x ≤ δ 0,2 ∧ x ′ = 5 }, sup{ -x ′ | x ≤ δ 1,1 ∧ -x ≤ δ 1,2 ∧ x ≤ 9 ∧ x ′ = x+1 }, sup{ -x ′ | x ≤ δ 2,1 ∧ -x ≤ δ 2,2 ∧ x ≤ 0 ∧ x ′ = x }        Strategies. A strategy µ induces a "subsystem" δ = F (δ) of M in
the sense that exactly one argument F i of the max operator on the right-hand side of each equation δ i = max(. . . , F i (δ), . . .) is chosen. Intuitively, this means that a strategy selects exactly one "incoming transition" for each template bound variable in each location ℓ ′ .

Example 3 (Strategy)

. A strategy in the example in Fig. 1 corresponds for instance the following system of equations:

δ 0,1 = ∞ δ 0,2 = ∞ δ 1,1 = sup{ x ′ | x ≤ δ 1,1 ∧ -x ≤ δ 1,2 ∧ x ≤ 9 ∧ x ′ = x+1 } δ 1,2 = sup{ -x ′ | x ≤ δ 0,1 ∧ -x ≤ δ 0,2 ∧ x ′ = 5 } δ 2,1 = -∞ δ 2,2 = -∞
We see that for δ 1,1 we have chosen the third and for δ 1,2 the second argument of the max operators in the equations of Example 2.

One has to compute the least solution lfp M of the system M, where M is defined as

M (d) = max µ in M µ (d) and with µ (d) = δ = F (δ) (d) = F (d).
Max-strategy improvement. lfp M is computed with the help of the maxstrategy improvement algorithm (see Fig. 2) which iteratively improves strategies µ until the least fixed point lfp µ of a strategy equals lfp M .

initial strategy:

µ := {δ ℓ 0 = ∞, δ ℓ = -∞ for all ℓ = ℓ0} initial bounds: d := λℓ.δ ℓ → ∞ for ℓ = ℓ0 -∞ for ℓ = ℓ0 while not d is a solution of M do µ := max improve M (µ, d) d := lfp µ done return d

Fig. 2: Max-strategy iteration algorithm

The least fixed point lfp µ of a strategy µ can be computed by solving the LP problem with the constraint system

for each δ ℓ ′ = R ♯ (δ ℓ ) in µ : d ℓ ′ ≤ T ℓ ′ x ′ ∧ T ℓ x ≤ d ℓ ∧ R(x, x ′ )
(where x and x ′ are auxiliary variables) and the objective function max i d i , i.e. the sum of all bounds d.

µ ′ is called an improvement of µ w.r.t. d, i.e. µ ′ = max improve M (µ, d) iff 1. µ ′ is "at least as good" as µ: µ ′ (d) ≥ µ (d), and 2. µ ′ is "strictly better for the changed equations": if (δ i = F i (δ)) in µ and (δ i ≥ F ′ i (δ)) in µ ′ and F i = F ′ i , then F ′ (d) > F (d).
Example 4 (Max-strategy iteration). We illustrate some steps of the analysis of the example in Fig. 1. Assume the current strategy is:

µ 1 =                δ 0,1 = ∞ δ 0,2 = ∞ δ 1,1 = sup{ x ′ | x ≤ δ 0,1 ∧ -x ≤ δ 0,2 ∧ x ′ = 5 } δ 1,2 = sup{ -x ′ | x ≤ δ 0,1 ∧ -x ≤ δ 0,2 ∧ x ′ = 5 } δ 2,1 = -∞ δ 2,2 = -∞               
and the current template bounds are:

d 1 =    δ 0,1 → ∞ δ 0,2 → ∞ δ 1,1 → 5 δ 1,2 → -5 δ 2,1 → -∞ δ 2,2 → -∞   
The strategy can only be improved w.r.t. δ 1,1 :

µ 2 =                δ 0,1 = ∞ δ 0,2 = ∞ δ 1,1 = sup{ x ′ | x ≤ δ 1,1 ∧ -x ≤ δ 1,2 ∧ x ≤ 9 ∧ x ′ = x+1 } δ 1,2 = sup{ -x ′ | x ≤ δ 0,1 ∧ -x ≤ δ 0,2 ∧ x ′ = 5 } δ 2,1 = -∞ δ 2,2 = -∞               
We compute the new fixed point w.r.t. µ 2 :

d 2 = lfp µ 2 =    δ 0,1 → ∞ δ 0,2 → ∞ δ 1,1 → 10 δ 1,2 → -5 δ 2,1 → -∞ δ 2,2 → -∞   
In the next step we can improve the strategy w.r.t. δ 2,1 and δ 2,2 , a.s.o.

An improving strategy is selected by testing for each equation whether an argument of its max-operator leads to a greater bound. Since the arguments of the max-operator are required to be monotonic, the bounds are always monotonically increasing and, thus, arguments that have already been selected in previous strategies need not be considered again.

Logico-Numerical Max-Strategy Iteration

We will present an algorithm which enables the use of max-strategy iteration in a logico-numerical context, i.e. programs with a state space B p × R n .

Abstract Domain

We consider the logico-numerical abstract domain A = ℘(B p ) × R m which combines Boolean formulas with template polyhedra. An abstract value (B, d) consists of the cartesian product of valuations of the Boolean variables B (represented as Boolean formulas using Bdds for example) and the template bounds d. We define the domain operations:

-Abstraction: α T (S) = {b | ∃x : (b, x) ∈ S} min{d | (b, γ x T (d)) ∈ S} -Concretization: γ T (S ♯ ) = B ∧ γ x T (d) -Join: B d ⊔ T B ′ d ′ = B ∨ B ′ d ⊔ x T d ′ -Image: R ℓ,ℓ ′ ♯ B d = {b ′ | T ℓ x ≤ d ∧ b ∈ B ∧ R(b, b ′ , x, x ′ )} sup {T ℓ ′ x ′ | T ℓ x ≤ d ∧ b ∈ B ∧ R(b, b ′ , x, x ′ )} ⊤ and ⊥ are defined as tt ∞ and ff -∞ respectively.
Since we are analyzing a CFG with locations L, we have the overall abstract domain Σ ♯ = L → A. An abstract value S ♯ = λℓ.(B ℓ , d ℓ ) ∈ Σ ♯ assigns to each location a value of the above logico-numerical domain. Note that the dimension m of d ℓ may depend on ℓ if the templates differ from location to location.

Algorithm

Our analysis is based on alternating (1) a truncated Kleene iteration over the logico-numerical abstract domain and (2) numerical max-strategy iteration, see Fig. The truncated Kleene iteration (propagation) explores the system until a certain criterion is satisfied; we say that the system preliminarily stable. We use the following criterion: we stop Kleene iteration if for all locations the set of reachable Boolean states does not change whatever transition we take. The underlying idea is to discover a subsystem, in which Boolean variables are stable during a presumably larger number of iterations. In such a subsystem numerical variables evolve, while Boolean transitions switch only within the system, i.e. they do not "discover" new Boolean states, until numerical conditions are satisfied that make Boolean variables leave the subsystem.

11 µ ′ = max improve M (µ, d) 12 while µ ′ = µ do µ := µ ′ d := lfp µ µ ′ = max improve M (µ, d) done            phase (
We use max-strategy iteration (phase (2)) to compute the fixed point for the numerical variables for such a subsystem. Then Kleene iteration (phase (1)) continues exploring the next preliminary stable subsystem. The algorithm terminates in a finite number of steps as soon as the Kleene iteration of phase (1) has reached a fixed point.

Formal description. See Fig. 3. Since we only manipulate abstract quantities, we will omit the superscript ♯ in the sequel in order to improve readability.

For phase [START_REF] Caspi | LUSTRE: a declarative language for real-time programming[END_REF] we use the definitions:

-Initial abstract value: S 0 = λℓ. For phase [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] we define the following: -The max-strategy improvement operator max improve M is defined as described in §2. -The operator generate dynamically derives the system of equations for the current preliminary stable subsystem: this means that we restrict the system to those transitions which stay within the subsystem defined by the current Boolean states λℓ.B ℓ . For this purpose we conjoin the term b ∈ B ℓ ∧ b ′ ∈ B ℓ ′ to the transition relation in the definition below. Strategies may only contain convex constraints: thus, we transform the relation into disjunctive normal form and generate one strategy per disjunct:

⊤ for ℓ = ℓ 0 ⊥ for ℓ = ℓ 0 -Post-condition: post(S) = λℓ ′ .S(ℓ ′ ) ⊔ ℓ R ℓ,ℓ ′ (S(ℓ)) ℓ0 ℓ1 ℓ2 b ′ 1 ∧ b ′ 2 ∧ x ′ = 0 (b ′ 1 = b1) ∧ (b ′ 2 = b2) ∧ x ≤ 19 ∧ x ′ = x+1 if b1 x-1 if ¬b1 (b ′ 1 = b1) ∧ (b ′ 2 = b2) ∧ x ≥ 20 ∧ (x ′ = x) (b ′ 1 = (x ≤ 100)) ∧ (b ′ 2 = b2) ∧ x ≥ 100 ∧ (x ′ = x-100)    (b ′ 1 = b1) ∧ (b ′ 2 = ¬b2) ∧ x ≤ 99∧ x ′ = x+1 if b2 x if ¬b2
generate(S) = ℓ ′ ,ℓ decomp convex(∃b, b ′ : R ℓ,ℓ ′ (b, x, b ′ , x ′ ) ∧ b ∈ B ℓ ∧ b ′ ∈ B ℓ ′ )
where

decomp convex(R ℓ,ℓ ′ ) = j δ ℓ ′ = R j ℓ,ℓ ′ (δ ℓ ) with R ℓ,ℓ ′ = j R j ℓ,ℓ ′ and R j ℓ,ℓ ′ convex.
Remark 1. Since the bounds d are monotonically increasing, we use the constant strategy δ = d (where d are the previously obtained bounds) as initial strategy for phase (2) (see line 10 in Fig. 3). This prevents the numerical max-strategy improvement from restarting with δ = -∞ each time.

We illustrate this algorithm by applying it to the CFG in Fig. 4:

Example 5. We use the template constraint matrix 1 -1 which corresponds to an interval analysis. In order to make the presentation more concise, we will

write states (ℓ → B d ) ∈ Σ as ℓ → ϕ(b 1 , b 2 ) [ -δ ℓ,2 , δ ℓ,1 ]
where ϕ is a Boolean formula.

The initial state in ℓ

0 is tt [-∞, ∞]
. We start exploring the system by taking transition (ℓ 0 , R, ℓ 1 ):

ℓ 1 → b 1 ∧ b 2 [0, 0] . We continue propagating through (ℓ 1 , R, ℓ 1 ): ℓ 1 → b 1 ∧ b 2 [0, 1]
. Now, we have reached preliminary stability because none of the transitions makes us discover new Boolean states in the next iteration ((ℓ 0 , R, ℓ 1 ) and (ℓ 1 , R, ℓ 1 ) yield nothing new w.r.t. Boolean states and the other transitions are infeasible, i.e., they give ⊥). Hence, we go ahead to phase (2) and extract the numerical equation system for each (ℓ, R, ℓ ′ ). E.g. for (ℓ 1 , R, ℓ 1 ), we compute:

∃b, b ′ : R ∧ b 1 ∧ b 2 ∧ b ′ 1 ∧ b ′ 2 = (x ′ = x+1 ∧ x ≤ 19
) which gives us the partial equations:

δ 1,1 = sup{ x ′ | x ≤ δ 1,1 ∧ -x ≤ δ 1,2 ∧ x ′ = x+1 ∧ x ≤ 19 } δ 1,2 = sup{ -x ′ | x ≤ δ 1,1 ∧ -x ≤ δ 1,2 ∧ x ′ = x+1 ∧ x ≤ 19 }
which have to be completed by the other incoming arcs of ℓ 1 . We start the max-strategy iteration with the strategy corresponding to the values obtained in phase (1):

µ = {δ 0 = ∞, δ 1,1 = 1, δ 1,2 = 0, δ 2 = -∞}
We observe that we can improve this strategy w.r.t. δ 1,1 :

µ ′ =    δ 1 = ∞ δ 1,1 = sup{x ′ | x ≤ δ 1,1 ∧ -x ≤ δ 1,2 ∧ x ′ = x+1 ∧ x ≤ 19}, δ 1,2 = 0 δ 2 = -∞   
The max-strategy iteration terminates with:

ℓ 1 → b 1 ∧ b 2 [0, 20] .
We continue propagating (phase (1)): By (ℓ 1 , R, ℓ 2 ) we get ℓ 2 → b 1 ∧ b 2 [START_REF] Gawlitza | Solving systems of rational equations through strategy iteration[END_REF][START_REF] Gawlitza | Solving systems of rational equations through strategy iteration[END_REF] ; then (ℓ 2 , R, ℓ 2 ) results in b 1 ∧ ¬b 2 [START_REF] Jeannet | BDDAPRON: A logico-numerical abstract domain library[END_REF][START_REF] Jeannet | BDDAPRON: A logico-numerical abstract domain library[END_REF] ; by joining these values we get ℓ 2 → b 1 [START_REF] Gawlitza | Solving systems of rational equations through strategy iteration[END_REF][START_REF] Jeannet | BDDAPRON: A logico-numerical abstract domain library[END_REF] . Taking (ℓ 2 , R, ℓ 2 ) a second time does not change the Boolean state: [START_REF] Gawlitza | Solving systems of rational equations through strategy iteration[END_REF][START_REF] Sotin | Policy iteration within logiconumerical abstract domains[END_REF] . Taking any other transition does not discover new Boolean states either, thus, we move on to phase (2) and compute the numerical equation system w.r.t. the current Boolean state: For example for (ℓ 2 , R, ℓ 2 ), we compute

ℓ 2 → b 1
(∃b, b ′ : R ∧ b 1 ∧ b ′ 1 ) = (x ′ = x+1 ∨ x ′ = x) ∧ x ≤ 99 which results in the partial equations δ 2,1 = max sup{ x ′ | x ≤ δ 2,1 ∧ -x ≤ δ 2,2 ∧ x ′ = x+1 ∧ x ≤ 99 }, sup{ x ′ | x ≤ δ 2,1 ∧ -x ≤ δ 2,2 ∧ x ′ = x ∧ x ≤ 99 } δ 2,2 = max sup{ -x ′ | x ≤ δ 2,1 ∧ -x ≤ δ 2,2 ∧ x ′ = x+1 ∧ x ≤ 99 }, sup{ -x ′ | x ≤ δ 2,1 ∧ -x ≤ δ 2,2 ∧ x ′ = x ∧ x ≤ 99 }
which have to be completed by the other incoming arcs of ℓ 2 . The only possible improvement w.r.t to the current state is w.r.t. δ 2,1 ; phase (2) results in ℓ 2 → b 1 [START_REF] Gawlitza | Solving systems of rational equations through strategy iteration[END_REF]100] .

We continue with phase (1), which filters the above value through (ℓ 2 , R, ℓ 1 )

augmenting the abstract value in

ℓ 1 to b 1 [0, 20]
. Then, none of the transitions makes the reachable state sets increase (neither Boolean nor numerical), hence we have reached the global fixed point:

ℓ 0 → ⊤, ℓ 1 → b 1 [0, 20] , ℓ 2 → b 1 [20, 100]
Note that a logico-numerical analysis in the same domain with widening and descending iterations yields no information about this example: S = λℓ.⊤.

Properties

Theorem 1 (Termination). The logico-numerical max-strategy algorithm terminates after a finite number of iterations.

Proof. Termination follows from these observations: (a) Phase ( 1) only propagates as long as new Boolean states are discovered; the number of Boolean states is finite. (b) Max-strategy iteration is called at most once for each subset of Boolean states. The number of subsets of Boolean states is finite. (c) There is a unique system of numerical equations (built by generate) for each subset of Boolean states. (d) Max-strategy iteration terminates after a finite number of improvement steps, because there is a finite number of strategies and each strategy is visited at most once [START_REF] Gawlitza | Precise relational invariants through strategy iteration[END_REF]. (e) Max-strategy iteration returns the unique least fixed point w.r.t. the given system of equations [START_REF] Gawlitza | Precise relational invariants through strategy iteration[END_REF]. Thus, as soon as all reachable Boolean states have been discovered and the associated numerical fixed point has been computed, the overall fixed point has been reached and the algorithm terminates.

Theorem 2 (Soundness). The logico-numerical max-strategy algorithm computes a fixed point of λS.S 0 ⊔ R ♯ (S).

Proof. Let us denote

• F = λS.S 0 ⊔ R ♯ (S).
• λS.(lfp B F )(S) the truncated Kleene iteration phase [START_REF] Caspi | LUSTRE: a declarative language for real-time programming[END_REF] (lines 4 to 7 in Fig. 3), i.e. λS. while B = B ′ do S := S ′ ; S ′ = F (S) end; return S ′ .

• λ(B, d).(B, (lfp X F X )(d)) the max-strategy iteration in phase (2) (lines 9 to 16 in Fig. 3), i.e. λS. M = generate(S); µ := (δ = d); µ ′ = max improve M (µ, d); while µ ′ = µ do µ := µ ′ ; d := lfp µ ; µ ′ = max improve M (µ, d) done; return S . Then, we can write the whole algorithm as lfp((id B , lfp

X F X ) • (lfp B F ) • F ).
Since lfp B F and (id B , lfp X F X ) are both extensive, we can under-approximate them by id = λS.S. Hence, we conclude from

lfp F ⊑ lfp( id id⊑(id B ,lfp X F X ) • id id⊑(lfp B F ) • F )
that our algorithm computes an over-approximation of the least fixed point, i.e. it is sound.

Theorem 3 (Optimality). The logico-numerical max-strategy algorithm computes the least fixed point of λS.S 0 ⊔ R ♯ (S).

Proof. Additionally to Thm. 2, we have to show that lfp((id B , lfp

X F X ) • (lfp B F ) • F ) ⊑ lfp F . (a) Phase (1) computes a certain number of iterations F k (⊥) = (lfp B F ) • F (⊥)
taking into account the whole transition system. We trivially have

F k (⊥) ⊑ lfp F (⊥). (b) Phase (2) (id B , lfp X F X )
iterates over the transitions of a subsystem. It is known [START_REF] Gawlitza | Precise relational invariants through strategy iteration[END_REF] that it computes the least fixed point w.r.t. this subsystem. Hence, the result of phase (2) cannot go beyond the fixed point of the whole system:

(id B , lfp X F X ) • F k (⊥) ⊑ lfp F . (c)
We can repeat arguments (a) and (b) for the outer loop:

. . .

• (id B , lfp X F X ) • F k2 • (id B , lfp X F X ) • F k1 (⊥) ⊑ lfp F
where k n is the number of iterations of the n th phase (1). Thus, we have ((id B , lfp X F X ) • F kn ) n (⊥) ⊑ lfp F for n ≥ 0. Hence, we conclude from lfp((id B , lfp X F X ) • (lfp B F ) • F ) ⊑ lfp F and Thm. 2 that our algorithm computes the least fixed point, i.e. it is optimal.

Application to data-flow programs

For our experiments in §4, we used Lustre programs, i.e. synchronous data-flow programs. For this reason we will briefly explain how to apply our algorithm to such programs.

Lustre programs can be reduced to a symbolic transition system

I(s) A(s, i) → s ′ = f (s, i)
where s = b x and i = β ξ are the vectors of (Boolean and numerical) state and input variables, I(s) is the initial condition, A(s, i) is an assertion constraining input variables depending on state variables, and f is the vector of transition functions. State space partitioning is used to obtain a CFG in which each equivalence class of the partition corresponds to a location.

The transition relations are constructed by

R ℓ,ℓ ′ = ∃β : x ′ = f x (b, x, β, ξ) b ′ = f b (b, x, β, ξ) ∧ ψ ℓ (x, b) ∧ ψ ℓ ′ (x ′ , b ′ ) ∧ A(b, x, β, ξ)
where

f x i = • • • a ij (x, ξ) if φ ij (b, x, β, ξ) . . .
, and ψ ℓ are the definitions of the partitions (locations). Boolean input variables are quantified existentially. Numerical inputs appear as auxiliary variables (i.e., variables without associated bounds) in the max-strategy iteration, hence, they are treated without modification of the algorithms.

Discussion

An important observation is that, since the overall abstract domain is of the form

L → ℘(B p ) × R
m , the choice of the CFG has two effects on the performance: first, it determines the set of representable abstract properties, and second, it influences the approximations made in the generation of the numerical equation system for the max-strategy iteration phase (2), because there is only one template polyhedron per location.

Generalization. The structure of the algorithm we presented is quite general.

In particular, it does not depend on the method used to compute the numerical least fixed point in phase [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. We conjecture that the algorithm makes every method, that is able to compute the least fixed point of a numerical system by ascending iterations, compute the least fixed point of a logico-numerical system. For example, we suppose that our algorithm can be used without any modification with the variant of max-strategy iteration for quadratic programs and quadratic templates proposed in [START_REF] Gawlitza | Computing relaxed abstract semantics w.r.t. quadratic zones precisely[END_REF].

If a method computes the fixed point by descending iterations, as for example min-strategy iteration [START_REF] Costan | A policy iteration algorithm for computing fixed points in static analysis of programs[END_REF][START_REF] Gaubert | Static analysis by policy iteration on relational domains[END_REF], our algorithm can still be used, but requires a small adaptation because the abstract value computed in phase [START_REF] Caspi | LUSTRE: a declarative language for real-time programming[END_REF], which is an underapproximation of the least fixed point, cannot be used to initialize phase (2), which requires an over-approximation: hence, line 10 in Fig. 3 must be replaced by guessing appropriate initial bounds and an initial strategy for phase [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. This makes the algorithm less elegant and the analysis, probably, less efficient.

Logico-numerical max-strategy iteration using a power domain. The algorithm is also rather generic w.r.t. the kind of logico-numerical abstract domain we use. For example, we could consider the logico-numerical power domain B p → ℘(R n ) where ℘(R n ) is abstracted by any domain that is supported by strategy iteration. Then the overall domain for our method is L → B p → R m . This domain implicitly dynamically partitions each location into sub-locations corresponding to Boolean valuations sharing a common numerical abstract value 6 .

The construction of the equation system (generate in our algorithm, Fig. 3) must take into account these partitions. This domain is more precise than the product domain described in §3, however, the drawback is that the number of partitions might explode if only few Boolean valuations share a common numerical abstract value.

Comparison with logico-numerical min-strategy iteration. The power domain B p → R m is also used by Sotin et al [START_REF] Sotin | Policy iteration within logiconumerical abstract domains[END_REF] who propose an approach to analyzing logico-numerical programs using min-strategies. In accordance with the form of the abstract domain, they consider logico-numerical strategies B p → Π (where Π is the set of min-strategies), which dynamically associates the numerical min-strategies to the reachable Boolean states during analysis. They start with an initial logico-numerical strategy P (0) = λb.π (0) with a chosen numerical min-strategy π (0) and compute a fixed point using logico-numerical Kleene iteration with widening and descending iterations. Then they iteratively improve the min-strategies in P (i) and recompute the fixed point. This approach does not integrate well with mathematical programming because the only known method for computing the fixed point of a logico-numerical strategy is logico-numerical Kleene iteration (with widening). Hence, in contrast to our approach, there is no guarantee to compute the least fixed point.

Comparison with abstract acceleration. Numerous methods have been developed to alleviate the problem of bad extrapolations due to widening, e.g. abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Schrammel | Applying abstract acceleration to (co-)reachability analysis of reactive programs[END_REF][START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF], a method for computing the transitive closure of numerical loops. These methods are able to accelerate some cases of self-loops and cycles with certain types of affine transformations, and they rely on widening in the general case. However, due to the use of general convex polyhedra, they are able to "discover" complex invariant constraints.

In contrast, max-strategy iteration is able to "accelerate" globally the whole transition system regardless of the graph structure or type of affine transformation, and it effectively computes the least fixed point. However, this is only possible on the simpler domain of template polyhedra.

Although the use of template polyhedra is a restriction, this kind of (static) approximation is much more predictable than the (dynamic) approximations made by widening.

Remark 2. Guided static analysis [START_REF] Gopan | Guided static analysis[END_REF] is a framework for analyzing monotonically increasing subsystems, which makes it possible to reduce the impact of widening by applying descending iterations "in the middle" of an analysis. Our algorithm proceeds in a similar fashion -although for different technical reasons -by applying max-strategy iteration on monotonically increasing subsystems.

Experimental Evaluation

We implemented the algorithm in our reactive system verification tool ReaVer7 , which is based on the logico-numerical abstract domain library BddApron [START_REF] Jeannet | BDDAPRON: A logico-numerical abstract domain library[END_REF] Fig. 5: Scalability of logico-numerical max-strategy iteration in comparison with numerical max-strategy iteration on the enumerated CFG, using octagonal constraints. The timeout was set to 3600 seconds. Note the logarithmic scales. and an improved version of the max-strategy iteration solver of Gawlitza et al [START_REF] Dang | Discretizing affine hybrid automata with uncertainty[END_REF]. Since template polyhedra are not yet implemented in the Apron library [START_REF] Jeannet | APRON: A library of numerical abstract domains for static analysis[END_REF], we emulated template polyhedra operations in phase (1) with the help of general polyhedra, which certainly impaired the performance -nonetheless we obtained encouraging results.

Benchmarks. We took 18 benchmarks8 used in [START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF]. These are high-level simulation models (programmed in Lustre) of manufacturing systems which consist of building blocks like sources, buffers, machines and routers that synchronize via handshakes (for this reason there are many Boolean variables). The properties to be verified like maximal throughput time depend on numerical variables. These programs have up to a few hundred lines of code, 27 Boolean and 7 numerical variables, which produce enumerated CFGs of up to 650 locations and 5000 transitions after simplification by Boolean reachability. The focus of the experiments was on comparing the precision of the inferred invariants rather than proving properties.

Results. We performed experiments with octagonal constraints (±x i , x i ± x j ) in order to evaluate efficiency and precision. We compared max-strategy iteration on the enumerated CFGs (MSI) with logico-numerical max-strategy iteration (LNMSI) on CFGs obtained by the static partitioning method by Boolean states implying the same numerical transitions ("numerical modes") from [START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF]. The resulting CFGs are on average five times smaller than the enumerated CFGs for the medium-sized benchmarks.

-LNMSI scales clearly better than MSI (see Fig. 5): our method was on average 9 times faster -for those benchmarks where both methods terminated before the timeout: MSI hit the timeout in 8 out of 18 cases (versus 3 for our method).

The gain in efficiency grows with increasing benchmark sizes. -The precision is almost preserved: only 0.38% (!) of the bounds were worse but still finite, and 0.16% were lost. This precision loss did not impact the number of proved properties. Due to the better scalability we were even able to prove 3 more benchmarks (10 as opposed to 7). -We compared the precision of LNMSI with octagonal constraints with a logiconumerical analysis with octagons using the standard approach with widening (N = 2) and 2 descending iterations on the same CFG. On average 18% of the bounds of our invariants were strictly better than those computed using the standard analysis. In 2 cases these improvements made the difference to prove the property. However, the standard analysis was 19 times faster on average. Furthermore, we experimented with different templates and CFG sizes: -The average gain in speed increases with the template size: 3.3 for interval analysis (±x i ), 5 for zones (±x i , x i -x j ) and 9 for octagons (for those benchmarks which did not run into timeouts). -The precision of LNMSI depends on the CFG size: the general trend is "the bigger the more precise", but the results are less clear: CFGs of the same size seem to have very different quality w.r.t. precision. Partitioning methods which find good partitions matter! -A smaller CFG does not automatically mean faster analysis: the fact that a smaller graph means more complicated logico-numerical transition functions and more numerical strategies per location outweighs the advantage of dealing with less locations. -It is interesting that LNMSI scales also better on the enumerated CFG: it seems to be advantageous to start with a small system with few strategies, iteratively increase the system, and finally, when computing the numerical fixed point of the full system, most of the strategies are already known not to improve the bounds, and thus max-strategy iteration converges faster. We also experimented with LNMSI using the logico-numerical power domain discussed in §3.5, which performed on our CFGs still 6 to 7 times faster on average and with a 100% preservation of bounds compared to MSI.

Conclusions

We presented logico-numerical max-strategy iteration, a solution to the intricate problem of combining numerical max-strategy iteration with techniques that are able to deal with Boolean variables implicitly and therefore allow to trade precision for efficiency.

In contrast to the previous attempt of Sotin et al [START_REF] Sotin | Policy iteration within logiconumerical abstract domains[END_REF] of extending strategy iteration to logico-numerical programs, which relies on widening operators to converge, our method enables the use of mathematical programming and hence, it indeed computes the best logico-numerical invariant w.r.t. the chosen abstract domain.

The effectiveness of our method depends on two factors:

(1) The choice of the templates: in our experiments we used mainly octagonal constraints, but we could have used methods (e.g. [START_REF] Sankaranarayanan | Scalable analysis of linear systems using mathematical programming[END_REF]) for inferring template constraints.

(2) The considered CFG (either of the imperative program, or the one obtained by partitioning in the case of data-flow programs) which determines the abstract domain: the partitioning method by "numerical modes" turned out to be surprisingly effective: compared to the solution based on an enumeration of the reachable Boolean states, the obtained CFGs were 5 times smaller on average, still the precision loss was negligible, i.e. almost zero, and we gained at least one order of magnitude w.r.t. efficiency. Furthermore, this paper delivers the first experimental results of applying numerical max-strategy iteration to larger programs: on the one hand max-strategy iteration is guaranteed to compute more precise invariants than standard techniques in the same domain, on the other hand our implementation is not (yet) able to compete with standard techniques w.r.t. efficiency.

Perspectives. Our algorithm is quite generic w.r.t. the numerical analysis method and logico-numerical abstract domain. Though, in order to tackle efficiency issues evoked above, it would be interesting to design a more integrated logico-numerical max-strategy solver. This would enable to share more information between subsequent calls to the max-strategy iteration, e.g. to avoid retesting of strategies that will definitely not lead to an improvement. Beyond that, we could more extensively use SMT-solvers. For instance, checking whether a strategy is an improvement is currently done after having constructed the numerical equation system; it would be beneficial to find the improving strategies already on the logico-numerical level.

Moreover, we plan to apply our method to the analysis of logico-numerical hybrid automata [START_REF] Schrammel | From hybrid data-flow languages to hybrid automata: A complete translation[END_REF] by extending the hybrid max-strategy iteration method of Dang and Gawlitza [START_REF] Dang | Template-based unbouded time verification of affine hybrid automata[END_REF][START_REF] Dang | Discretizing affine hybrid automata with uncertainty[END_REF].

3

 3

  .

1 S 9 M

 19 := S 0 2 S ′ = post(S) 3 while ¬stable(S, S ′ ) do 4 while ¬p stable(S, S ′ ) do S := S ′ S ′ = post(S) done = generate(S) 10 µ := (δ = d)

Fig. 3 :

 3 Fig. 3: Logico-numerical max-strategy iteration algorithm

Fig. 4 : 1 -

 41 Fig. 4: CFG of the program in Example 1

  in §2.2 shows the CFG of an affine program.

	b1=true; b2=true; x=0;
	while(true)
	{
	while(x<=19) { x = b1 ? x+1 : x-1; }
	while(x<=99) { x = b2 ? x+1 : x; b2 = !b2; }
	if (x>=100) { b1 = (x<=100); x = x-100; }
	}
	Fig. 4 in §3.2 shows a CFG corresponding to this program. Note that we allow
	numerical constraints in assignments to Boolean variables.
	Example 1. An example for such a logico-numerical program is the following C
	program:

The methods presented in this paper will focus on logico-numerical programs with Σ = B p × R n with state vectors s = b x ∈ Σ and relations R(s, s ′ ) with affine, numerical subrelations.

The superscript x is used to distinguish the (numerical) template polyhedra operations from the logico-numerical domain operations that we are going to define in §3.1.

This sharing can be implemented with the help of MtBdds where the numerical abstract values are stored in the leaves[START_REF] Jeannet | BDDAPRON: A logico-numerical abstract domain library[END_REF].

http://pop-art.inrialpes.fr/people/schramme/reaver/

The benchmarks can be downloaded from: http://pop-art.inrialpes.fr/people/schramme/maxstrat/

Acknowledgements. We thank Thomas M. Gawlitza, Bertrand Jeannet, Philipp Rümmer and the anonymous reviewers for their valuable remarks on the draft of this paper.

⋆ This work was partly supported by the Inria large-scale initiative Synchronics.