Antoine Miné

Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations

Keywords: abstract interpretation, static analysis, polyhedra, backward analysis

In this article, we discuss the automatic inference of sufficient pre-conditions by abstract interpretation and sketch the construction of an under-approximating backward analysis. We focus on numeric domains and propose transfer functions, including a lower widening, for polyhedra, without resorting to disjunctive completion nor complementation, while soundly handling non-determinism. Applications include the derivation of sufficient conditions for a program to never step outside an envelope of safe states, or dually to force it to eventually fail. Our construction is preliminary and essentially untried, but we hope to convince that this avenue of research is worth considering.

Introduction

A major problem studied in program verification is the automatic inference of invariants and necessary conditions for programs to be correct. In this article, we consider a related problem: the inference of sufficient conditions.

Consider the simple loop in Fig. 1, where j is incremented by a random value in [0; 1] at each iteration. A forward invariant analysis would find that, at the end of the loop, j ∈ [0; 110] and the assertion can be violated. A backward analysis of necessary conditions would not infer any new condition on the initial value of j because any value in [0; 10] has an execution satisfying the assertion. However, a backward sufficient condition analysis would infer Miné j = [0;10]; i = 0; while (i < 100) { i++; j = j + [0;1]; } assert (j <= 105); that, for the assertion to always hold, it is sufficient to start with j ∈ [0; 5]. Applications of sufficient conditions include: counter-example generation [START_REF] Brauer | Inferring definite counterexamples through under-approximation[END_REF], contract inference [START_REF] Cousot | Precondition inference from intermittent assertions and application to contracts on collections[END_REF], verification driven by temporal properties [START_REF] Massé | Temporal Property-driven Verification by Abstract Interpretation[END_REF], optimizing compilation by hoisting safety checks, etc.

Abstract interpretation [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF] has been applied with some success [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF] to the automatic generation of (over-approximated) invariants, thanks notably to the design of effective abstract domains, in particular numeric domains [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], allowing efficient symbolic computations in domains of infinite size and height. Yet, it has barely been applied to the automatic inference of sufficient conditions (although [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF] discusses under-approximations) and then generally using finite domains or bounded control-flow paths [START_REF] Brauer | Inferring definite counterexamples through under-approximation[END_REF], while logic-based weakest precondition methods [START_REF] Dijkstra | Guarded commands, non-determinacy and formal derivation of programs[END_REF] have thrived. We attribute this lack to the perceived difficulty in designing theoretically optimal [START_REF] Schmidt | Closed and logical relations for over-and under-approximation of powersets[END_REF] as well as practical underapproximations, and the fact that sufficient and necessary conditions differ in the presence of non-determinism. Existing solutions are restricted to deterministic programs, exact abstract domains (e.g., disjunctive completions, which do not scale well), or set-complements of over-approximating domains (e.g., disjunctions of linear inequalities, that cannot express invariants as simple as j ∈ [0; 5]). We present here a preliminary work that hints towards the opposite: it seems possible to define reasonably practical (although non-optimal) polyhedral abstract under-approximations for non-deterministic programs.

Section 2 introduces sufficient conditions at the level of transition systems. Section 3 presents some algebraic properties of backward functions, which are exploited in Sec. 4 to design under-approximated operators for polyhedra. Section 5 discusses related work and Sec. 6 concludes.

Transition Systems

Invariants and sufficient conditions

To stay general, we consider, following [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF], a small-step operational semantics and model programs as transition systems (Σ, τ ); Σ is a set of states and τ ⊆ Σ × Σ is a transition relation. An execution trace is a finite or infinite countable sequence of states (σ 1 , . . . , σ i , . . .) ∈ Σ ∞ such that ∀i : (σ i , σ i+1 ) ∈ τ .

Invariants. The invariant inference problem consists in, given a set I ⊆ Σ of initial states, inferring the set inv(I) of states encountered in all executions Miné starting in I. This set can be expressed as a fixpoint following Cousot [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF]:

3 inv(I) = lfp I λX.X ∪ post(X) (1)
where lfp x f is the least fixpoint of f greater than or equal to x and post(X)

