Marco Milanese

Antoine Miné

Generation of Violation Witnesses by Under-Approximating Abstract Interpretation

Keywords: Abstract interpretation, Software verication, Program analysis, Bug catching, Under-approximation

Generation of Violation Witnesses by Under-Approximating

Introduction

The focus of static analysis by abstract interpretation [START_REF] Cousot | Abstract interpretation: a unied lattice model for static analysis of programs by construction or approximation of xpoints[END_REF][START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] has traditionally been on the assurance of program correctness. However, the dual problem of verifying the presence of bugs is equally intriguing, since in practice sound static analysis tools generate many false positives and checking them manually can be time-consuming. This calls for a novel kind of abstract semantics where domains and operators are under-approximated rather than over-approximated.

A preliminary study in this area was done in our previous work [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF], where we investigated an abstract backward semantic to infer sucient program preconditions. This analysis builds on conventional abstract domains, but in this analysis they represent an under-approximation of the concrete invariant. To achieve this analysis, novel under-approximation domain operators are required, and in [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] we have shown how they can be designed for the polyhedra domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. The results were implemented in a static analysis tool targeting a toy language.

unsigned int i = 10; while (i >= 10) { i++; } i += input(); assert(i != 5);

(a) Program with integer overow and input.

int i = input(); int j; assume(i >= 0 && i <= 2); if (i == 0) j = 0; else if (i == 1) j = 1; else if (i == 2) j = 0; assert(j == 1);

(b) Simple disjunctive program.

Fig. 1: Programs that show the limits of the semantics of [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF].

Motivation. Consider the program of Fig. 1a. The while loop starts with i = 10 and terminates when i overows to 0. Therefore, if input() returns 5 the assertion will fail. Unfortunately the semantic proposed in [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] can not detect the overow as it only supports mathematical numbers (i.e., numbers with innite precision). Moreover in this semantic there is no built-in encoding for user input and thus the preconditions that it can nd concern only program's arguments. Consequently, it can not nd the sucient precondition, input() = 5, for the assertion to fail.

Additionally, under-approximated operators were studied only for the polyhedra domain, but as for conventional abstract interpretation, other domains can be considered and the choice of the domain boils down to a precision-eciency trade-o. As an example, the polyhedra domain fails to nd the sucient precondition, input() = 1, for the correctness of the program of Fig 1b as the invariant before the assertion, (i ∈ {0, 2} ∧ j = 0) ∨ (i = 1 ∧ j = 1), is not polyhedral.

Termination. The preconditions found by this analysis under-approximate Dijkstra's weakest liberal precondition, ensuring either divergence or termination within the post-condition. The former case can be problematic, such as when the analysis is used to nd preconditions for bugs, as a non-empty precondition may be a symptom of an innite loop rather than an actual bug. However, non-termination can be ruled out with various techniques, including termination checking with a ranking function and modern works on its synthesis have been quite successful [START_REF] Cook | Terminator: Beyond safety: (tool paper)[END_REF][START_REF] Colóon | Synthesis of linear ranking functions[END_REF]. For the sake of simplicity we do not implement those techniques and instead opt for a simple approach of checking termination by experimentally executing the program (with a time limit). Related Works. Lately there has been an increase in interest on underapproximations following the seminal work of Peter O'Hearn on Reverse Hoare Logic/Incorrectness Logic [START_REF] De Vries | Reverse hoare logic[END_REF][START_REF] O'hearn | Incorrectness logic[END_REF]. Compared to our approach, this stream of works focuses on forward, not backward, analyses, thus they do not study preconditions for bugs but instead they nd post-conditions for them. Moreover, as logic methods, they can prove that a post-condition is a valid under-approximation of the reachable states. Some hints on how post-conditions can be inferred were discussed in [START_REF] O'hearn | Incorrectness logic[END_REF]Sect. 6], but they handle loops by unrolling, thus limiting the analysis to some loop bound. On the contrary, our approach can infer preconditions and loops are handled with widening operators, so that unrolling is not needed and unbounded loops can be handled. Incorrectness logic was made memory aware by Raad et al. [START_REF] Raad | Local reasoning about the presence of bugs: Incorrectness separation logic[END_REF] using ideas from separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. In comparison, our work focuses exclusively on numeric programs and abstract domains for handling memory properties are left as a future work. Finally, reasoning with incorrectness logic can be made automatic with theorem provers as in [START_REF] Le | Finding real bugs in big programs with incorrectness logic[END_REF][START_REF] Raad | Local reasoning about the presence of bugs: Incorrectness separation logic[END_REF], whereas in our work, reasoning occurs with abstract domains. This makes the analysis more scalable.

Counter-examples generation is also possible with several instances of model checking, e.g., symbolic execution [START_REF] King | Symbolic execution and program testing[END_REF][START_REF] Baldoni | A survey of symbolic execution techniques[END_REF] and CEGAR [START_REF] Clarke | Counterexample-guided abstraction renement for symbolic model checking[END_REF], where the state exploration is handled using SMT solvers (CEGAR is guided by counter-examples and utilizes other techniques besides SMT for the renement phase, e.g., interpolants).

Traditional backward analyses based on abstract interpretation [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF][START_REF] Cousot | Rening model checking by abstract interpretation[END_REF][START_REF] Bourdoncle | Abstract debugging of higher-order imperative languages[END_REF] focus on inferring necessary preconditions P , that is conditions such that no execution starting from ¬P can succeed. For example 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 code contracts. They dier from us in the handling of non-determinism as they keep states that succeed at least for one non-deterministic program path, whereas we keep states that succeed for all non-deterministic paths. Moreover, unlike us, they use symbolic reasoning, not numeric domains.

In this work we focus on sucient preconditions P , that is conditions such that all executions from P must succeed: these require under-approximated operators. Designing under-approximation domains featuring optimal operators can be challenging [START_REF] Ascari | Limits and diculties in the design of underapproximation abstract domains[END_REF] at least partially explaining why they are rarer than overapproximation ones. Several high-order constructions have been proposed in which conventional domains are used to construct under-approximation ones.

Lev-Ami et al. [START_REF] Lev-Ami | Backward analysis for inferring quantied preconditions[END_REF] propose to use set-complements of abstract domains, but this yields shapes that are rarely interesting. Other methods based on existential quantication [START_REF] Schmidt | A calculus of logical relations for over-and underapproximating static analyses[END_REF] and disjunctive completions [START_REF] Moy | Sucient preconditions for modular assertion checking[END_REF] were proposed, but they incur in a too high complexity and are dicult to abstract away.

Under-approximations were used also in the work of Urban et al. [START_REF] Urban | Abstract interpretation of ctl properties[END_REF], namely for the co-domain. However, the results are dicult to compare in theory due to dierent abstractions and dierent concrete semantics.

Contribution. In this paper we extend upon the backward sucient preconditions analysis, addressing some of the limitations that hinder its applicability to C-like programs, namely: handling of user input and integer wrapping.

To improve the precision of the polyhedra domain, we consider the well-known power-set construction and derive sound under-approximation operators for it.

We then proceed to implement the improved analysis in a static analysis tool and add support for extracting a violation witness in SV-COMP's format [START_REF] Beyer | Witness validation and stepwise testication across software veriers[END_REF]. To the best of our knowledge, this is the rst abstract interpretation based tool that can certify program incorrectness (at least among the ones participating in SV-COMP). We compare its performance with that of other static analysis tools participating in SV-COMP23 [START_REF] Beyer | Competition on software verication and witness validation: Sv-comp 2023[END_REF] on a selected subset of the competition's benchmarks.

a ::= [x, y] | v | a1 + a2 | a1 -a2 | a1 * a2 | a1/a2 b ::= a1 = a2 | a1 ̸ = a2 | a1 ≤ a2 | a1 < a2 | a1 > a2 | a1 ≥ a2 | t | f | ¬b | b1 ∧ b2 | b1 ∨ b2 s ::= skip() | v := a | assume(b) | s1; s2 | if b then s1 else s2 | while b do s done

Semantics

The semantic studied in [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] is limited to numeric variables and properties and is given for a toy language with mathematical numbers. In this paper, we address how it can be adapted to support xed-precision integers and user input.

Handling more advanced features of C-like languages, such as pointers, arrays, structures, dynamic memory allocation, remains a future work. Floating-point arithmetic is out of the scope of this work but it should not be a large problem as [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] shows that expression evaluation can be over-approximated and still leads to sound under-approximated statements, thus rounding errors can be abstracted as small non-deterministic error intervals, as in forward analysis, and easily supported in a polyhedral analysis. This section is organized as follows: in 2.2 we recall the semantics of [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF], then in 2.3 we extend it with user input and in 2.4 with nite-precision integers.

Notation

Given a set X, we denote with P(X) the set of all subsets of X. If f is a function, then dom(f ) denotes its domain. If X is a poset and f : X → X, we denote with gfp R f the greatest x-point of f less or equal than R.

Background on Sucient Preconditions Semantic

We recall here the semantics from [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF], on top of which we construct our new analysis. The analysis is given both in equational form (where the program is represented as a control ow graph) and in big-step form (where the program is represented with an inductive language), for our purposes we only consider the latter. Language and Forward Semantics. We assume a simple While programming language with assume(b), assignments and skip() atomic statements and sequencing, if-then-else and while loops inductive statements (see Fig. 2). The set of variables is denoted with V and it is assumed to be xed. Variables are of mathematic integer type, hence program stores (or environments) are in E ≜ V → Z. Arithmetic and boolean expressions are interpreted respectively by E[[a]] : P(E) → P(Z) and B[[b]] : P(E) → P({t, f}), whereas statements by τ [[s]] : P(E) → P(E). For more details we refer the reader to [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF][START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF]. Backward Semantic. Conventional backward analyses focus on inferring necessary preconditions for some post-condition. In particular, given a program s ∈ While and a post-condition S ∈ P(E), they infer an over-approximation (an over-approximation of a necessary precondition is again a necessary precondi-

← τ [[skip()]]S ≜ S ← τ [[v := a]]S ≜ {ρ | ∀x ∈ E[[a]]ρ. ρ[v → x] ∈ S} ← τ [[assume(b)]]S ≜ S ∪ {ρ | B[[b]]ρ = {f}} ← τ [[s1; s2]]S ≜ ( ← τ [[s1]] • ← τ [[s2]])S ← τ [[if b then s1 else s2]]S ≜ ( ← τ [[assume(b)]] • ← τ [[s1]])S ∩ ( ← τ [[assume(¬b)]] • ← τ [[s2]])S ← τ [[while b do s done]]S ≜ gfp← τ [[¬b]] (λX. X ∩ ( ← τ [[assume(b)]] • ← τ [[s]])X)
tion) of P n ≜ {ρ | ∃ρ ′ ∈ τ [[s]]{ρ}. ρ ′ ∈ S}. Notice that if τ [[s]
]{ρ} ∈ S then ρ ∈ P n , i.e., if a store ρ transitions to S, then it is contained in P n .

On the contrary, the backward analysis proposed in [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] infers sucient preconditions. In particular, it infers an under-approximation (an underapproximation of a sucient precondition is again a sucient precondition) of

P s ≜ {ρ | ∀ρ ′ ∈ τ [[s]]{ρ}. ρ ′ ∈ S}.
← f (B) ≜ {a ∈ A | f ({a}) ⊆ B}. In particular, letting f ≡ τ [[s]] yields ← τ [[s]
] that computes the sucient precondition of s. Backward versions of functions enjoy several properties and in 1 With an abuse of notation we confuse the store [x → z] with z.

particular we can exploit them to compute ← τ [[s]] by induction on the syntax of s. We report the resulting backward semantic in Fig. 3 and refer the reader to Theorems 2 and 3 of [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] for further details (in particular, the soundness of this construction).

Abstract Semantic. As usual in abstract interpretation, we represent program properties with abstract domains. An abstract domain is a tuple ⟨D ♯ , γ ♯ , ⊑ ♯ , Whereas conventional reachability analysis is sound when it overapproximates concrete invariants, the sucient precondition analysis is sound when it under-approximates them. For this reason, an abstraction of the concrete semantic of Fig. 3 can not be obtained by simply replacing the concrete operators with the abstract ones (as typically done in abstract interpretation), instead they must be replaced with a new special set of abstract operators that guarantee an under-approximation of the concrete computation. In particular, we need operators ⊔ ♯ , ⊓ ♯ , that under-approximate respectively ∪, ∩, a lower widening 2 ∇ ♯ and ← τ ♯ [[s]] that under-approximates ← τ [[s]] for atomic statements.

⊔ ♯ , ⊓ ♯ , ∇ ♯ , τ ♯ [[s]]⟩ where γ ♯ : D ♯ → P(E) is a monotonic map, ⊑ ♯ : D ♯ × D ♯ is a partial order relation, ⊔ ♯ , ⊓ ♯ ,
As an example, in [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] it is shown how to design such operators for the polyhedra domain, with the exception of ⊔ ♯ . However a simple, yet imprecise, denition for ⊔ ♯ is to just return one of its arguments. A more precise operator will be presented in Sect. 3, exploiting the powerset domain. Consequently, a sound abstraction of the backward semantic can be obtained by leveraging the underapproximated versions of domain operators.

Additionally, even though the concrete backward semantics depends solely on the post-condition, to design an abstract transfer function, it can be useful to have an over-approximation of the precondition (e.g., to linearize arithmetic expressions as in [START_REF] Miné | Symbolic methods to enhance the precision of numerical abstract domains[END_REF]). Fortunately this over-approximation can be easily computed (through a traditional forward reachability analysis) and stored for later usage in the backward pass. Hence, for the rest of this paper, we will assume the availability of an over-approximation of the result of each backward operator.

Correctness and Incorrectness. Program specications can be modeled in the language with assert(b) statements. Their semantic changes depending on the goal of the analysis, whether it is for preconditions for program correctness or incorrectness. We can see this with an example.

Example 2. Consider the programs of Figs. 4a,4b,4c. Program 4a contains no assertion, thus it is trivially always correct (and never incorrect). In Program 4b, to compute a sucient precondition for correctness we collect x ≥ 50 from the 2 A lower (or dual) widening

∇ ♯ : D ♯ × D ♯ → D ♯ is a binary operator such that: 1. for all d ♯ 1 , d ♯ 2 ∈ D ♯ , γ ♯ (d ♯ 1 ∇ ♯ d ♯ 2 ) ⊆ γ ♯ (d ♯ 1 ) ∩ γ ♯ (d ♯ 2 ); 2. for any sequence (x ♯ i ) i∈N , the sequence dened as y ♯ 0 ≜ x ♯ 0 and y ♯ i+1 ≜ y ♯ i ∇ ♯ x ♯ i+1
becomes stable in a nite number of iterations.

User Input

A crucial aspect of programming is I/O. The language we studied has a limited support for I/O in the form of input arguments and return values, but this is often not enough as real-world programs can perform I/O operations at arbitrary execution points. In particular, as we focus on nding preconditions, we are mostly interested in the eect of user input.

To address this issue, a new statement, v := input(), is added to the language. When this statement is executed, the machine reads a value from an external source and stores it in v. As dierent input statements may read from dierent sources, we assume that nitely many sources are available, each identied with an index, and annotate each input statement with the index identifying the source, e.g., v := input n () for an input from the nth source.

Remark 1 (Input versus non-determinism). It might appear that the following two programs

x := input 1 ()

x := [-∞, +∞] assert(x > 100) assert(x > 100)
have the same semantics, but this is not the case: intuitively, input 1 () diers from the non-deterministic interval [-∞, +∞] in that the former depicts an user-controllable, input to the program, while the latter depicts an internal uncontrollable form of input. Consequently, the (correctness) precondition for the rst program involves not only the value of x but also the value returned by input 1 (). Vice versa, the one of the second program only concerns the value of x. In the rst case, the precondition is: input 1 > 100. Indeed, if this condition holds the program satises the assertion. In the second one, the precondition is ∅. Indeed, there is no set of stores that for any non-deterministic execution ensures that the assertion is satised.

⊓ ⊔