def = { σ ∈ Σ | ∃σ ∈ X : (σ , σ) ∈ τ }.
Sufficient conditions. In this article, we consider the reverse problem: sufficient condition inference, which consists in, given an invariant set T to obey, inferring the set of initial states cond(T ) that guarantee that all executions stay in T . It is also given in fixpoint form following Bourdoncle [START_REF] Bourdoncle | Abstract debugging of higher-order imperative languages[END_REF]:

4 cond(T ) = gfp T λX.X ∩ pre(X) (2)
where gfp x f is the greatest fixpoint of f smaller than or equal to x and pre(X)

def = { σ ∈ Σ | ∀σ ∈ Σ : (σ, σ ) ∈ τ =⇒ σ ∈ X }. cond(T )
is indeed a sufficient condition and, in fact, the most general sufficient condition:

Theorem 2.1 ∀T, X : inv(cond(T )) ⊆ T and inv(X) ⊆ T =⇒ X ⊆ cond(T ).
Non-determinism. The function pre we use differs from the function pre used in most backward analyses [START_REF] Bourdoncle | Abstract debugging of higher-order imperative languages[END_REF][START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF][START_REF]Understanding the origin of alarms in Astrée[END_REF] and defined as pre(X)

def = { σ ∈ Σ | ∃σ ∈ X : (σ, σ ) ∈ τ }.
Indeed, pre(X) = pre(X) when the transition system is non-deterministic, i.e., some states have several successors or none. Nondeterminism is useful to model unspecified parts of programs, such as the interaction with unanalyzed libraries or with the environment (as in Fig. 1), and permits further abstractions (Sec. 4.6). Using pre ensures that the target invariant T holds for all the (possibly infinite) sequences of choices made at each execution step, while pre would infer conditions for the invariant to hold for at least one sequence of choices, but not necessarily all (a laxer condition).

Blocking states. Any state σ without a successor satisfies ∀X : σ ∈ pre(X), and so, σ ∈ T =⇒ σ ∈ cond(T ). Such states correspond to a normal or abnormal program termination -e.g., the statement y = 1/x generates a transition only from states where x = 0. In the following, we assume the absence of blocking states by adding transitions to self-looping states: error states transition to a self-loop ω / ∈ T , and normal termination states transition to a self-loop α ∈ T , so that no erroneous execution can stem from cond(T ).

Approximation. Transition systems can become large or infinite, so that inv(I) and cond(T ) cannot be computed efficiently or at all. We settle for sound approximations. Invariant sets are over-approximated in order to be certain Miné to include all program behaviors. Sufficient condition sets are dually underapproximated as any subset I ⊆ cond(T ) still satisfies inv(I ) ⊆ T .

Applications of sufficient conditions

This section presents a few applications of computing an under-approximation of cond(T ). The rest of the paper focuses on how to compute it effectively.

Given a set of initial states I, the subset of initial states that never lead to a run-time error nor assertion violation can be expressed as I ω def = I ∩ cond(Σ \ {ω}). An analyzer computing an under-approximation of I ω infers sufficient initial conditions so that all executions are correct (i.e., never reach ω). Applied to a single function, it infers sufficient conditions on its parameters and global entry state ensuring its correct behavior. An application to software engineering is the automatic inference of method contracts. An application to optimizing compilation is run-time check hoisting: a fast version of the function without any check is called instead of the regular one if, at the function entry, sufficient conditions making these checks useless hold.

As last application, we consider the automatic inference of counterexamples. Given a set T of target states (e.g., erroneous states), we seek initial conditions such that all the executions eventually reach a state in T . In that case, Thm. 2.1 cannot be directly applied as it focuses on invariance properties while we are now interested in an inevitability property. We now show that this problem can nevertheless be reduced to an invariance one, of the form cond(T ) for some T . We use an idea proposed by Cousot et al. [START_REF] Cousot | An abstract interpretation framework for termination[END_REF] for the analysis of termination (another inevitability property): we enrich the transition system with a counter variable l counting execution steps from some positive value down to 0 when reaching T . Given (Σ, τ ) and T ⊆ Σ, we construct (Σ , τ ) and T as:

Σ def = Σ × N, T def = { (σ, l) ∈ Σ | l > 0 ∨ σ ∈ T } ((σ, l), (σ , l )) ∈ τ def ⇐⇒ ((σ / ∈ T ∧ (σ, σ ) ∈ τ ) ∨ σ = σ ∈ T ) ∧ l = l + 1
This transformation is always sound and sometimes complete:

Theorem 2.2 If (σ, l) ∈ cond(T )
, then all the traces starting in σ eventually enter a state in T . If the non-determinism in τ is finite,5 the converse holds.

The restriction to finite non-determinism may hinder the analysis of fair systems, as an infinite number of countable choices must be performed, e.g.:

while ([0; 1]) { n = [0; +∞]; while (n > 0) { n = n -1 } } . 6
Program semantics are not generally defined as monolithic transition systems, but rather as compositions of small reusable blocks. To each atomic language instruction i corresponds a forward transfer function post i , and we will construct backward transfer functions directly from these post i . Formally, given a function f : P(X) → P(Y ), we define its backward version ←f as:

← - f : P(Y ) → P(X) s.t. ← - f (B) def = { a ∈ X | f ({a}) ⊆ B } . (3)
We note immediately that ← -post = pre. Moreover, ← -• enjoys useful properties. We list a few ones to give a gist of the underlying algebraic structure:

Theorem 3.1 (i) ← - f is a monotonic, complete ∩-morphism. (ii) ← - f is a sup-∪-morphism: ∪ i∈I ← - f (B i ) ⊆ ← - f (∪ i∈I B i ) (in general it is not a ∪-morphism, nor is it strict, even when f is). (iii) If f is a strict complete ∪-morphism, then A ⊆ ← - f (B) ⇐⇒ f (A) ⊆ B,
that is, we have a Galois connection:

P(X) ---→ ← --- f ← - f P(Y ). (iv) ← --- f ∪ g = ← - f ∩ ← -g (note that ∪, ∩, ⊆ are extended point-wise to functions). (v) ← --- f ∩ g ⊇ ← - f ∪ ← -g (in general, the equality does not hold). (vi) If f is monotonic, then ←-- f • g ⊆ ← -g • ← - f . (vii) If f is a strict complete ∪-morphism, then ←-- f • g = ← -g • ← - f . (viii) f ⊆ g =⇒ ← -g ⊆ ← - f . (ix) If f and g are strict complete ∪-morphisms, then f ⊆ g ⇐⇒ ← -g ⊆ ← - f . (x) If f is a strict complete ∪-morphism, then ←-------------- λx.lfp x (λz.z ∪ f (z)) = λy.gfp y (λz.z ∩ ← - f (z)).
Property iv is useful to handle semantics expressed as systems of flow equations ∀i : X i = ∪ j F i,j (X j ); we get: ∀j :

X j = ∩ j ← - F i,j (X i ).
Compositional semantics make use of •, ∪, and nested least fixpoints (vii, iv, x). Properties iii and x generalize Thm. 2.1 and Eq. 2. Finally, viii-ix, turn forward overapproximations into backward under-approximations. All these properties will also be useful to design abstract operators for atomic statements, in Sec. 4.

Under-Approximated Polyhedral Operators

We use the results of the previous section to design practical backward operators sufficient to implement an analysis. We focus on numeric properties that we abstract using convex closed polyhedra (although the ideas we present can be used in other linear inequality domains, such as intervals or octagons). Familiarity with the over-approximating polyhedron domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] is assumed.

Miné (a) ← -τ y ≤ 0 (b) ← -τ y ≤ 0 (c) ← -τ y ≤ 0 (d) ← -τ y ≤ 0
We assume a set V of variables with value in

Q. Environments ρ ∈ E def = V → Q map each variable to its value in Q. A polyhedron P can be encoded as a set C = { c 1 , . . . , c n } of affine constraints c i = (a i • x ≥ b i ), which represents γ c (C) def = { ρ ∈ E | ∀(a • x ≥ b) ∈ C : a • ρ(x) ≥ b },
but also as a set of vertices and rays (V, R), so called generators, which represents

γ g (V, R) def = { v∈V α v v + r∈R β r r | α v , β r ≥ 0, v∈V α v = 1 }.
Here, a denotes a vector, • is the dot product, and ρ(x) is the vector of variable values in environment ρ. Given a statement s, we denote by τ {| s | } its forward concrete transfer function, and by ← -