Concrete Semantic In order to model user input, our representation of states as program stores is not sucient anymore. Inspired by the input representation proposed in [START_REF] Delmas | Analysis of software patches using numerical abstract interpretation[END_REF], we model external inputs as streams, i.e., pairs of an innite sequence of integers and an index, where the index is used to store the position of the next number to be read from the sequence. The set of streams is denoted with S ≜ Z ω × N and get(s) indicates the current value of the stream s. We further assume that p dierent input sources are available, modeled as multi-streams, i.e., vectors of p streams, denoted with M ≜ S p . Therefore program states are modeled as pairs of a store (environment) and a multi-stream, E ′ ≜ E × M.

We further denote with incr n (m) the multi-stream m in which the nth stream is equal to m n but with its index incremented and the other streams left unchanged.

For non-input statements, the semantic τ [[s]] : P(E ′ ) → P(E ′ ) operates on the store as before, while leaving the streams untouched, e.g.,

τ [[v := a]]P ≜ {(ρ[v → x], m) | (ρ, m) ∈ P, x ∈ E[[a]]ρ}.
On the contrary, the semantic of v := input n () stores in v the current value of the nth stream and increments its index: Abstraction. Input streams can be abstracted in several dierent ways, e.g., by retaining a nite prex, or with an automaton, etc. In this work, we consider an abstraction that classies streams as either time-invariant (e.g., (111..., 0) ∈ S) or time-dependent (e.g, (123..., 0) ∈ S). The set of time-invariant streams is denoted with S i and the set of time-dependent streams with S t . In this abstraction, in the former case we track the value that is repeated in the stream, while in the latter all the information is discarded. In both cases the information regarding the current position on the stream (the index) is not preserved.

τ [[v := input n ()]]P ≜ {(ρ[v → get(m n )], incr n (m)) | (ρ, m) ∈ P }.

Time-invariant Stream Abstraction

Example 3. Consider the following example.

i, j := 0 for x = 1 to 10 do

i := i + input 1 () j := j + input 2 ()
end for

assert(i = j)

⊓ ⊔

To formalize this abstraction we use a partial map from p stream variables to Z. We denote the nth stream variable with v s n and with V s the set of stream variables. If v s n is dened in the map, then the corresponding stream is time-invariant with value matching the variable's value, otherwise it is time-dependent. More formally:

Denition 1 (Time-invariant stream abstraction). Let E ′ be a set of states. We dene E ′ ≜ (V ∪ V s ) ⇀ Z, the concretization γ : P( E ′ ) → P(E ′ ) and abstraction α : P(E ′ ) → P( E ′ ) functions as follows:

γ(R) ≜ {(ρ, m) | ∃ ρ ∈ R. ρ(v k ) V = ρ(v k ) V , matchStream( ρ, m)} α(R) ≜ { ρ | ∃(ρ, m) ∈ R. ρ(v k ) V = ρ(v k ) V , matchStream( ρ, m)}
where:

matchStream( ρ, m) ⇔ ∀n = 1, .., p. ρ(v s n ) = get(m n ) if m n ∈ S i undef if m n ∈ S t ⊓ ⊔
Theorem 1. The following Galois Connection holds:

(P(E ′ ), ⊆) ---→ ← --- α γ (P( E ′ ), ⊆).
Proof. See Appendix A.

Semantic. The semantic of statements dierent from v := input n () coincides with the concrete one as those statements only operate on the store part of the state (not on the streams), and that part is not abstracted; for example

τ [[v := a]]P ≜ { ρ[v → x] | ρ ∈ P, x ∈ E[[a]] ρ V }.
On the other hand, τ [[v := input n ()]] aects the stream. In particular, if the stream is time-invariant (thus v s n is dened in ρ) then τ [[v := input n ()]] copies v s n (which is equal to the stream's value) to v. Otherwise, if the stream is timedependent, v gets [-∞, +∞] as no information is retained in the abstraction and [-∞, +∞] is always a sound choice. More formally:

τ [[v := input n ()]]P ≜ { ρ[v → x] | ρ ∈ P, x ∈ Z. (v s n ∈ dom( ρ) ⇒ x = ρ(v s n ))}.
As in the forward semantic, the backward semantic of non-input statements can be easily derived from the concrete semantic; for example

← τ [[v := a]]S = { ρ | ∀x ∈ E[[a]] ρ. ρ[v → x] ∈ S}.
The backward semantic of input statements ensures that if the stream is timedependent (v s n undened) then for all substitutions of v in ρ the resulting store is in the post-condition. Otherwise if the stream is time-independent, then ρ[v → ρ(v s n )] must be in the post-condition. More formally we have:

← τ [[v := input n ()]]S = { ρ | ∀x ∈ Z. (v s n / ∈ dom( ρ) ∧ ρ[v → x] ∈ S) ∨ (v s n ∈ dom( ρ) ∧ (x = ρ(v s n ) ⇔ ρ[v → x] ∈ S))}
Theorem 2. The semantic of statements, both forward and backward, is sound:

τ [[s]] γ(R) ⊆ γ( τ [[s]]R) γ( ← τ [[s]]S) ⊆ ← τ [[s]] γ(S).
Proof. See Appendix A.

Abstract Semantic In the previous section, we demonstrated an abstraction of input streams into environments where some variables can be dened (timeinvariant streams) or not (time-dependent streams). The usual numeric domains can not be used directly as they assume that all variables are dened. This issue was already studied in the context of abstracting heterogeneous environments (i.e., environments where some variables are optional). One simple approach is to partition the environments according to the dened variables, but this scales poorly as there can be an exponential number of partitions in the worst case.

We adopt instead the method proposed in [START_REF] Journault | An abstract domain for trees with numeric relations[END_REF], though in a simplied version.

This approach lifts a numeric domain D ♯ , to a domain D ♯ consisting of pairs ⟨d ♯ , l⟩, where V ⊆ l ⊆ V ∪V s and d ♯ ∈ D ♯ . The element d ♯ is dened on V ∪V s and the concretization of ⟨d ♯ , l⟩ yields states with domain subsuming l and satisfying the constraints of d ♯ . In the original approach [START_REF] Journault | An abstract domain for trees with numeric relations[END_REF], the elements of D ♯ contained an additional set u ⊇ l representing an upper bound for the domain of the states (here u = V ∪ V s ), but in our case this additional exibility is not needed since stream variables can not be added or removed explicitly (e.g., with ad-hoc statements) but they can only be added as a side-eect of input statements, hence only the lower bound can vary.

More formally the concretization is dened as γ ♯ (⟨d

♯ , l⟩) ≜ { ρ | ∃ ρ ′ ∈ γ ♯ (d ♯ ), V ⊆ l ⊆ dom( ρ) ⊆ V ∪ V s , ρ = ρ ′ dom( ρ) }.
Details on the construction of over-approximation domain operators can be found in [START_REF] Journault | An abstract domain for trees with numeric relations[END_REF]. Here instead we focus on under-approximation operators. If ⊓ ♯ , ⊔ ♯ , ∇ ♯ are under-approximation operators for the base domain D ♯ , then they can be lifted to D ♯ : Semantic. The semantic of input statements can be handled as follows:

Join: ⟨d ♯ 1 , l 1 ⟩ ⊔ ♯ ⟨d ♯ 2 , l 2 ⟩ ≜ ⟨d ♯ 1 ⊔ ♯ d ♯ 2 , l 1 ∪ l 2 ⟩; Meet: ⟨d ♯ 1 , l 1 ⟩ ⊓ ♯ ⟨d ♯ 2 , l 2 ⟩ ≜ ⟨d ♯ 1 ⊓ ♯ d ♯ 2 , l 1 ∪ l 2 ⟩; Widening: ⟨d ♯ 1 , l 1 ⟩ ∇ ♯ ⟨d ♯ 2 , l 2 ⟩ ≜ ⟨d ♯ 1 ∇ ♯ d ♯ 2 , l 1 ⟩ if l 2 ⊆ l 1 ⟨d ♯ 1 ⊓ ♯ d ♯ 2 , l 2 ⟩ if l 1 ⊂ l 2 . Proposition 1. ⊔ ♯ , ⊓ ♯ are
τ ♯ [[v := input n ()]]⟨D ♯ , l⟩ ≜ ⟨τ ♯ [[v := [-∞, ∞]]]D ♯ , l⟩ if v s n / ∈ l ⟨τ ♯ [[v := v s n ]]D ♯ , l⟩ if v s n ∈ l Indeed, if v s n /
∈ l then the concretization contains both time-invariant and timedependent streams: for the latter no information is stored, thus v gets ⊤. If instead v s n ∈ l then the concretization contains only time-invariant streams and thus the assignment copies the value from the stream variable.

The backward semantic is computed as:

← τ ♯ [[v := input n ()]]⟨D ♯ , l⟩ ≜ ⟨D ♯ , l⟩ if v s n / ∈ l ∧ ← τ ♯ [[v := [-∞, ∞]]]D ♯ = D ♯ ⟨ ← τ ♯ [[v := v s n ]]D ♯ , l ∪ {v s n }⟩
otherwise Indeed, we can distinguish three cases:

D ♯ unmodied, for all states ρ ∈ γ ♯ (D ♯ ) and x ∈ Z, ρ[v → x] ∈ γ ♯ (D ♯ ).
Therefore the backward precondition is simply ⟨D ♯ , l⟩. Notice that the condition on the backward projection is crucial to ensure the soundness of timedependent streams: the projection over-approximates any assignment, thus

[38, Theorem 2.6] ensures that ρ[v → x] ∈ γ ♯ (D ♯ ). 3. If v s n / ∈ l and ← τ ♯ [[v := [-∞, ∞]]]D ♯ ̸ = D ♯
then, as before, we have both timeinvariant and time-dependent streams, but, unlike the previous case, there

exist ρ ∈ γ ♯ (D ♯ ) and x ∈ Z such that ρ[v → x] / ∈ γ ♯ (D ♯ ). Consequently,
time-dependent streams can not be included in the precondition as they would be unsound. For this reason the precondition adds v s n to l (thus underapproximating the precondition) and transforms D ♯ as in the rst case. Theorem 3. The abstract semantic is sound, i.e., for any s ∈ While and d ♯ ∈ D ♯ the following holds:

τ [[s]] γ ♯ ( d ♯ ) ⊆ γ ♯ ( τ ♯ [[s]] d ♯ ) ← τ [[s]] γ ♯ ( d ♯ ) ⊇ γ ♯ ( ← τ ♯ [[s]] d ♯ )
Proof. See Appendix A.

Integer Wrapping

In this section, we generalize our framework to support xed precision integers (i.e., with wrap-around), typically found in C-like languages. This is important as some analyzers detect integer overows but do not handle wrap-around: they either stop the analysis for the traces that overow (which is not sound for programs that do wrap-around on purpose) or put the variable to the full range of their type (which is sound but imprecise). For the sake of brevity, we limit our presentation to unsigned 8-bit integers, but it is easy to generalize this framework to other types.

Arithmetic and boolean semantics are replaced with versions that operate with 8-bit unsigned integers, e.g., E[[x + 10]]{x → 250} = {[x → 4]}. To do so, it suces to replace the usual arithmetic operators with versions that take care of integer wrapping. Unfortunately this requires new wrap aware operators to be designed. To avoid this diculty, we prefer a modular approach in which rstly the result is computed with innite precision operators (i.e., the usual unwrapped ones), and then it is wrapped with a wrapping operator.

Denition 2 (Wrapping operator). Dene wrap : Z → [0, 255] as wrap(z) ≜ z mod 256, where mod computes the Euclidean remainder.

⊓ ⊔

Consequently, the abstract semantic must take into account wrapping of integers. Several approaches have been proposed in the literature to handle this problem [START_REF] Sen | Executable analysis using abstract interpretation with circular linear progressions[END_REF][START_REF] Gotlieb | Constraint solving on modular integers[END_REF][START_REF] Gange | Interval analysis and machine arithmetic: Why signedness ignorance is bliss[END_REF][START_REF] Simon | Taming the wrapping of integer arithmetic[END_REF].

Case Study: Polyhedra Domain As an example, we show how to instantiate the abstract semantic to the case of the polyhedra domain. Our work is based on the work of Simon et al. [START_REF] Simon | Taming the wrapping of integer arithmetic[END_REF]: they demonstrate how to design sound abstract operators for the polyhedra domain that take into account integer wrapping. For this purpose, they presented an algorithm for computing a wrap ♯ operator. It takes in input a polyhedron P , a variable v to wrap, and as result it produces a new polyhedron P ′ in which v lies in [0, 255]. Fig. 5 shows an example of the computation of wrap ♯ . We extend their work (which only tackles over-approximation forward operators) to handle under-approximation backward operators. Intuitively, the backward version of wrap ♯ for a polyhedron P (along a variables v) should compute a polyhedral representation of the points that, after wrapping, end up in P . This boils down to replicating P innitely many times, where each copy is translated by a integer multiple of 256 along v, i.e., the sequence {P + 256ke v } k∈Z . Fig. 6 shows an example of this computation.

Although all the polyhedra of the sequence above are valid unwrappings, not necessarily all of them represent reachable states. In particular, if pre is an over-approximation of the input of wrap ♯ , then the valid polyhedra are only the ones intersecting pre. This information can be used to guide the unwrapping of a polyhedron. We present in Algorithm 1 a procedure for computing ← --wrap ♯ . The auxiliary function quadrantIndices(pre, v) computes the indices of the quadrants spanned by v in pre (see [START_REF] Simon | Taming the wrapping of integer arithmetic[END_REF]Algorithm 1]). Notice that the polyhedra of the left is split in two parts: one that does not need wrapping (x ∈ [0, 255]) and another that does (x ∈ [256, 511]). To compute the result (green polyhedron), the rst part is joined with the translation of the second one by -256 (along x).

the sequence are merged together with an under-approximating join, but this can incur a loss of precision if the polyhedra are separated (as in Fig. 6) since in this case the set union is not convex, and thus to under-approximate it with a polyhedral shape, only one polyhedron can be retained (hence in Fig. 6, the result must be either one of the polyhedra in green or the one in blue). A robust solution to this kind of imprecisions will be addressed in the next section.

Additionally, the meet with pre in the algorithm excludes the polyhedra that are surely not reachable, thus increasing the odds of retaining an appropriate polyhedron.

Powerset Domain

As noted in [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF], designing an under-approximating join for polyhedra can be challenging. This problem was sidestepped by designing such an operator only in some specic cases, namely on joins occurring in the analysis of backward lters of if-then-else statements and while loops. This simplies the design as only under-approximations of the join of an arbitrary polyhedron with a halfspace are handled. This is carried out using special heuristics, tailored to handle many practical cases. Unfortunately, they are not robust and may cause losses of precision in other cases. This is especially true for our semantic, as, unlike the one in [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF], we use ⊔ ♯ to handle arbitrary joins (e.g., in ← --- wrap and later in this section for widenings).

Furthermore, even if a perfect join heuristic could be designed, the polyhedra domain would still not be precise if the concrete union is non-convex. This can often occur in real world programs (e.g., in the unwrapping of the polyhedron of Fig. 6).

Under-approximated Powerset

A robust approach to addressing this issue is to leverage the powerset [START_REF] Filé | The powerset operator on abstract interpretations[END_REF] construction: in this construction, a base domain D ♯ is lifted to a nite set of Algorithm 1 Calculate ← --- wrap ♯ (P, v, t, pre)

Require: Parameter m > 0: maximum number of copies. q l , qu ← quadrantIndices(pre, v, t) abstract elements P f inite (D ♯ ). The concretization of a set yields the union of the concretizations of all its elements. Notably, the join operator becomes exact, and thus it is a sound under-approximation of ∪. Consequently the underapproximation join ⊔ ♯ p can coincide with the over-approximating one ⊔ ♯ p .

if q l = -∞ ∧ qu = +∞ then return P else if q l = -∞ then q l ← qu -m else if qu = +∞ then qu ← q l + m else {Retain at most m copies} qu ← q l + min(qu -q l , m) end if Q ← ⊥ ♯ for k ← q l to qu -1 do Q ← Q ⊔ ♯ ((τ ♯ [[v := v -256k]]P ) ⊓ ♯ pre)
Denition 3 (Powerset domain). Let D ♯ be an abstract domain. We let P (D ♯ ) ≜ P f inite (D ♯ ) be its powerset lifting. P (D ♯ ) is partially ordered by

S ♯ 1 ⊑ ♯ p S ♯ 2 ⇔ ∀d ♯ 1 ∈ S ♯ 1 . ∃d ♯ 2 ∈ S ♯ 2 . d ♯ 1 ⊑ ♯ d ♯ 2 .
Moreover, join and meet are respectively dened as