τ {| s | } its backward version ← -τ {| s | } def = ← --- τ {| s | }.
Note that ∅ can always be used to under-approximate any ←τ {| s | }, the same way over-approximating analyzers soundly bail-out with E in case of a timeout or unimplemented operation. Because backward operators are generally not strict (i.e., ←f (∅) = ∅, as the tests in Sec. 4.1), returning ∅ at some point does not prevent finding a non-empty sufficient condition at the entry point; it only means that the analysis forces some program branch to be dead.

Tests

We first consider simple affine tests a • x ≥ b. We have:

τ {| a • x ≥ b? | } R def = { ρ ∈ R | a • ρ(x) ≥ b } and so ← -τ {| a • x ≥ b? | } R = R ∪ { ρ ∈ E | a • ρ(x) < b }
On polyhedra, forward affine tests are handled exactly by simply adding the constraint. However, the result of a backward affine test on a closed convex set is generally not closed nor convex (see Fig. 2.a), so, we need an actual under-approximation. One solution is to remove a • x ≥ b from the set C, as:

Theorem 4.1 γ c (C \ {a • x ≥ b}) ⊆ ← -τ {| a • x ≥ b? | } γ c (C).
Sometimes, this results in the identity (Fig. 2.b) which is indeed a (trivial) under-approximation. More precise (i.e., larger) under-approximations can be computed by removing the constraints that are redundant in C ∪ {a • x ≥ b}.

Miné

Intuitively, these are constraints that restrict γ c (C) in the half-space a • x < b, while the test result is not restricted in this half-space (Fig. 2.c). In practice, we first add a•x ≥ b, then remove redundant constraints, then remove a•x ≥ b.

Consider now the degenerate case where γ c (C) |= a • x = b (Fig. 2.d). Constraint representations are not unique, and different choices may result in different outcomes. To guide us, we exploit the fact that tests come in pairs, one for each program branch: while a forward semantics computes, at a branch split, (Y,

Z) = (τ {| a • x ≥ b? | } X, τ {| a • x < b? | } X), the backward compu- tation merges both branches as X = ← -τ {| a • x ≥ b? | } Y ∩ ← -τ {| a • x < b? | } Z. Assuming that Y = γ g (V Y , R Y ) is degenerate, we construct a non-degenerate polyhedron before computing ← -τ {| a • x ≥ b? | } by adding the rays r from Z such that τ {| a • x ≥ b? | } γ g (V Y , R Y ∪ {r}) = τ {| a • x ≥ b? | } γ g (V Y , R Y ). The effect is to create common rays in ← -τ {| a • x ≥ b? | } Y and ← -τ {| a • x < b? | } Z
to make the subsequent intersection as large as possible. This simple heuristic is sufficient to analyze Fig. 1 (where the degeneracy comes from the invariant i = 100 at loop exit) but it is nevertheless fragile and begs to be improved.

To handle strict tests, we note that τ {| a • x ≥ b? | } over-approximates τ {| a • x > b? | }, and so, by Thm.

3.1.viii, ← -τ {| a • x > b? | } can be under- approximated by ← -τ {| a • x ≥ b? | }. Similarly for non-deterministic tests, τ {| a • x ≥ [b; c]? | } = τ {| a • x ≥ b? | }, and so, ← -τ {| a • x ≥ [b; c]? | } is modeled as ← -τ {| a • x ≥ b? | }.
We will see in Sec. 4.6 that non-linear tests can be abstracted into such non-deterministic affine ones. Finally, boolean combinations of tests are handled as follows, using Thm. 3.1.iv,vii:

7 τ {| t 1 ∨ t 2 | } = τ {| t 1 | } ∪ τ {| t 2 | } and so ← -τ {| t 1 ∨ t 2 | } = ← -τ {| t 1 | } ∩ ← -τ {| t 2 | } τ {| t 1 ∧ t 2 | } = τ {| t 2 | } • τ {| t 1 | } and so ← -τ {| t 1 ∧ t 2 | } = ← -τ {| t 1 | } • ← -τ {| t 2 | } For instance, ← -τ {| a • x = [b; c]? | } = ← -τ {| a • x ≥ b? | } • ← -τ {| (-a) • x ≥ -c? | }.

Projection

Given a variable V , projecting it forgets its value:

τ {| V := ? | } R def = { ρ[V → v] | ρ ∈ R, v ∈ Q } and so ← -τ {| V := ? | } R = { ρ ∈ E | ∀v ∈ Q : ρ[V → v] ∈ R }
We have the following property:

Theorem 4.2 If R is convex closed, then ← -τ {| V := ? | } R is either R or ∅.
The projection can be efficiently and exactly implemented for polyhedra as: if τ {| V := ? | } P = P then ←τ {| V := ? | } P = P , otherwise ←τ {| V := ? | } P = ∅. Adding and removing an uninitialized variable can then be derived as follows:

Miné ← -τ {| del V | } = τ {| add V | } ← -τ {| add V | } = τ {| del V | } • ← -τ {| V := ? | }

Assignments

By Thm. 3.1.viii, and given that the forward projection over-approximates any assignment, the backward projection can be used to under-approximate any assignment, but this is rather coarse. More interestingly, general assignments can be reduced to tests by introducing a temporary variable V . We note [V /V ] the renaming of V as V . We have:

τ {| V := e | } = [V /V ] • τ {| del V | } • τ {| V = e? | } • τ {| add V | } and so ← -τ {| V := e | } = ← -τ {| add V | } • ← -τ {| V = e? | } • ← -τ {| del V | } • [V /V ]
In case of degeneracy on a test argument, Sec. 4.1 relied on rays provided by another polyhedron to guide the operation. We do not have another polyhedron here, but we know that the test is followed by a projection (as part of ←τ {| add V | }), hence, the heuristic is modified to use the rays V and -V .

Intuitively, we try to maximize the set of environments ρ such that the result of the test contains

{ ρ[V → v] | v ∈ Q },
and so, will be kept by ←τ {| V := ? | }.

Moreover, some restricted yet useful classes of assignments enjoy more direct abstractions, based solely on forward operators, such as:

Theorem 4.3 (i) ← -τ {| V := [a; b] | } = τ {| V := ? | } • (τ {| V := V -a | } ∩ τ {| V := V -b | }) • τ {| V ≥ a? ∧ V ≤ b? | }). (ii) ← -τ {| V := V + [a; b] | } = τ {| V := V -a | } ∩ τ {| V := V -b | }. (iii) ← -τ {| V := W | } = τ {| V := ? | } • τ {| V = W ? | } (when V = W ).
(iv) If V := e is invertible, i.e., there exists an expression e -1 such that

τ {| V := e -1 | } • τ {| V := e | } = τ {| V := e | } • τ {| V := e -1 | } = λR.R, then ← -τ {| V := e | } = τ {| V := e -1 | } -e.g., V := W α W W with α V = 0.

Lower widening

Invariance semantics by abstract interpretation feature least fixpoints, e.g., to handle loops and solve equation systems. Traditionally, they are solved by iteration with an upper convergence acceleration operator, the widening [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF]. To compute sufficient conditions, we under-approximate greatest fixpoints instead (Eq. 2 and Thm. 3.1.x). We thus define a lower widening obeying:

(i) γ(A B) ⊆ γ(A) ∩ γ(B). (ii) For any sequence (X n ) n∈N , the sequence Y 0 = X 0 , Y n+1 = Y n X n+1 Miné stabilizes: ∃i : Y i+1 = Y i .
As a consequence, for any under-approximation F of a concrete operator F , and any X 0 , the sequence X i+1 = X i F (X i ) stabilizes in finite time to some X δ ; moreover, this X δ satisfies γ(X δ ) ⊆ gfp γ(X 0 ) F [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF]. On polyhedra, by analogy with the widening [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] that keeps only stable constraints, we define a lower widening that keeps only stable generators. Let V P and R P denote the vertices and rays of a polyhedron P = γ g (V P , R P ). We define formally as:

V A B def = { v ∈ V A | v ∈ B } R A B def = { r ∈ R A | B ⊕ R + r = B } (4)
where

⊕ denotes the Minkowski sum (A ⊕ B def = { a + b | a ∈ A, b ∈ B }) and R + r denotes the set { λr | λ ≥ 0 }). We have: Theorem 4.4
is a lower widening.