S ♯ 1 ⊔ ♯ p S ♯ 2 ≜ S ♯ 1 ∪ S ♯ 2 and S ♯ 1 ⊓ ♯ p S ♯ 2 ≜ {d ♯ 1 ⊓ ♯ d ♯ 2 | d ♯ 1 ∈ S ♯ 1 , d ♯ 2 ∈ S ♯ 2 }. ⊓ ⊔
Additionally, if the base meet is exact (which is the case in many numeric domains, including polyhedra), also ⊓ ♯ p is, thus it is a sound under-approximating operator as well.

Widening. A trivial widening can be obtained by joining all elements of the powerset (for each argument) and then applying the base widening (hence the result is a singleton). Likewise to get a trivial lower widening, it is possible to apply the base lower widening on just one element of each argument and discard all the others. Unfortunately, these operators are quite imprecise, as shown in the following example. Example 4. Consider the following example suggested by Gopan and Reps [START_REF] Gopan | Lookahead widening[END_REF].

i, j := 0

for i := 1 to 100 do if i ≤ 50 then j ← j + 1 else j ← j -1
end for

The while loop presents two phases: one in which j is incremented (then branch),

and one in which it is decremented (else branch). This induces a non-convex loop invariant, that requires at least two polyhedra to be represented precisely.

It is clear that the trivial widenings can not nd such a result as they yield a singleton.

⊓ ⊔

A simple, yet useful, improvement consists in retaining stable elements, i.e., elements that are shared in both arguments, and widen only the remaining (unstable) elements. More formally: Denition 4 (Improved Powerset Widening). Let S ♯

1 = ⟨d ♯ 1,1 , .., d ♯ 1,n ⟩ and S ♯ 2 = ⟨d ♯ 2,1 , .., d ♯
2,m ⟩. Dene:

S ♯ 1 ∇ ♯ p S ♯ 2 ≜ ⟨d ♯ 1 ∇ ♯ (⊔ ♯ S ♯ u2 )⟩ ∪ (S ♯ s \ {d ♯ 1 }) if S ♯ u1 = ∅ ∧ S ♯ u2 ̸ = ∅ ∧ d ♯ 1 ∈ S ♯ 1 ⟨(⊔ ♯ S ♯ u1 ) ∇ ♯ (⊔ ♯ S ♯ u2 )⟩ ∪ S ♯ s otherwise S ♯ 1 ∇ ♯ p S ♯ 2 ≜ S ♯ s if S ♯ u1 = ∅ ∨ S ♯ u2 = ∅ ⟨d ♯ u1 ∇ ♯ d ♯ u2 ⟩ ∪ S ♯ s if d ♯ u1 ∈ S ♯ u1 ∧ d ♯ u2 ∈ S ♯ u2 where S ♯ s ≜ S ♯ 1 ∩ S ♯ 2 is the set of stable elements, S ♯ u1 ≜ S ♯ 1 \ S ♯ s the set of unstable elements of S ♯ 1 and S ♯ u2 ≜ S ♯ 2 \ S ♯ s the set of unstable elements of S ♯ 2 . ⊓ ⊔ Proposition 2. ∇ ♯ p (∇ ♯ p ) is
: d ♯ 1 , d ♯ 2 polyhedra in constraint representation. Ensure: d ♯ renes d ♯ 1 with d ♯ 2 . d ♯ ← d ♯ 1 for c matching a • v ≥ b in d ♯ 1 do d ♯ 1,nc ← d ♯ 1 \ {c} v1, r1 ← sat(d ♯ 1 , c) {sat(d ♯ , c
) returns the vertices and rays of

d ♯ saturating c} c ′ ← a • v ≥ b -1 v2, r2 ← sat(d ♯ 2 , c ′ ) d ♯ m ← gen(v1 ∪ v2, r1 ∩ r2) {gen(v, r) returns the polyhedron generated by vertices v and rays r} if c ′ ∈ d ♯ m then d ♯ m,nc ′ ← d ♯ m \ {c ′ } d ♯ i ← d ♯ 1,nc ∩ d ♯ m,nc ′ ∩ d ♯ 2 else d ♯ i ← d ♯ 1,nc ∩ d ♯ m ∩ d ♯ 2 end if d ♯ h ← d ♯ 1 ⊔ ♯ d ♯ i {rays(•) computes the set of rays of a polyhedron} if rays(d ♯ 1 ) ⊆ rays(d ♯ h ) then d ♯ ← d ♯ h break end if end for point-wise, is {∅} as both ← τ [[s]]b 1 = ∅ and ← τ [[s]]b 2 = ∅.
But the set of states represented by S, that is ∪ b∈S b, does admit a non-empty precondition since

← τ [[s]] ∪ b∈S b = [x → [0, 4], y → 0] ̸ = ∅
. This is possible as the backward semantic (unlike the forward one) is not a ∪-morphism, but instead only the inclusion holds, i.e., i

← τ [[s]]S i ⊆ ← τ [[s]
] i S i for any family of states {S i } i∈N (whereas the equality holds for ∪-morphisms).

However, the powerset

S ′ ≜ {b ′ 1 , b ′ 2 } admits a non-empty backward semantic as { ← τ [[s]]b ′ 1 , ← τ [[s]]b ′ 2 } = {[x → [0, 4], y → 0],
∅}, even if S ′ represents the same states as S (the only dierence is the internal composition of the powerset).

For this reason the elements of the powerset domain should be kept as large as possible, so that

← τ ♯ [[s]
] is maximized (notice that in the forward analysis setting, we strive for the opposite goal, namely keeping the elements as small as possible).

In particular, we can allow some sharing of states among elements of the set, provided that this does not aect the overall concretization of the powerset.

For this purpose we use a renement operator: an under-approximation join

⊔ ♯ is a renement operator if d ♯ ≜ d ♯ 1 ⊔ ♯ d ♯ 2 ⊒ ♯ d ♯ 1 , meaning that d ♯ renes d ♯ 1 with states from d ♯ 2 .
Then, we can rene a powerset by replacing each element with its renement with all the other elements. Additionally, renements can help mitigate the computational cost of the powerset as, after renement, some elements may become redundant and thus can be removed.

Algorithm 3 Integer polyhedral renement: adjacent singleton variables

Require:

d ♯ 1 , d ♯ 2 polyhedra in constraint representation. Ensure: d ♯ renes d ♯ 1 with d ♯ 2 . d ♯ ← d ♯ 1 for c matching v = n in d ♯ 1 do if v = n + 1 ∈ d ♯ 2 ∨ v = n -1 ∈ d ♯ 2 then {rays(•) computes the set of rays of a polyhedron} if rays(d ♯ 1 ) = rays(d ♯ 2 ) then d ♯ ← d ♯ 1 ⊔ ♯ d ♯ 2 break end if end if end for

Case Study: Polyhedra Renement

To design a renement operator, it is possible to leverage a procedure for checking if the over-approximation join is exact. Indeed, an exact join is also a valid renement. For the polyhedra domain, this problem has been studied by Bemporad et al. [START_REF] Bemporad | Convexity recognition of the union of polyhedra[END_REF] and Bagnara et al. [START_REF] Bagnara | Exact join detection for convex polyhedra and other numerical abstractions[END_REF], but they focus on polyhedra representing real-valued environments.

On the other hand, if variables are of integer type (as in our semantic), the join can be exact even if the union of the polyhedra is not convex. For example the union of the polyhedra (in constraint representation)

d ♯ 1 ≜ {0 ≤ x ≤ 1} and d ♯ 2 ≜ {2 ≤ x ≤ 3} is not a convex set, but still the join is exact: γ(d ♯ 1 ) ∪ γ(d ♯ 2 ) = {0, 1, 2, 3} = γ(d ♯ 1 ⊔ ♯ d ♯ 2 ).
3 Since this kind of polyhedra appears frequently in practice (e.g., in loops incrementing variables by one unit), we propose two renement algorithms tailored for these cases.

Consider the bi-dimensional polyhedra d ♯ 1 ≜ {x ≥ 0, y ≥ 0, x + y ≤ 4} and d ♯ 2 ≜ {x ≤ 3, y ≤ 3, x + y ≥ 5}.
It is easy to check that there exists a part of d ♯ 2 that can be exactly joined with d ♯ 1 (the triangle with vertices (2, 3), (3, 2), ( 83 , 8 3 )), and thus can rene d ♯ 1 . This is the case as the strip 4 < x + y < 5 separating it from d ♯ 1 does not contain any integer. Algorithm 2 tackles this case by scanning for constraints of this kind and if they are found, computes parts of the second argument that can rene the rst. Algorithm 3 scans for a variable in d ♯ 1 and d ♯ 2 that is xed in the two polyhedra to constants diering by one unit. If such a variable is found, then the join between the two polyhedra is exact. As an example, let

d ♯ 1 ≜ {x = 0, 0 ≤ y ≤ 2} and d ♯ 2 ≜ {x = 1, 4 ≤ y ≤ 6}.
Since the strip 0 < x < 1 does not contain any integer, the join is exact. 3 With an abuse of notation, we confuse {x} → Z with Z.

Implementation and Experiments

In addition to the theoretical foundations, the contribution [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF] included a PoC static analyzer, Banal [START_REF]The banal static analyzer prototype[END_REF]. This analyzer targets a toy language with a semantic not compatible with the one of C (e.g., it assumes mathematical integers instead of machine integers). We extended it with the features presented in this work:

an implementation of a subset of the C semantic and a frontend for a signicant subset of the language, user input (Sect. 2.3), machine integers (Sect. 2.4), a powerset domain (Sect. 3) and improved operators. As a consequence, our new prototype is able to analyze benchmarks from the SV-COMP competition. As our work focuses on incorrectness, we report only the results of the analysis of incorrect programs.

Witnesses Generation. To analyze SV-COMP benchmarks, Banal translates each call site to __VERIFIER_nondet_int() with an input statement (each with a distinct stream). Consequently, it computes preconditions in the form of an abstract element relating the input variables. Then, as all states in the abstract element are valid sucient preconditions for the violation of some assertion, we extract one concrete vector of values. Notice that for the purpose of SV-COMP, the quality of a violation witness [START_REF] Beyer | Witness validation and stepwise testication across software veriers[END_REF] is measured by how much it restricts the state-space exploration. The more restricted it is, the less states the validator has to explore in order to check the witness. By picking a concrete vector (which represents only one execution path) we obtain the most precise kind of witness.

Furthermore, as previously discussed, the preconditions generated by our analysis may simply lead to an innite loop, rather than a true bug. To rule out this possibility Banal replaces each input call site with its concrete value, compiles the benchmark and runs it with a time limit (2s). If an assertion fails, then the counter-example is conrmed.

Finally, a witness is generated in SV-COMP's graphml format: we make a control ow automaton resembling the control ow graph of the benchmark and specify for each input site the corresponding concrete value. Moreover, to certify the correctness of our result using independent techniques, we validate the witness with the CPA-W2T [START_REF] Beyer | Tests from witnesses: Execution-based validation of verication results[END_REF] validator (which is specically tailored for checking concrete witnesses) and declare the benchmark to be successfully analyzed only if successfully validated.

Experimental Evaluation. To asses the performance of our analysis, we run our tool and three leading tools from SV-COMP23: CPAChecker [START_REF] Beyer | Cpachecker: A tool for congurable software verication[END_REF][START_REF] Dangl | Cpachecker with support for recursive programs and oating-point arithmetic: (competition contribution)[END_REF], UAutomizer [START_REF] Heizmann | Software model checking for people who love automata[END_REF] and Veriabs [START_REF] Afzal | Veriabs: Verication by abstraction and test generation[END_REF][START_REF] Darke | Veriabs: A tool for scalable verication by abstraction (competition contribution)[END_REF] All tests were conducted on an Intel Core i7-8550U CPU with 3GiB memory limit and 300 seconds time limit using the BenchExec [START_REF] Beyer | Reliable benchmarking: requirements and solutions[END_REF] platform. We report the results in Table 1, where unknown indicates an inconclusive result and unsupported indicates a failure due to missing support for some C features (e.g., arrays, pointers).

Despite some encouraging results, Banal performs worse than the other tools due to several imprecisions (e.g, widening failure, non-linear arithmetic) in the analysis and missing support for several C features. However, since it is based on abstract interpretation, Banal is faster than the other tools. In particular, on the successfully analyzed tasks Banal is 22x faster than CPAChecker, 50x than UAutomizer and 50x than Veriabs. This performance gap becomes even wider if we consider programs where bugs are reached after many loop iterators (so necessitate loop unrolling and thus are limited to bugs reachable in few loop iterations (so called shallow bugs). To assess this, we selected some benchmarks from the previous set and re-run the analysis xing the number of loop iterations with dierent values. The results are reported in Table 2. CPAChecker and UAutomizer hit timeouts when loops require > 1000 unrollings, while Banal's execution time is not aected. In all cases (including shallow bugs, e.g., < 10 iterations) we observe that Banal is much faster than the other tools. Interestingly, also Veriabs can scale thanks to loop summarization [START_REF] Xie | Proteus: Computing disjunctive loop summary via path dependency analysis[END_REF] techniques allowing it to replace loops with expressions summarizing their eect. However these techniques only work with special loop structures. To exhibit this, we added two synthetic benchmarks simple_nested and assert_loop (see Fig 8a,8b) for which the summarization fails (thus forcing Veriabs to unroll the loop) but Banal succeeds.

Conclusion

In this article, we built on top of the preliminary work of [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sucient program conditions[END_REF], studying how to improve it to construct a more eective analysis. It supports more varied and realistic semantics (such as wrap-around) as well as classic abstract domain constructions (such as powerset domains, improved widenings, etc.), to the point where it can provide encouraging results on realistic analysis problems. Our implementation targeted C programs, but the semantics are agnostic with respect to the language and can used to analyze any language with machine integers data types.

Future work. Although this work displays promising results, much work is still needed to analyze real-world programs. Firstly, we believe that more precise abstractions are needed to analyze numeric properties (e.g., domains for constants, congruences, bit-wise operations). The semantic should be extended to handle more features of the C language (e.g., memory allocation, arrays, structs). We do support non-linear integer arithmetic, thus adding support for oating point arithmetic should not be a too large eort. Moreover, we proposed an abstraction modeling streams as returning always the same value: this may suce in loop-free programs (as each stream is read only once), but can be imprecise in other cases. Whereas the polyhedra domain (and even its power-set) is precise, it comes with a signicant computational cost. We believe that more lightweight domains (like intervals [START_REF] Cousot | Abstract interpretation: a unied lattice model for static analysis of programs by construction or approximation of xpoints[END_REF] or octagons [START_REF] Miné | The octagon abstract domain[END_REF]) and packing techniques will play a crucial role in making this analysis more scalable to real world programs.

the limit l = |Y n |. Crucially, after n steps, since the size of the set must remain constant, either all elements are stable or both S ♯ u1 and S ♯ u2 contain one element, as otherwise the size would decrease.

For i ≥ n, we can link each element of Y i with an element of Y i+1 . In particular, we construct l sequences {Z r i } i≥n (indexed by r), so that i ≥ n, Y i = {Z 1 i , .., Z l i }. The base case is Z r n ≜ y n,r (where y n,r are elements of Y n ).

For the inductive case we have:

if Y i = Y i+1 , then Z r i+1 ≜ Z r i for all r;
otherwise all elements except one are stable, say the element corresponding to the pth sequence. We dene Z r i+1 ≜ Z r i for r ̸ = p and Z p i+1 ≜ Z p i ∇ ♯ x (where x is the unstable element of X i+1 ).

Consider Z r , obtained by retaining only the elements of Z r from the second case. If Z r is nite (innitely many elements were ltered out) then Z r converges in a nite number of steps. Consider now the remaining m ≤ l sequences that vary innitely many times 4 . They also must converge: indeed we can invoke the convergence property of ∇ ♯ as by construction Z r i+1 ≜ Z r i ∇ ♯ x and this sequence must converge by denition of widening. To conclude, dene k as the maximum of the number of steps required for each sequence to converge. It turns out that

Y k+i = {Z 1 k+i , .., Z l k+i } = {Z 1 k , .., Z l k } = Y k .
The same reasoning can be used to show that ∇ ♯ p is a lower widening. ⊓ ⊔ Remark 2. Before proving the correctness of Algorithms 2, 3 we provide a useful decomposition of the points in the polyhedra join. Let P 1 , P 2 be two closed polyhedra and P ≜ P 1 ⊔ ♯ P 2 . For any z ∈ P we have that

z = i λ i v i + i λ ′ i v ′ i + i µ i r i + i µ ′ i r ′ i , where i λ i + i λ ′ i = 1, {v i } i , {v ′ i } i
are respectively the vertices of P 1 and P 2 and {r i } i , {r ′ i } i are respectively the rays of P 1 and P 2 . Three cases are possible.

1. If λ i = 0, then z is a convex combination of vertices of P 2 plus a nonnegative linear combination of rays from both P 1 and P 2 ; 2. If λ ′ i = 0, then z is a convex combination of vertices of P 1 plus a nonnegative linear combination of rays from both P 1 and P 2 ; 3. Otherwise, let A = i λ i , B = i λ ′ i so that

z = A 1 A i λ i v i + 1 A i µ i r i + B 1 B i λ ′ i v ′ i + 1 B i µ ′ i r ′ i = Ax +
q i • a < 0 q i • a i ≥ 0
where {a i } i represents the other constraints of d ♯ 1 . We consider three cases: ] such that z = x + λ i µ ′ i q i , where x = i λ i v i + i µ i r i + (1 -λ) i µ ′ i q i is in d ♯ 1 and saturates c.

a • z ≥ b) z is in d ♯ 1 as it satises all the constrains of d ♯ 1 • z • a i = i λ i v i • a i + i µ i r i • a i + i µ ′ i q i • a i ≥ b i ; • z • a ≥ b by hypothesis. Since z ∈ d ♯ 1 , then z ∈ d ♯ 1 ∪ d ♯
a • z = i α i a • v 1 i + i β i a • v 2 i + i γ i a • r ′ i = i α i (b) + i β i (b -1) + i γ i (0)
which implies α i = 0, hence z ∈ d ♯ 2 . As in the previous case we conclude