Generator representations are not unique, and the output of depends on the choice of representation. The same issue occurs for the standard widening. We can use a similar fix: we add to A B any generator from B that is redundant with a generator in A. Our lower widening can also be refined in a classic way by permitting thresholds: given a finite set of vertices (resp. rays), each vertex v (resp. ray r) included in both polyhedra A and B (v ∈ A∧v ∈ B, resp. A⊕R + r = A∧B ⊕R + r = B) is added to A B. As for any extrapolation operator, the effectiveness of will need, in future work, to be assessed in practice. There is ample room for improvement and adaptation.

Lower widenings are introduced in [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF] but, up to our knowledge, and unlike (upper) widenings, no practical instance on infinite domains has ever been designed. Lower widenings are designed to "jump below" fixpoints (hence performing an induction) and should not be confused with narrowing operators that "stay above" fixpoints (performing a refinement).

Joins

In invariance analyses, unions of environment sets are computed at every control flow join. Naturally, a large effort in abstract analysis design is spent designing precise and efficient over-approximations of unions. By the duality of Thm. 3.1.iv, such joins do not occur in sufficient condition analyses; they are replaced with intersections ∩ at control-flow splits, and these are easier to abstract in most domain (e.g., polyhedra). Hence, we avoid the issue of designing under-approximations of arbitrary unions. We do under-approximate unions as part of test operators (Sec. 4.1), but these have a very specific form which helped us design the approximation.

Expression approximation

We focused previously on affine tests and assignments because they match the expressive power of polyhedra, but programs feature more complex expressions. In [START_REF] Miné | Symbolic methods to enhance the precision of numerical abstract domains[END_REF], we proposed to solve this problem for over-approximating transfer functions using an expression abstraction mechanism. We noted e D f the fact that f approximates e on D, i.e., ∀ρ ∈ D : e ρ ⊆ f ρ, where

• : E → P(Q) evaluates an expression in an environment. Then:

if R ⊆ D then τ {| V := e | } R ⊆ τ {| V := f | } R and τ {| e? | } R ⊆ τ {| f ? | } R
so, in the abstract, e can be replaced with f if the argument A satisfies e γ(A ) f . We now show that this method also works for under-approximations:

Theorem 4.5 If e D f , we have:

(i) ← -τ {| V := e | } R ⊇ ( ← -τ {| V := f | } R) ∩ D. (ii) ← -τ {| e? | } R ⊇ ( ← -τ {| f ? | } R) ∩ D.
We study the case of abstract assignments (tests are similar): ) f . One way to construct f is to use the "linearization" from [START_REF] Miné | Symbolic methods to enhance the precision of numerical abstract domains[END_REF]: it converts an arbitrary expression into an expression of the form V α V V + [a; b] by performing interval arithmetics on non-linear parts, using variable bounds from D . The theorem does not make any hypothesis on the choice of D (unlike the case of forward analysis). A smaller D improves the precision of f by making [a; b] tighter, but, as we want to maximize the result of the backward assignment, we should avoid discarding states in ←τ {|

← -τ {| V := e | } A can be replaced with ← -τ {| V := f | } A ∩ D if e γ(D
V := f | }R but not in ← -τ {| V := f | }R∩D.
In practice, we use for D the result γ(D ) of a prior invariance analysis as we know that, in the concrete,

← -τ {| V := e | } R ⊆ γ(D ). For instance, the assignment ← -τ {| X ← Y × Z | } R will be replaced with ← -τ {| X ← Y × [0; 1] | } R ∩ D if the invariant γ(D ) before the assignment implies that Z ∈ [0; 1].
It may seem counter-intuitive that over-approximating expressions results in under-approximating backward transfer functions. Observe that overapproximations enlarge the non-determinism of expressions, and so, make it less likely to find sufficient conditions holding for all cases.

Implementation

We have implemented a proof-of-concept analyzer [START_REF] Miné | The Banal static analyzer prototype[END_REF] that infers sufficient pre-conditions for programs written in a toy language to never violate any user-specified assertion. It first performs a classic forward over-approximating analysis, followed with a backward under-approximating one. All the abstract operators are implemented with polyhedra, on top of the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. It is able to find the sufficient condition j ∈ [0; 5] in the example of Fig. 1. We also analyzed the BubbleSort example that introduced polyhedral analysis [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF].

Miné 5 Related Work

Since their introduction by Dijkstra [START_REF] Dijkstra | Guarded commands, non-determinacy and formal derivation of programs[END_REF], weakest (liberal) preconditions have been much studied, using a variety of inference and checking methods, including interactive theorem proving [START_REF] Flanagan | Extended static checking for Java[END_REF] and automatic finite-state computations. These methods are exact (possibly with respect to an abstract model overapproximating the concrete system, so that sufficient conditions on the model do not always give sufficient conditions for the original system). Fully automatic methods based on under-approximations are less common.

Bourdoncle introduces [START_REF] Bourdoncle | Abstract debugging of higher-order imperative languages[END_REF] sufficient conditions, denoted always(T ), but only focuses on deterministic systems (i.e., pre = pre). He also mentions that classic domains, such as intervals, are inadequate to express underapproximations as they are not closed under complementation, but he does not propose an alternative. Moy [START_REF] Moy | Sufficient preconditions for modular assertion checking[END_REF] solves this issue by allowing disjunctions of abstract states (they correspond to path enumerations and can grow arbitrarily large). Lev-Ami et al. [START_REF] Lev-Ami | Backward analysis for inferring quantified pre-conditions[END_REF] derive under-approximations from overapproximations by assuming, similarly, that abstract domains are closed by complementation (or negation, when seen as formulas). Brauer et al. [START_REF] Brauer | Inferring definite counterexamples through under-approximation[END_REF] employ boolean formulas on a bit-vector (finite) domain. These domains are more costly than classic convex ones, and our method is not limited to them.

Schmidt [START_REF] Schmidt | Closed and logical relations for over-and under-approximation of powersets[END_REF] defines Galois Connections (and so best operators) for all four backward/forward over-/under-approximation cases using a higher-order powerset construction. Massé [START_REF] Massé | Temporal Property-driven Verification by Abstract Interpretation[END_REF] proposes an analysis parametrized by arbitrary temporal properties, including pre operators, based on abstract domains for lower closure operators. We shy away from higher-order constructions. We may lose optimality and generality, but achieve a more straightforward and, we believe, practical framework. In particular, we do not change the semantics of abstract elements, but only add new transfer functions, and achieve the same algorithmic complexity as forward analyses.

Cousot et al. [START_REF] Cousot | Precondition inference from intermittent assertions and application to contracts on collections[END_REF] propose a backward precondition analysis for contracts. It differs from the weakest precondition approach we follow in its treatment of non-determinism: it keeps states that, for some sequence of choices (but not necessarily all), give rise to a non-erroneous execution. Our handling of inevitability is directly inspired from Cousot et al. [START_REF] Cousot | An abstract interpretation framework for termination[END_REF].

Conclusion

In this article, we have discussed the inference of sufficient conditions by abstract interpretation. We have presented general properties of backward under-approximated semantics, and proposed example transfer functions in the polyhedra domain. Much work remains to be done, including designing new under-approximated operators (tests and lower widenings, in particular), Miné considering new domains, experimenting on realistic programs. Our construction and results are very preliminary and remain mostly untried; our hope is only to convince the reader that this constitutes a fruitful avenue of research.

Fig. 1 .

 1 Fig. 1. Simple loop example.

Fig. 2 .

 2 Fig. 2. Modeling the test y ≤ 0 backwards in the concrete (a) and with polyhedra (b)-(d).

Miné

This work is supported by the INRIA project "Abstraction" common to CNRS and ENS in France.

Email: mine@di.ens.fr c 2012 Published by Elsevier Science B. V.

In[START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF], Cousot notes it sp(τ * ) and defines it rather as lfp λX.I ∪ post(X). Both formulations are equivalent: both equal ∪ n≥0 post n (I) because post is a complete ∪-morphism in the complete lattice (P(Σ), ⊆, ∪, ∩).

[START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF] In[START_REF] Bourdoncle | Abstract debugging of higher-order imperative languages[END_REF], Bourdoncle calls this set always(T ) and defines it equivalently as gfp λX.T ∩ pre(X), but only considers the case where ∀σ : | post({σ})| = 1, i.e., pre = pre.

I.e., ∀σ : post({σ}) is finite, which is weaker than requiring a bounded non-determinism.

Note that, if the number of infinite choices is bounded, they can be embedded as fresh non-initialized variables to obtain a program with finite non-determinism.

We avoid the use of ∩ for ∧ as it does not behave well with respect to ← -• , see Thm. 3.1.v.