z ∈ d ♯ 1 ∪ d ♯ 2 .
a • z ≤ b -1) Even in this case, we aim to prove that z ∈ d ♯

. Let

A = i λ i v i • a + i µ i r i • a and B = i µ ′ i q i • a. Moreover, by construction A ≥ b and B < 0, but by hypothesis b -1 ≥ a • z = A -B. Therefore, exists α ∈ [0, 1] such that A -αB = b -1. Let z ′ be i λ i v i + i µ i r i + α i µ ′ i q i . By the previous point z ′ ∈ d ♯ 2 . Finally, z = z ′ + (1 -α) i µ ′ i q i , thus ({q i } i are rays of d ♯ 2 ) z ∈ d ♯ 2 .

3) Consider z obtained as a combination of x ∈ d ♯ 1 and y ∈ d ♯ i , that is z = αx + (1 -α)y where α ∈ [0, 1]. We can consider three cases: ⊓ ⊔ Theorem 5. Algorithm 3 computes a renement of the rst argument.

a • z ≥ b) since y ∈ d ♯ 1,nc we that • z • a i = αx • a i + (1 -α)y • a i ≥ b i ; • z • a ≥ b by hypothesis thus z ∈ d ♯ 1 . b -1 ≤ a • z ≤ b) As in 2 a • z ≤ b -1) We have b -1 ≥ a • z = αx • a + (1 -α)y • a, but as x ∈ d ♯ 1 ,
Proof. Assume that the renement succeeded, that is d ♯ is replaced with d ♯

1 ⊔ ♯ d ♯ 2 .
We need to show that the join is exact, i.e., all the points (intersecting the integer ⊓ ⊔

Fig. 2 :

 2 Fig. 2: While language.

Fig. 3 :

 3 Fig. 3: Backward semantic of statements.

  Notice that necessary and sucient preconditions can dier in the presence of non-determinism as demonstrated in the following example. Example 1. Consider the program s ≡ x := x + [-1, 1] with post-condition S ≜ [0, 5] 1 . The strongest necessary precondition is P n = [-1, 6] as for any x ∈ P n there exists a trace leading to the post-condition (∀x ∈ P n . τ [[s]]{x} ∩ S ̸ = ∅). The weakest sucient precondition is P s = [1, 4] as for any x ∈ P s all traces lead to the post-condition (∀x ∈ P n . τ [[s]]{x} ⊆ S). ⊓ ⊔ Let f : P(A) → P(B) be a function, we dene the backward version of f , denoted ← f , as

1 :

 1 x := x + 10 (4a) 1: x := x + 10 2: assert(x ≥ 50) (4b) 1: x := x + 10 2: assert(x ≥ 50) 3: x := x -10 4: assert(x ≤ 50) (4c) assertion and then subtract 10, which yields x ≥ 40 (likewise, for incorrectness we obtain x < 40). In Program 4c the reasoning for correctness is the same as the previous program: we proceed backwards and for each assertion encountered we retain only the states satisfying its guard. This yields x ∈ [40, 50]. On the other hand, to nd preconditions for program incorrectness we have two possibilities: the failure of the assertion at line 2 or 4. For the one at line 2 we proceed as in Program 4b (which yields x < 40). For the one at line 4 we collect x > 50 and proceed backwards. As soon as we encounter the assertion at line 2, we retain the states satisfying its guard (as for correctness), as in order to reach line 4, an execution must satisfy the assertion at line 2. Combining the preconditions yields x / ∈ [40, 50]. ⊓ ⊔ The previous example suggests that our semantics can infer preconditions for both correctness and incorrectness. In the former case the analysis has to start from ⊤ (or some other post-condition of interest) and compute ← τ [[assert(b)]]S as S ∩ [b] where [b] denotes the set of states satisfying b. In the latter it has to start from ⊥ and compute ← τ [[assert(b)]]S as (S ∩ [b]) ∪ [¬b].

1 .

 1 If v s n ∈ l then we only have time-invariant streams in the post-condition. In this case the forward transfer function performs the assignment v := v s n , thus the backward precondition can simply invert this assignment; 2. If v s n / ∈ l and ← τ ♯ [[v := [-∞, ∞]]]D ♯ = D ♯ then we have both time-invariant and time-dependent streams. In addition, as the backward projection leaves

Fig. 5 :

 5 Fig. 5: Wrapping of a polyhedron along the horizontal axis. The polyhedron on

Fig. 6 :

 6 Fig. 6: Unwrapping of x. The unwrapping of the blue polyhedron produces innitely many (here only four are shown) copies of it, separated by the integer's size. The wrapping of each polyhedron in green (depicted with the arrows) coincides with P.

2 Fig. 7 :

 27 Fig. 7: Powerset renement. The blue polyhedron (left gure) can be extended over the green one (right gure) without changing the overall concretization of the powerset.

  an upper (lower) widening operator for P (D ♯ ). Proof. See Appendix A. Renement. Consider the program s computing y := y + [0, 8] and the powerset S ≜ {b 1 , b 2 } of Fig. 7. The backward (concrete) semantic of S, computed Algorithm 2 Integer polyhedral renement: adjacent constraints Require

Fig. 8 :

 8 Fig. 8: Simple programs with deep bugs.

2 .b - 1 ≤

 21 a • z ≤ b) By hypothesis b ∈ Z and a • z is a linear expression of integral variables, thus the only assignments satisfying the inequality yield either b or b -1. If a • z = b we can conclude as in the previous case. Otherwise, exists λ ∈ [0, 1

x 2 and y ∈ d ♯ 2 ,

 22 • a ≥ b, hence exists β ∈ [α, 1] such that βx • a + (1 -β)y • a = b -1. Let z ′ = βx + (1 -β)y. By the previous point z ′ ∈ d ♯ 2 . If β = 0, then a • z = b -1 and we can conclude as in the previous point. Otherwise if β ̸ = 0, x = z ′ -(1-β)y β which implies z = α β z ′ + (1 -α β )y, but as z ′ ∈ d ♯ by convexity z ∈ d ♯ 2 .

lattice) of d ♯ are either in d ♯ 1 or in d ♯ 2 .

 2 Let z ∈ d ♯ . Hence, z must satisfy one of the three cases of Remark 2. Since d ♯ 1 and d ♯ 2 share the same rays, cases 1 and 2 are subsumed by case 3. Therefore we can assume z = αx + (1 -α)y where α ∈ [0, 1]. By construction |v x -v y | = 1,where v x and v y denote the value of the variable v respectively in x and y.Consequently, the value of v in z cat not be an integer unless z = x or z = y, thus proving the result.

  are sound over-approximations of ∪, ∩, ∇ ♯ is a widening operator and τ ♯ [[s]] is a sound over-approximation of τ [[s]] for atomic statements (compound statements are handled by induction on the syntax).

  There are several streams that can render the assertion true, for instance if input 1 () returns 10 at the rst iteration and 0 for other iterations and input 2 () always returns 1. In this case the stream for input 1 () is time-dependent and the one for input 2 () is time-invariant.Notice that the abstraction tracks sets of states, maintaining the value of

both program variables and time-invariant streams, and thus it is able to express relationships between them. For instance, the set of preconditions where both streams are time-invariant, with the same value in [0, 100]. It can also infer relations between stream values and programs variables.

  sound under-approximations of ∪, ∩ and ∇

	♯ is a
	lower widening.
	Proof. See Appendix A.

Table 2 :

 2 10 2 10 3 10 4 10 5 10 6 Analysis time for increasing number of loop iterations, for some selected benchmarks. ✗ denotes a timeout.

							on a selected subset of the competition's bench-
	marks.	In	particular,	we	built	our	set	of	benchmarks	from	the
	ReachSafety-Loops set of the competition, as it comprises several simple numer-
	ical	programs,	from	which	we	removed		the	nla-digbench and
	nla-digbench-scaling folders as they contain programs with polynomial in-
	variants that require special analysis techniques that are out of scope of this
	work. Our set of benchmarks contains 63 C les (35172 LOC) corresponding to
	61% (in terms of LOC) of the ReachSafety-Loops set.

  By, where x ∈ P 1 and y ∈ P 2 . Since A + B = 1, z ∈ [x, y]. ⊓ ⊔ Theorem 4. Algorithm 2 computes a renement of the rst argument.Proof. Assume that the renement succeeded, that is d ♯ is replaced with d ♯ h .Such value is obtained by joining d ♯ i with d ♯ 1 . To prove our result we need to show that the join is exact, i.e., all the points (intersecting the integer lattice)of d ♯ are either in d ♯ 1 or in d ♯ 2 (as d ♯ i ⊆ d ♯ 2 ).Let z ∈ d ♯ . z must satisfy one of the three cases of Remark 2. Case 3 subsumes case 1 as, by construction, the rays of d ♯ 1 are also in d ♯2 . Therefore, we only need to handle cases 2 and 3.2)Consider z obtained as a combination of vertices of d ♯ 1 and rays both in d ♯ where {v i } i are vertices of d ♯ 1 , {r i } i are rays of d ♯ 1 and {q i } are rays exclusively of d ♯ i (or that can not be obtained by a combination of rays of d ♯ 1 ). Since {q i } i are rays of d ♯ i they are also of d ♯ 1,nc , thus they must violate c, but satisfy all the other constraints of d ♯

	and d ♯ i :	1
	z =
	1 :

i λ i v i + i µ i r i + i µ ′ i q i

  Therefore, x ∈ d ♯ m and consequently z ∈ d ♯ m . For this reason there existα i , β i , γ i such that z = i α i v 1 i + i β i v 2 i + i γ i r ′ i where i α i + β i = 1, {v 1 i } i are vertices of d ♯ 1 saturating c, {v 2 i } i are vertices of d ♯ 2 saturatingc ′ , and {r i } i are rays of both d ♯ 1 and d ♯ 2 saturating c.

	Consequently:

m will turn out to be 0.

Acknowledgments This work was supported by the SECURVAL project. The SECUREVAL project was funded by the France 2030 government investment plan managed by the French National Research Agency, under the reference ANR-22-PECY-0005.

Data Availability Statement

All the software used for the experimental part of this work was released in an artifact [START_REF] Marco | Artifact of paper: "Generation of Violation Witnesses by Under-Approximating Abstract Interpretation[END_REF]. It includes not only the source code of the Banal static analyzer, but also the benchmarks and scripts used to produce the Tables 1,2.

A Proofs Theorem 1. The following Galois Connection holds:

Proof. It is easy to check that γ(•) and α(•) are monotonic. Then, we need to show that γ • α is extensive, i.e., R ⊆ γ( α(R)). Assume that (ρ, m) ∈ R. By construction, there exists ρ ∈ α(R) such that ρ V = ρ and m n is time-invariant i ρ(v s n ) is dened and it evaluates to the value of m n . To conclude, γ( α(R)) contains (ρ, m) because for ρ all the conditions of the denition are satised.

Secondly, we need to show that α • γ is reductive, i.e, α( γ(R)) ⊆ R. Assume that ρ ∈ α( γ(R)). By construction, there exists (ρ, m) such that ρ V = ρ and m n is time-invariant with value ρ(v s n ) if v s n belongs to the domain of ρ, otherwise m n is time-dependent. Finally, exists ρ ′ ∈ R such that ρ ′ V = ρ and v s n corresponds to m n ; this proves that ρ ′ = ρ. ⊓ ⊔ Theorem 2. The semantic of statements, both forward and backward, is sound:

Proof. We focus on the input case as the other cases are trivial. Forward transfer function:

To conclude we need to show that (ρ, m) satises all the constraints of the states (ρ ′′ , m ′′ ).

) is undened and thus also in this case we satisfy the constraints of m

Backward transfer function:

To conclude, we recall few results from [38, Theorem 2]:

Using the second fact and the soundness of τ [[v := input n ()]] we have that:

then by the rst fact:

Proposition 1. ⊔ ♯ , ⊓ ♯ are sound under-approximations of ∪, ∩ and ∇ ♯ is a lower widening.

Proof.

) satisfying the denition. By soundness of the underapproximation join of D ♯ we have that ρ ∈ γ ♯ (d ♯ 1 ) or ρ ∈ γ ♯ (d ♯ 2 ), without loss of generality assume the former. The result follows from the chain of inclusions:

Remark: to compute the set of variables, we use the union rather than the intersection (as in the upper join). This is needed to preserve the soundness. Meet:

Lower widening: It is easy to check that ∇ ♯ under-approximates the intersection. The second case can only occur a nite number of times and the rst one terminates by the properties of ∇ ♯ .

⊓ ⊔ Theorem 3. The abstract semantic is sound, i.e., for any s ∈ While and d ♯ ∈ D ♯ the following holds:

Proof. The proof is done by induction on the syntax. We only focus on the input statement as the other ones are handled as usual.

Forward transfer function: The rst case (v s n / ∈ l) is easily sound as we add all values for v. If instead, v s n ∈ l then for all the environments of the concreatization we have that the variable v s n is dened, hence the premise of the implication (v s n ∈ dom( ρ) -see the denition of the concrete semantic) is always satised, so that x must be equal to ρ(v s n ), hence the soundness of the second case.

Backward transfer function: The soundness of the second case follows from the fact that all the environments will contain the stream variable v s n and thus only the rst case of the concrete semantic will be reached (which performs simply the assignment v := v s n ). In the rst case we perform the check

which corresponds to the test of the second case of the concrete semantic. Notice also that this subsumes the rst case, as ∀x. ρ Proof. In order to prove that ∇ ♯ p is a widening operator, we need show:

In order to prove the rst point, it is enough to exhibit, for every element of

By construction, ⊔ ♯ p = ∪, thus we can further assume without loss of generality that d

2 , proving the claim. Otherwise if d ♯ / ∈ S ♯ 2 , then d ♯ ∈ S ♯ u1 and thus d ♯ ⊑ ♯ ⊔ ♯ S ♯ u1 . Since ∇ ♯ is a widening, then d ♯ ⊑ ♯ ⊔ ♯ S ♯ u1 ⊑ ♯ (⊔ ♯ S ♯ u1 ) ∇ ♯ (⊔ ♯ S ♯ u2 ), which proves the result. In order to prove the second point, we need to show that there exists k ∈ N such that Y k = Y k+i for all i ≥ 0. As a preliminary step, notice that by construction of Y i and denition of ∇ ♯ , i ≤ j implies |Y i | ≥ |Y j | and for all i ∈ N |Y i | ≥ 0, so that the size of the powerset must converge in n steps to