Jingyu Ke

Hongfei Fu

Hongming Liu
email: hm-liu@sjtu.edu.cn

Liqian Chen
email: lqchen@nudt.edu.cn

Guoqiang Li
email: li.g@sjtu.edu.cn.

Disjunctive Affine

Gen- Eration Invariant

Farkas ' With

2023 Lemma

Hal

Affine Disjunctive Invariant Generation with Farkas' Lemma

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Invariant generation is the classical problem that aims at automated generation of assertions that overapproximates the set of reachable program states in a program. We consider affine invariants over affine while loops (i.e., loops with affine loop guards, conditional branches and assignment statements), and explore the automated generation of disjunctive affine invariants. Disjunctive invariants are important to capture disjunctive features in programs such as multiple phases, transitions between different modes, etc., and are typically more precise than conjunctive invariants over programs with these features. To generate tight affine invariants, existing approaches have investigated the application of Farkas' Lemma to conjunctive affine invariant generation, but none of them considers disjunctive affine invariants.

In this work, we introduce a novel approach to generate affine disjunctive invariants using Farkas' Lemma. Our approach employs a carefully designed control flow transformation to create an affine transition system from the original loop to which previous approaches in Farkas' Lemma apply. The affine transition system distinguishes paths within a loop body with their corresponding conjunctive invariants, and takes the disjunction of these conjunctive invariants. Furthermore, we propose optimizations to improve the scalability, accuracy and applicability of our approach. These optimizations include: a) an invariant propagation technique that enables the spread of invariants within the strongly connected components of the transition system to improve scalability; b) the tackling of infeasible implication in the application of Farkas' Lemma to improve accuracy; c) the standard loop summarization that extends our approach to nested loops to improve applicability. The experimental results over a benchmark set of more than 100 affine while loops (mostly from SVCOMP2023) shows that our approach outperforms other approaches in both the number of solved instances and the time efficiency. In particular, our approach handles most instances in 100 milliseconds, achieving a speedup of 10X to 1000X while maintaining a comparable success rate when compared with the state-of-the-art tool Veriabs.

INTRODUCTION

Invariant generation is the classical problem that targets the automated generation of invariants which can be used to aid the verification of critical program properties. An invariant at a program location is an assertion that over-approximates the set of program states reachable to that location, i.e., every reachable program state to the location is guaranteed to satisfy the assertion. Since invariants provide an over-approximation for reachable program states, they play a fundamental role in program verification and can be used for safety [START_REF] Albarghouthi | Ufo: A Framework for Abstraction-and Interpolation-Based Software Verification[END_REF][START_REF] Manna | Temporal verification of reactive systems -safety[END_REF][START_REF] Padon | Ivy: safety verification by interactive generalization[END_REF], reachability [START_REF] Alias | Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs[END_REF][START_REF] Asadi | Polynomial reachability witnesses via Stellensätze[END_REF][START_REF] Bradley | Linear Ranking with Reachability[END_REF][START_REF] Chen | Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems[END_REF][START_REF] Colón | Synthesis of Linear Ranking Functions[END_REF][START_REF] David | Danger Invariants[END_REF][START_REF] Podelski | A Complete Method for the Synthesis of Linear Ranking Functions[END_REF] and time-complexity [START_REF] Chatterjee | Non-polynomial Worst-Case Analysis of Recursive Programs[END_REF] analysis in program verification.

Automated approaches for invariant generation have been studied over decades and there have been an abundance of literature along this line of research. From different program objects, invariant generation targets numerical values (e.g., integers or real numbers) [START_REF] Bagnara | Precise Widening Operators for Convex Polyhedra[END_REF][START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF][START_REF] Chatterjee | Polynomial invariant generation for non-deterministic recursive programs[END_REF][START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF]Rodríguez-Carbonell and Kapur 2004a;[START_REF] Singh | Fast polyhedra abstract domain[END_REF], arrays [START_REF] Larraz | SMT-Based Array Invariant Generation[END_REF][START_REF] Srivastava | Program verification using templates over predicate abstraction[END_REF], pointers [START_REF] Calcagno | Compositional Shape Analysis by Means of Bi-Abduction[END_REF][START_REF] Chanh | SLING: using dynamic analysis to infer program invariants in separation logic[END_REF], algebraic data types [K. et al. 2022], etc. By different methodologies, invariant generation can be solved by abstract interpretation [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF][START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF][START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF][START_REF] Gopan | Guided Static Analysis[END_REF], constraint solving [START_REF] Chatterjee | Polynomial invariant generation for non-deterministic recursive programs[END_REF][START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF][START_REF] Cousot | Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming[END_REF][START_REF] Gulwani | Program analysis as constraint solving[END_REF], inference [START_REF] Calcagno | Compositional Shape Analysis by Means of Bi-Abduction[END_REF][START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF][START_REF] Donaldson | Software Verification Using k-Induction[END_REF][START_REF] Gan | Nonlinear Craig Interpolant Generation[END_REF][START_REF] Garg | ICE: A Robust Framework for Learning Invariants[END_REF][START_REF] Kenneth | Quantified Invariant Generation Using an Interpolating Saturation Prover[END_REF][START_REF] Sharma | From invariant checking to invariant inference using randomized search[END_REF][START_REF] Somenzi | IC3: where monolithic and incremental meet[END_REF][START_REF] Xu | Interval counterexamples for loop invariant learning[END_REF], recurrence analysis [START_REF] Farzan | Compositional Recurrence Analysis[END_REF][START_REF] Kincaid | Compositional recurrence analysis revisited[END_REF][START_REF] Kincaid | Non-linear reasoning for invariant synthesis[END_REF], machine learning [START_REF] Garg | Learning invariants using decision trees and implication counterexamples[END_REF][START_REF] He | Learning fast and precise numerical analysis[END_REF]Ryan et al. 2020;[START_REF] Yao | Learning nonlinear loop invariants with gated continuous logic networks[END_REF], data-driven approaches [START_REF] Chen | Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation[END_REF][START_REF] Csallner | DySy: dynamic symbolic execution for invariant inference[END_REF][START_REF] Chanh | SLING: using dynamic analysis to infer program invariants in separation logic[END_REF][START_REF] Nguyen | Using dynamic analysis to discover polynomial and array invariants[END_REF][START_REF] Riley | Multi-Phase Invariant Synthesis[END_REF][START_REF] Sharma | A Data Driven Approach for Algebraic Loop Invariants[END_REF], etc. Most results in the literature consider a strengthened version of invariants, called inductive invariants, that requires the inductive condition that the invariant at a program location is preserved upon every execution back and forth to the location (i.e., under the assumption that the invariant holds at the location, it continues to hold whenever the program execution goes back to the location).

In this work, we consider the automated generation of disjunctive invariants, i.e., invariants that are in the form of a disjunction of assertions. Compared with conjunctive invariants, disjunctive invariants capture disjunctive features such as multiple phases and mode transitions in loops. We primarily focus on the generation of affine disjunctive invariants in affine loops. An affine loop is a while loop where all conditional and assignment statements are in the form of linear expressions.

We consider constraint solving to generate affine disjunctive invariants. A typical constraint solving method is via Farkas' Lemma [START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF][START_REF] Ji | Affine Loop Invariant Generation via Matrix Algebra[END_REF][START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b] that provides a complete characterization for affine invariants. However, the application of Farkas' Lemma is limited to conjunction of affine inequalities. The question on how to leverage Farkas' Lemma to generate affine disjunctive invariants remains to be a challenge.

Our contributions. To address the aforementioned challenge, we explore a succinct disjunctive pattern from the conditional branches in a non-nested loop, show how this disjunctive pattern can be integrated with Farkas' Lemma, and further explore optimizations to increase the scalability, applicability and accuracy. Our detailed contributions cover the five points below.

First, we recognize that an important source of disjunction arises from the branching in control flow. To utilize the branching information, we explore a control flow transformation that transforms the loop into a transition system compatible with Farkas' Lemma. For non-nested loops, our approach collects every path that jumps from the entry point to the end of the loop body. These paths are treated as locations in the transition system. Then, our approach establishes the transitions between these locations to finish the construction of the transition system. Finally, affine conjunctive invariants are computed over the transition system by the previous approach [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]] in Farkas' Lemma, and the disjunctive invariant is the disjunction of the invariants at all locations.

Second, to mitigate the combinatorial explosion in the number of paths and during the invariant computation, we propose a novel invariant propagation technique dedicated to our control flow transformation. The technique starts to compute an invariant at the initial location, and proceeds by a breadth-first traversal to identify potential topological orders in the sub-transition system obtained by removing the initial location. Throughout invariant propagation, invariants are computed only at the initial location (of a strongly connected component of the transition system), and therefore could improve the scalability by mitigating the combinatorial explosion as stated above.

Third, we address the case of infeasible implication in the application of Farkas' Lemma that has not been addressed previously. This allows our approach to remove infeasible transitions in the transformed transition system, hence removing infeasible jumps between the paths of the loop body. Removing such transitions improves the accuracy of the generated invariants. Such accuracy gain is necessary since ignoring infeasible jumps may destroy the disjunctive feature in the loop.

Fourth, we extend our approach to nested loops via standard loop summary that extracts the input-output relationship of a loop. This improves the applicability of our approach.

Finally, we implement our approach as a prototype upon the Clang Static Analyzer [Clang Static Analyzer 2022]. Experiment over benchmarks from [START_REF] Sv-Comp | Software Verification Competition[END_REF][START_REF] Sv-Comp | Software Verification Competition[END_REF] and [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF] shows that our approach outperforms existing methods in both the number of solved instances and the time efficiency. Compared with the SV-COMP 2023 winner Veriabs [START_REF] Darke | VeriAbs: A tool for scalable verification by abstraction (competition contribution)[END_REF] in ReachSafety, our approach solves a comparable number of benchmarks with a speedup up to 3 orders of magnitude in time efficiency. Limitations. Our approach handles integer-value variables by the over-approximation to real numbers, and hence cannot handle machine integers in general. However, we can handle several simple properties of machine integers such as integer overflow by suitable piecewise linear representations.

PRELIMINARIES

We first recall affine transition systems [Sankaranarayanan et al. 2004b] and invariants over them, and then the classical theorem of Farkas' Lemma and some basic knowledge in polyhedra theory.

Affine Transition Systems and Invariants

To introduce affine transition systems, we need several basic concepts. An affine inequality over a set 𝑉 = {𝑥 1 , . . . , 𝑥 𝑛 } of real-valued variables is of the form 𝑎 1 𝑥 1 + • • • + 𝑎 𝑛 𝑥 𝑛 + 𝑏 ≥ 0, where 𝑎 𝑖 's and 𝑏 are real coefficients, An affine assertion over 𝑉 is a conjunction of affine inequalities and equalities over 𝑉 . A propositional affine predicate (PAP) over 𝑉 is a propositional formula whose atomic propositions are affine inequalities and equalities over 𝑉 . A PAP is in disjunctive (resp. conjunctive) normal form (DNF) (resp. CNF) if it is a finite disjunction of affine assertions (resp. a finite conjunction of finite disjunctions of affine assertions), respectively. An affine transition system possesses a finite number of locations and variables and specifies transitions between locations with affine guards and affine update on the values of the variables.

Definition 1 (Affine Transition Systems [Sankaranarayanan et al. 2004b]). An affine transition system (ATS) is a tuple Γ = ⟨𝑋, 𝑋 ′ , 𝐿, T, ℓ * , 𝜃 ⟩ for which:

• 𝑋 is a finite set of real-valued variables and 𝑋 ′ = {𝑥 ′ | 𝑥 ∈ 𝑋 } is the set of primed variables.

• 𝐿 is a finite set of locations and ℓ * ∈ 𝐿 is the initial location.

• T is a finite set of transitions where each transition 𝜏 is a triple ⟨ℓ, ℓ ′ , 𝜌⟩ from location ℓ to location ℓ ′ with the guard condition 𝜌 as a PAP over 𝑋 ∪ 𝑋 ′ . • 𝜃 is a PAP in DNF over the variables 𝑋 .

The directed graph DG(Γ) of the ATS Γ is defined as the graph where the vertices are the locations of Γ and there is an edge (ℓ, ℓ ′ ) iff there is a transition ⟨ℓ, ℓ ′ , 𝜌⟩ with source location ℓ and target location ℓ ′ .

The intuition of an ATS Γ = ⟨𝑋, 𝑋 ′ , 𝐿, T, ℓ * , 𝜃 ⟩ is as follows. Γ possesses locations 𝐿 and variables 𝑋 . Each variable 𝑥 ∈ 𝑋 is mostly used to represent the current value of the variable and each primed variable 𝑥 ′ ∈ 𝑋 ′ is used to represent the next value of its unprimed variable 𝑥 ∈ 𝑋 after one step of transition. Each transition ⟨ℓ, ℓ ′ , 𝜌⟩ specifies the jump from the current location ℓ to the next location ℓ ′ with the guard condition 𝜌 specifying the condition to enable the transition. The guard condition involves both the current values (represented by 𝑋 ) and the next values (by 𝑋 ′ ), so that it can specify the relationship between the current and next values. Each clause of the PAP 𝜃 specifies an independent initial condition at the initial location ℓ * .

Below we specify the semantics of an ATS. A valuation over a finite set 𝑉 of variables is a function 𝜎 : 𝑉 → R that assigns to each variable 𝑥 ∈ 𝑉 a real value 𝜎 (𝑥) ∈ R. In this work, mostly we consider valuations over the variables 𝑋 of an ATS and simply abbreviate "valuation over 𝑋 " as "valuation" (i.e., omitting 𝑋 ). Given an ATS, a configuration is a pair (ℓ, 𝜎) with the intuition that ℓ is the current location and 𝜎 is a valuation that specifies the current values for the variables.

Given an affine assertion 𝜑 and a valuation 𝜎 over a variable set 𝑉 , we write 𝜎 |= 𝜑 to mean that 𝜎 satisfies 𝜑, i.e., 𝜑 is true when one substitutes the corresponding values 𝜎 (𝑥) to all the variables 𝑥 in 𝜑. Given an ATS Γ, two valuations 𝜎, 𝜎 ′ and an affine assertion 𝜑 over 𝑋 ∪ 𝑋 ′ , we write 𝜎, 𝜎 ′ |= 𝜑 to mean that 𝜑 is true when one substitutes every variable 𝑥 ∈ 𝑋 by 𝜎 (𝑥) and every variable 𝑥 ′ ∈ 𝑋 ′ by 𝜎 ′ (𝑥) in 𝜑. Moreover, given two affine assertions 𝜑,𝜓 over a variable set 𝑉 , we write 𝜑 |= 𝜓 to mean that 𝜑 implies 𝜓 , i.e., for every valuation 𝜎 over 𝑉 we have that 𝜎 |= 𝜑 implies 𝜎 |= 𝜓 .

The semantics of an ATS Γ is given by its paths. A path 𝜋 of the ATS Γ is a finite sequence of configurations (ℓ 0 , 𝜎 0 ) . . . (ℓ 𝑘 , 𝜎 𝑘 ) such that

• (Initialization) ℓ 0 = ℓ * and 𝜎 0 |= 𝜃 , and

• (Consecution) for every 0 ≤ 𝑗 ≤ 𝑘 -1, there exists a transition 𝜏 = ⟨ℓ, ℓ ′ , 𝜌⟩ such that ℓ = ℓ 𝑗 , ℓ ′ = ℓ 𝑗+1 and 𝜎 𝑗 , 𝜎 𝑗+1 |= 𝜌.
We say that a configuration (ℓ, 𝜎) is reachable if there exists a path (ℓ 0 , 𝜎 0 ) . . . (ℓ 𝑘 , 𝜎 𝑘 ) such that (ℓ 𝑘 , 𝜎 𝑘 ) = (ℓ, 𝜎). Intuitively, a path starts with some legitimate initial configuration (as specified by Initialization) and proceeds by repeatedly applying the transitions to the current configuration (as described in Consecution). Thus, any path 𝜋 = (ℓ 0 , 𝜎 0 ) . . . (ℓ 𝑘 , 𝜎 𝑘 ) corresponds to a possible execution of the underlying ATS. Informally, an ATS starts at the initial location ℓ * with an arbitrary initial valuation 𝜎 * such that 𝜎 * |= 𝜃 , constituting an initial configuration (ℓ 0 , 𝜎 0 ); then at each step 𝑗 (𝑗 ≥ 0), given the current configuration (ℓ 𝑗 , 𝜎 𝑗 ), the ATS determines the next configuration (ℓ 𝑗+1 , 𝜎 𝑗+1 ) by first selecting a transition 𝜏 = ⟨ℓ, ℓ ′ , 𝜌⟩ such that ℓ = ℓ 𝑗 and then choosing (ℓ 𝑗+1 , 𝜎 𝑗+1 ) to be any configuration that satisfies ℓ 𝑗+1 = ℓ ′ and 𝜎 𝑗 , 𝜎 𝑗+1 |= 𝜌.

In the following, we assume that the guard condition 𝜌 of each transition in a ATS is an affine assertion. This follows from the fact that one can always transform the guard condition into a DNF and then split the transition into multiple sub-transitions where the guard condition of each sub-transition is an affine assertion that is a disjunctive clause of the DNF. A small detail here is that to handle strict inequalities such as 𝛼 < 𝛽 which arise from taking the negation of a non-strict affine inequality, we either have the over-approximation 𝛼 ≤ 𝛽 or tighten it as 𝛼 ≤ 𝛽 -1 in the integer case (i.e., every variable is integer valued, and every coefficient is an integer).

We consider invariants over affine transition systems. An invariant at a location ℓ of an ATS is an assertion 𝜑 such that for every path 𝜋 = (ℓ 0 , 𝜎 0 ) . . . (ℓ 𝑘 , 𝜎 𝑘 ) of the ATS and each 0 ≤ 𝑖 ≤ 𝑘, it holds that ℓ 𝑖 = ℓ implies 𝜎 𝑖 |= 𝜑. An invariant 𝜑 is affine if 𝜑 is an affine assertion over the variable set 𝑋 , and is disjunctively affine if 𝜑 is a PAP in DNF. Intuitively, an invariant 𝜑 at a location ℓ is an assertion that over-approximates the set of reachable configurations at ℓ; the invariant is affine if it is in the form of an affine assertion, and disjunctively affine if it is a disjunction of affine assertions.

In invariant generation, one often investigates a strengthened version of invariants called inductive invariants. In this work, we present affine inductive invariants in the form of inductive affine assertion maps [START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF][START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b] as follows. An affine assertion map (AAM) over an ATS is a function 𝜂 that maps every location ℓ of the ATS to an affine assertion 𝜂 (ℓ) over the variables 𝑋 . An AAM 𝜂 is called inductive if the following holds:

• (Initialization) 𝜃 |= 𝜂 (ℓ * ); • (Consecution) For every transition 𝜏 = ⟨ℓ, ℓ ′ , 𝜌⟩, we have that 𝜂 (ℓ) ∧ 𝜌 |= 𝜂 (ℓ ′ ) ′ , where 𝜂 (ℓ ′ ) ′ is the affine assertion obtained by replacing every variable 𝑥 ∈ 𝑋 in 𝜂 (ℓ ′ ) with its next-value counterpart 𝑥 ′ ∈ 𝑋 ′ .

Informally, an AAM is inductive if it is (i) implied by the initial condition given by 𝜃 at the initial location ℓ * (i.e., Initialization) and (ii) preserved under the application of every transition (i.e., Consecution). By a straightforward induction on the length of a path under an ATS, one could verify that every affine assertion in an inductive AAM is indeed an invariant. In the rest of the work, we focus on the automated synthesis of inductive AAMs, and the disjunctive affine invariants are obtained by taking a disjunction of relevant affine assertions in an AAM.

In this work, we also encounter the notion of loop summary. Loop summary describes the relationship between the input and output of a while loop. Given an ATS, we denote by 𝑋 in := {𝑥 in | 𝑥 ∈ 𝑋 } a copy of input variables from 𝑋 and 𝑋 out := {𝑥 out | 𝑥 ∈ 𝑋 } a copy of output variables. We write x in (resp. x out ) for the vector of input (resp. output) variables, respectively. With the designated termination location ℓ 𝑒 at the end of a while loop, a loop summary 𝑆 is a logical formula 𝑆 (x in , x out ) with free variables x in , x out such that for all paths 𝜋 = (ℓ 0 , 𝜎 0 ) . . . (ℓ 𝑘 , 𝜎 𝑘 ) such that ℓ 𝑘 = ℓ 𝑒 , we have 𝑆 (𝜎 0 , 𝜎 𝑘 ).

Farkas' Lemma and Polyhedra

Farkas' Lemma [START_REF] Farkas | A Fourier-féle mechanikai elv alkalmazásai (Hungarian)[END_REF]] is a classical theorem in the theory of affine inequalities and previous results [START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF][START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b] have applied the theorem to affine invariant generation. In these results, the form of Farkas' Lemma follows [Schrijver 1999, Corollary 7.1h].

Theorem 2.1 (Farkas' Lemma). Consider an affine assertion 𝜑 over a set 𝑉 = {𝑥 1 , . . . , 𝑥 𝑛 } of real-valued variables as in Figure 1a. When 𝜑 is satisfiable (i.e., there is a valuation over 𝑉 that satisfies 𝜑), it implies an affine inequality 𝜓 as in Figure 1b (i.e., 𝜑 |= 𝜓 ) if and only if there exist non-negative real numbers 𝜆 0 , 𝜆 1 , . . . , 𝜆 𝑚 such that (i) 𝑐 𝑗 = 𝑚 𝑖=1 𝜆 𝑖 • 𝑎 𝑖 𝑗 for all 1 ≤ 𝑗 ≤ 𝑛, and (ii) 𝑑 = 𝜆 0 + 𝑚 𝑖=1 𝜆 𝑖 •𝑏 𝑖 as in Figure 1c. Moreover, 𝜑 is unsatisfiable if and only if the inequality -1 ≥ 0 (as 𝜓 ) can be derived from above.

𝜑 :

𝑎 11 •𝑥 1 +• • •+ 𝑎 1𝑛 •𝑥 𝑛 +𝑏 1 ≥0 . . . . . . . . . 𝑎 𝑚1 •𝑥 1 +• • •+𝑎 𝑚𝑛 •𝑥 𝑛 +𝑏 𝑚 ≥0 (a) 𝜑 in Farkas' Lemma 𝜓 : 𝑐 1 •𝑥 1 +• • •+𝑐 𝑛 •𝑥 𝑛 +𝑑 ≥0 (b) 𝜓 in Farkas' Lemma 𝜆 0 1 ≥ 0 𝜆 1 𝑎 11 • 𝑥 1 +• • •+ 𝑎 1𝑛 • 𝑥 𝑛 + 𝑏 1 1 0 . . . . . . . . . . . . 𝜆 𝑚 𝑎 𝑚1 • 𝑥 1 +• • •+𝑎 𝑚𝑛 • 𝑥 𝑛 +𝑏 𝑚 𝑚 0 𝑐 1 • 𝑥 1 +• • •+ 𝑐 𝑛 • 𝑥 𝑛 + 𝑑 ≥ 0 -1 ≥ 0          𝜑 ← 𝜓 ←false ⇒ 𝜆 1 𝑎 11 +• • •+𝜆 𝑚 𝑎 𝑚1 =𝑐 1 . . . 𝜆 1 𝑎 1𝑛 +• • •+𝜆 𝑚 𝑎 𝑚𝑛 =𝑐 𝑛 𝜆 0 +𝜆 1 𝑏 1 +• • •+𝜆 𝑚 𝑏 𝑚 = 𝑑 . . .
(c) The Tabular Form for Farkas' Lemma Fig. 1. The 𝜑, 𝜓 and Tabular Form for Farkas' Lemma [START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF]Sankaranarayanan et al. 2004b] One direction of Farkas' Lemma is straightforward, as one easily sees that if we have a nonnegative affine combination of the inequalities in 𝜑 that can derive 𝜓 , then it is guaranteed that 𝜓 holds whenever 𝜑 is true. Farkas' Lemma further establishes that the other direction is also valid. In general, Farkas' Lemma simplifies the inclusion of a polyhedron inside a halfspace into the satisfiability of a system of affine inequalities. We refer to the case of unsatisfiable 𝜑 with 𝜓 := -1 ≥ 0 in the statement of Theorem 2.1 as infeasible implication.

The application of Farkas' Lemma can be visualized by the tabular form in Figure 1c (taken from [START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF]), where 1 , . . . , 𝑚 ∈ {=, ≥} and we multiply 𝜆 0 , 𝜆 1 , . . . , 𝜆 𝑚 with their inequalities in 𝜑 and sum up them together to get 𝜓 . For 1 ≤ 𝑗 ≤ 𝑚, we require 𝜆 𝑗 ≥ 0. (a) Source 𝑃 1 and its transformation 𝑃 2 .

𝑋 = {𝑥, 𝑦}, 𝐿 = {ℓ 1 , ℓ * 2 }, T = {𝜏 1 , 𝜏 2 , 𝜏 3 , 𝜏 4 }, 𝜃 : 𝑥 = 0 ∧ 𝑦 = 50, 𝜏 1 : ⟨ℓ 1 , ℓ 1 , 𝜌 1 ⟩, 𝜏 2 : ⟨ℓ 1 , ℓ 2 , 𝜌 2 ⟩, 𝜏 3 : ⟨ℓ 2 , ℓ 2 , 𝜌 3 ⟩, 𝜏 4 : ⟨ℓ 2 , ℓ 1 , 𝜌 4 ⟩, 𝜌 1 :        50 ≤ 𝑥 ≤ 99 50 ≤ 𝑥 ′ ≤ 99 𝑥 ′ = 𝑥 + 1 𝑦 ′ = 𝑦 + 1        , 𝜌 2 :        50 ≤ 𝑥 ≤ 99 𝑥 ′ ≤ 49 𝑥 ′ = 𝑥 + 1 𝑦 ′ = 𝑦 + 1        𝜌 3 :        𝑥 ≤ 49 𝑥 ′ ≤ 49 𝑥 ′ = 𝑥 + 1 𝑦 ′ = 𝑦       
, 𝜌 4 :

       𝑥 ≤ 49 50 ≤ 𝑥 ′ ≤ 99 𝑥 ′ = 𝑥 + 1 𝑦 ′ = 𝑦        (b)
The ATS Corresponding to 𝑃 2 Fig. 2. An affine while loop from [START_REF] Sharma | Simplifying Loop Invariant Generation Using Splitter Predicates[END_REF] and its transformed form and corresponding ATS

In the previous results, the infeasible implication is not handled. In this work, we present a way to handle this via a nontrivial manipulation of polyhedra. To this end, we recall basic concepts from polyhedra theory as follows.

A subset

𝑃 of R 𝑛 is a polyhedron if 𝑃 = {x ∈ R 𝑛 | A •
x ≤ b} for some real matrix 𝐴 ∈ R 𝑚×𝑛 and real vector b ∈ R 𝑚 , where x is treated as a column vector and the comparison A

• x ≤ b is defined in the coordinate-wise fashion. A polyhedron 𝑃 is a polyhedral cone if 𝑃 = {x ∈ R 𝑛 | A • x ≤ 0} for some real matrix 𝐴 ∈ R 𝑚×𝑛 ,
where 0 is the 𝑚-dimensional zero column vector. It is well-known from the Farkas-Minkowski-Weyl Theorem [Schrijver 1999, Corollary 7.1a] that any polyhedral cone 𝑃 can be represented as 𝑃 = { 𝑘 𝑖=1 𝜆 𝑖 • g 𝑖 | 𝜆 𝑖 ≥ 0 for all 1 ≤ 𝑖 ≤ 𝑘 } for some real vectors g 1 , . . . , g 𝑘 , where such vectors g 𝑖 's are called a collection of generators for the polyhedral cone 𝑃.

OVERVIEW OF OUR APPROACH

Below we use a simple affine while loop as an example to provide an overview of our approach.

Consider the simple affine program 𝑃 1 as shown in Figure 2a. Our method primarily involves three steps. The first step is to transform general non-nested loops into a canonical control flow format, which is done by traversing from the loop head to the loop tail, extracting each feasible path 𝜋 of the loop body, and converting it into an equivalent canonical form. This form corresponds to one case statement for each path's guard condition 𝜙, where each guard condition is a conjunction of a conditional formula 𝜙 𝑐 and an assignment formula 𝜙 𝑎 .

Example 1. Take the transformed program 𝑃 2 in Figure 2a as an example. we elaborate the transformation for case 𝑥 > 49. Starting from the loop head and traversing the source program 𝑃 1 , we first handle the assignment 𝑥 = 𝑥 +1 and transform the statement to the assignment formula 𝜙 𝑎 := 𝑥 ′ = 𝑥 +1, where 𝑥 ′ is the value of 𝑥 after the assignment. Continuing the traversal, we handle the if branch if(𝑥 > 50) and explore both the situations where the branch condition is true and false. If the branch condition evaluates to true, we establish the conditional formula 𝜙 𝑐 := 𝑥 +1 > 50 since the current value of 𝑥 has been incremented by one in the loop execution, and then traverse the assignment 𝑦 = 𝑦 + 1, resulting in the updated assignment formula 𝜙 𝑎 = 𝑥 ′ = 𝑥 + 1 ∧ 𝑦 ′ = 𝑦 + 1. At this point, the traversal reaches the loop tail. Hence, the path for the if branch evaluated to true is described by the formula 𝜙 𝑐 ∧ 𝜙 𝑎 where 𝜙 𝑐 = 𝑥 > 49 and 𝜙 𝑎 = 𝑥 ′ = 𝑥 + 1 ∧𝑦 ′ = 𝑦 + 1, and corresponds to case 𝑥 > 49 in 𝑃 2 . □ To obtain affine disjunctive invariants over the transformed program 𝑃 2 , the second step is to construct an ATS from 𝑃 2 . In this ATS, each case statement in the program 𝑃 2 is considered as an independent location. The jumps between the locations are derived from the jumps between difference case statements in the current and next loop iteration of 𝑃 2 .

Example 2. To create an ATS from the transformed program 𝑃 2 , our primary focus is on the creation of locations and transitions. In 𝑃 2 , there are two case statements, leading to a maximum of four possible transitions in a complete directed graph. The ATS is shown in Figure 2b. Take the self-loop transition 𝜏 1 at ℓ 1 in the figure. The location ℓ 1 corresponds to case 𝑥 > 49 in 𝑃 2 , and we denote 𝜙 𝑐 := 𝑥 > 49. The transition 𝜏 1 := ⟨ℓ 1 , ℓ 1 , 𝜌 1 ⟩ describes the situation that the loop 𝑃 2 executes the case of 𝑥 > 49 both in the current and next loop iteration. In this transition, the guard condition 𝜌 1 is a conjunction specifying that both the current and the next loop iterations enter case 𝑥 > 49, which gives

𝜌 1 := 𝜙 𝑐 ∧ 𝜙 𝑐 [𝑥 ′ /𝑥] ∧ 𝜙 𝑎 ∧ 𝐺 ∧ 𝐺 [𝑥 ′ /𝑥]
where 𝜙 𝑎 := 𝑥 ′ = 𝑥 + 1 ∧𝑦 ′ = 𝑦 + 1 is the assignment formula discussed in Example 1 and 𝐺 := 𝑥 < 100 is the loop guard. Other transitions (i.e., 𝜏 2 , 𝜏 3 , 𝜏 4 ) are derived similarly, see Figure 2b for details. □ After the ATS is constructed, the third step is to apply the approaches [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b] in Farkas' Lemma to obtain invariants at the locations of the ATS, and group them disjunctively together to obtain the final invariant. Below we give a brief illustration.

Example 3. Consider to generate affine invariants over the ATS in Figure 2b. The approach [Sankaranarayanan et al. 2004b] first establishes an affine template at each location by setting 𝜂 (ℓ

𝑖 ) := 𝑐 ℓ 𝑖 ,1 𝑥 + 𝑐 ℓ 𝑖 ,2 𝑦 + 𝑑 ℓ 𝑖 ≥ 0 for 𝑖 ∈ {1, 2}, where 𝑐 ℓ 𝑖 ,1 , 𝑐 ℓ 𝑖 ,2
, 𝑑 ℓ 𝑖 are unknown coefficients to be resolved. Then, it generates the constraints from the initialization and consecution conditions and simplifies the constraints by the Farkas' tabular in Figure 1c. The initialization of 𝜃 |= 𝜂 (ℓ * ) results in linear constraints over the unknown coefficients, but the consecution 𝜂 (ℓ) ∧ 𝜌 |= 𝜂 (ℓ ′ ) ′ for a transition 𝜏 = ⟨ℓ, ℓ ′ , 𝜌⟩ results in quadratic constraints in the unknown coefficients since we have an unknown coefficient (say 𝜇) multiplied to 𝜂 (ℓ). To resolve the quadratic constraints from the consecution, the previous approach [Sankaranarayanan et al. 2004b] has considered heuristics to guess the value of the multiplier 𝜇 through either practical rules such as factorization or setting 𝜇 manually to 0 or 1.

After the application of the Farkas' tabular, the derived constraints in the unknown coefficients constitute a PAP Φ in CNF. The approach [Sankaranarayanan et al. 2004b] expands the PAP Φ equivalently into a DNF where each clause in the disjunction is an affine assertion that defines a polyhedral cone, and further computes the the affine invariants as the generators of the polyhedral cones in the DNF. A polyhedral cone from a clause in the DNF is shown in Figure 3a (where we abbreviate 𝑐 ℓ 𝑖 ,𝑗 , 𝑑 ℓ 𝑖 as 𝑐 𝑖 𝑗 , 𝑑 𝑖 ), and the generators of the polyhedral cone is shown in the left part of Figure 3b where "point" means a single vector, "ray" means a vector that can be scaled by an arbitrary positive value, and "line" means a vector that can be scaled by an any positive or negative value. When putting the generators back to invariants, we obtain the invariants shown in the right part of Figure 3b. In Figure 3b, we remove trivial invariants such as 0 ≥ 0 and redundant inequalities. In the end, the overall disjunctive invariant at the entry point of the loop body is 𝜂 (ℓ 1 ) ∨ 𝜂 (ℓ 2 ), which is (𝑥 = 𝑦 ∧ 50 ≤ 𝑥 ≤ 99) ∨ (𝑦 = 50 ∧ 0 ≤ 𝑥 ≤ 49). Additionally, we can calculate the invariant at the loop exit location, which we denote by ℓ 𝑒 . The calculation formula can be expressed as 𝜂 (ℓ 𝑒 ) = 𝑖 (𝜂 (ℓ 𝑖 ) ∧ 𝜙 𝑖𝑎 ∧ ¬𝐺), where 𝜙 𝑖𝑎 is the assignment formula corresponding to the path of ℓ 𝑖 , and 𝐺 is the loop guard. Therefore, we can simply calculate 𝜂 (ℓ 𝑒 ) := 𝑥 = 𝑦 = 100. □

         𝑐 12 -𝑐 22 = 0, 𝑐 21 ≥ 0, 𝑐 11 + 𝑐 12 ≥ 0, 50𝑐 12 + 𝑑 2 ≥ 0, 50𝑐 11 + 𝑑 1 -49𝑐 21 -𝑑 2 ≥ 0          (a) A clause in the DNF type 𝑐 11 𝑐 12 𝑑 1 𝑐 21 𝑐 22 𝑑 2 𝜂 (ℓ 1 ) 𝜂 (ℓ 2 ) point 0 0 0 0 0 0 0 ≥ 0 0 ≥ 0 line 1 -1 0 0 -1 50 𝑥 -𝑦 = 0 -𝑦 + 50 = 0 ray 0 0 49 1 0 0 49 ≥ 0 𝑥 ≥ 0 ray 0 0 1 0 0 0 1 ≥ 0 0 ≥ 0 ray 1 0 -50 0 0 0 𝑥 -50 ≥ 0 0 ≥ 0 ray 0 0 1 0 0 1 1 ≥ 0 1 ≥ 0 (b)
In the third step, we observe that existing approaches [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b] in Farkas' Lemma is not computationally efficient since all these approaches require to compute the invariants at all locations of an ATS. Hence, the amount of computation may be huge if the number of locations is considerable. Thus, we propose an invariant propagation technique that computes invariants only at the starting location (of a strongly connected component of the ATS) and propagates this invariant to other locations through a local topological order. This approach reduces the amount of computation for invariant generation. The following example provides a simple illustration of this technique, with a more detailed treatment to be given in the next section.

Example 4. Consider the affine transition system Γ in Figure 2b. Its underlying directed graph 𝐷𝐺 (Γ) is given in Figure 4a (here we ignore the termination location ℓ 𝑒 ). As we have calculated the invariant 𝜂 (ℓ 2 ) := 𝑦 = 50 ∧ 0 ≤ 𝑥 ≤ 49 at the initial location ℓ 2 , we can ignore all transitions leading to ℓ 2 (the correctness of which will be demonstrated in the next section), transforming it into the form as shown in Figure 4b. By ignoring the self-loop 𝜏 1 , we obtain a local topological order ℓ 2 < ℓ 1 . By propagating the invariant 𝜂 (ℓ 2 ) along the transition 𝜏 4 to the location ℓ 1 , we establish the initial condition 𝜓 1 for the location ℓ 1 . Subsequently, we consider the ATS obtained by removing the location ℓ 1 , corresponding to Figure 4c. This ATS consists of one location ℓ 1 with the initial condition 𝜓 1 and the self-loop transition T 1 . By solving this reduced ATS, we obtain the invariant 𝜂 (ℓ 1 ) = (𝑥 = 𝑦 ∧ 50 ≤ 𝑥 ≤ 99). □

𝑙 2 𝑙 1 𝜏 3 𝜏 4 𝜏 1 𝜏 2 (a) 𝐷𝐺 (Γ) of ATS in Figure 2b 𝑙 2 𝑙 1 𝜏 4 𝜏 1 (b) 𝐷𝐺 (Γ) After Elimination 𝑙 1 𝜏 1 (c) 𝐷𝐺 (Γ) After Propagation

ALGORITHMIC TECHNIQUES FOR AFFINE DISJUNCTIVE INVARIANT GENERATION

In this section, we formally present our method for generating affine disjunctive invariants over nonnested loops. Our method includes a control flow transformation that transforms a non-nested loop into an affine transition system, an invariant propagation technique that optimizes the invariant generation process, and the tackling of the infeasible implication in the application of Farkas' Lemma to optimize the accuracy.

Control Flow Transformation

Throughout the section, we fix the set of program variables in a loop as 𝑋 = {𝑥 1 , . . . , 𝑥 𝑛 } and identify it as the set of variables in the ATS to be derived from the loop. We consider the canonical form of a non-nested affine while loop as in Figure 5, where we have:

• The column vector x = (𝑥 1 , . . . , 𝑥 𝑛 ) T represents the vector of program variables.

• 𝐺 is the loop condition (or loop guard) of the while loop that in general can be a PAP.

• The case keyword divides the loop into conditional branches so that if the current values of the program variables satisfy the condition 𝜙 𝑖 , then the assignment at the 𝑖th conditional branch (i.e., x := F 𝑖 (x)) is executed. Note that we do not require the branch conditions 𝜙 1 , . . . , 𝜙 𝑚 need not to be logically pairwise disjoint.

• Each F 𝑖 (1 ≤ 𝑖 ≤ 𝑚) is an affine function, i.e., F 𝑖 (x) = Ax + b where A (resp. b) is an
𝑛 × 𝑛 square matrices (resp. 𝑛-dimensional column vector) that specifies the affine update under the function F 𝑖 in the conditional branch 𝜙 𝑖 . The assignment x := F 𝑖 (x) is considered simultaneously for the variables in x so that in one execution step, the current valuation 𝜎 is updated to F 𝑖 (𝜎). • The statements 𝛿 1 , . . . , 𝛿 𝑚 specify whether the loop continues after the affine update of the conditional branches 𝜙 1 , . . . , 𝜙 𝑚 . Each statement 𝛿 𝑖 is either the skip statement that does nothing (which means that the loop continues after the affine update of F 𝑖 ) or the break statement (which means that the loop exits after the affine update).

while (𝐺) { c a s e 𝜙 1 : x := F 1 (x) ; 𝛿 1 ; . . . c a s e 𝜙 𝑚 : x := F 𝑚 (x) ; 𝛿 𝑚 ; } Fig. 5. The canonical form of a non-nested affine while loop Any non-nested affine while loop with break statement can be transformed into the canonical form in Figure 5 by recursively examining the substructures of the loop body of the loop. A detailed recursive transformation process is provided in Appendix A. Note that although the transformation into our canonical form may cause exponential blow up in the number of conditional branches in the loop body, in practice a loop typically has a small number of conditional branches and further improvement can be carried out by removing invalid branches (i.e., those whose branch condition is unsatisfiable, such as 𝜏 2 in Figure 2). Moreover, such a canonical form is often necessary to capture precise disjunctive information in a while loop.

Below we demonstrate our control flow transformation that transforms the canonical form into an ATS. The intuition is that we treat each branch condition 𝜙 𝑖 in the figure as a standalone location and the overall disjunctive invariant is the disjunction of the generated invariants at these locations. Moreover, the transitions are determined by the jumps between branch locations on whether the loop will enter a branch condition in the next loop iteration given the branch condition the loop currently resides in. The detailed transformation is given as follows.

Formally, the ATS Γ 𝑊 for a loop 𝑊 in our canonical form is constructed as follows:

• The set of locations is {ℓ 1 , . . . , ℓ 𝑚 , ℓ 𝑒 }, where each ℓ 𝑖 (1 ≤ 𝑖 ≤ 𝑚) corresponds to the branch condition 𝜙 𝑖 and ℓ 𝑒 is the termination location of the loop.

• For each 1 ≤ 𝑖 ≤ 𝑚 such that 𝛿 𝑖 = break, we have the transition (we denote

x ′ := (𝑥 ′ 1 , . . . , 𝑥 ′ 𝑛 ) T ) 𝜏 𝑖 = (ℓ 𝑖 , ℓ 𝑒 , 𝐺 ∧ 𝜙 𝑖 ∧ x ′ = F 𝑖 (x))
that specifies the one-step jump from the branch condition 𝜙 𝑖 to the termination location ℓ 𝑒 , where the guard condition is a conjunction of the loop guard G (for staying in the loop at the current loop iteration), the branch condition 𝜙 𝑖 (that the current execution of the loop body resides in 𝜙 𝑖 ) and x ′ = F 𝑖 (x) (for the affine update). • For each 1 ≤ 𝑖, 𝑗 ≤ 𝑚 such that 𝛿 𝑖 ≠ break, we have the transition

𝜏 𝑖 𝑗 = (ℓ 𝑖 , ℓ 𝑗 , 𝐺 ∧ 𝜙 𝑖 ∧ 𝐺 [x ′ /x] ∧ 𝜙 𝑗 [x ′ /x] ∧ x ′ = F 𝑖 (x))
that specifies the jump from the branch condition 𝜙 𝑖 in the current loop iteration to the branch condition 𝜙 𝑗 in the next loop iteration, for which the guard condition is

𝐺 ∧ 𝜙 𝑖 ∧ 𝐺 [x ′ /x] ∧ 𝜙 𝑗 [x ′ /x] ∧ x ′ = F 𝑖 (x)
since the transition needs to pass the loop guard 𝐺, satisfy the branch condition 𝜙 𝑖 when staying in the location ℓ 𝑖 , have the affine update specified by F 𝑖 and fulfill the loop guard 𝐺 [x ′ /x] and the branch condition 𝜙 𝑗 upon entering the location ℓ 𝑗 in the next loop iteration.

• For each 1 ≤ 𝑖 ≤ 𝑚 such that 𝛿 𝑖 ≠ break, we have the transition

𝜏 ′ 𝑖 = (ℓ 𝑖 , ℓ 𝑒 , 𝐺 ∧ 𝜙 𝑖 ∧ (¬𝐺) [x ′ /x] ∧ x ′ = F 𝑖 (x))
for the jump from the branch condition 𝜙 𝑖 to the termination location ℓ 𝑒 for which the guard condition is a conjunction of the loop guard 𝐺, the branch condition 𝜙 𝑖 , the affine update x ′ = F 𝑖 (x) and the negation of the loop guard (for jumping out of the loop).

After the transformation, we remove transitions with unsatisfiable guard condition to reduce the size of the derived ATS. The transformation for our running example has been given in Example 2. With the transformed ATS Γ 𝑊 , we follow existing approaches [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b] to generate affine conjunctive invariants at the locations of the ATS Γ 𝑊 . In particular, we apply the recent approach [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]] that has the most scalability. Finally, recall that the overall disjunctive invariant for the ATS Γ 𝑊 is the disjunction of the invariants at all the locations.

Invariant Propagation

In the computation of invariants, previous approaches [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b] require to generate the invariants at all the locations of an ATS. As invariant computation is usually expensive, it is important to explore optimizations that avoid to generate invariants at every location. In this section, we propose a novel invariant propagation technique that is applicable to any directed graph of an ATS and achieves maximal efficiency in specific graph structures such as directed cycles. Below we demonstrate the invariant propagation via its pseudocode.

The pseudocode is given in Algorithm 1, where the variable SCCs denotes a list of sub-ATS's, each element Γ 𝑖 corresponding to the ATS of a strongly connected component in the 𝐷𝐺 (Γ) graph, and the variable SCCNo denotes the index of the SCC, to which ℓ belongs, in the list SCCs. Moreover, FindSCC(ℓ, SCCs) is used to find the index of the SCC containing the location ℓ in the SCCs. Merge(𝜂, 𝜂 𝑠 ) is employed to merge two inductive assertion maps by disjunction. Project(Γ, ℓ) is used to remove the relevant location and transitions of ℓ in ATS Γ to obtain the sub-ATS Γ 𝑠𝑢𝑏 .

First, at Line 1 of Algorithm 1, the Tarjan() function, which refers to the classic Tarjan's algorithm to compute the strongly connected components (SCC) of a directed graph [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF]], computes the list of strongly connected components SCCs = Γ 1 , . . . , Γ 𝑛 of the input ATS Γ. Subsequently, we decompose the entire directed graph 𝐷𝐺 (Γ) into the clusters of its strongly connected components and cases that cannot be further divided. In the following text, we use "SCC" to refer to the strongly Algorithm 1 Invariant Propagation InvProp(Γ, 𝐷𝐺 (Γ), ℓ * ) Require: Γ -ATS, 𝐷𝐺 (Γ) -directed graph of Γ, ℓ * -initial location of Γ. Ensure: 𝜂 -an inductive assertion map for Γ.

1: SCCs = Tarjan(𝐷𝐺 (Γ), Γ) 2: if Len(SCCs) ≠ 1 then 3:

SCCNo = FindSCC(ℓ * , SCCs) 4:
stack.𝑝𝑢𝑠ℎ(SCCNo, ℓ * ) 5:

while ¬ stack.isEmpty() do 6:

curNo, ℓ 𝑠 = stack.pop()

7: Γ 𝑠 = SCCs[curNo] 8: 𝜂 s = InvProp(Γ 𝑠 , 𝐷𝐺 (Γ 𝑠 ), ℓ 𝑠 ) 9:
for each transition 𝜏 directed from ℓ 𝑠 to ℓ 𝑡 do 10:

nextNo=FindSCC(ℓ 𝑡 , SCCs)

𝜂 s = InvProp(Γ 𝑠 , 𝐷𝐺 (Γ 𝑠 ), ℓ 𝑡 ) 21:
𝜂 = Merge(𝜂, 𝜂 s ) 22: end for 23: return 𝜂 connected components in the directed graph, as well as to both the ATS Γ projected onto the corresponding parts and the sub-ATS Γ 𝑠 .

For the divisible cases that the whole graph 𝐷𝐺 (Γ) can be divided into different SCCs, as encountered at Line 2, we traverse the SCCs starting from the SCC of the initial location ℓ * in a depth-first search order. In each traversal, we call the InvProp() function on the current SCC to solve its inductive AAM 𝜂. We then consider transitions that connect the current SCC to another SCC (at Line 9 of the pseudocode, with some details omitted such as the fact that these edges definitely connect the current SCC with another distinct SCC). We conjunctively propagate the invariants with the transition guard conditions in a single step to another SCC, setting it as the initial condition 𝜃 . Afterwards, we add this to the stack, specifying the relevant starting location.

For the indivisible cases, we adopt the projection method as in [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF] to compute the invariant 𝜂 (ℓ * ) at the starting location ℓ * only, which is implemented by InitInv() in Line 17. Similarly, we project the SCC onto the sub-SCC Γ 𝑠𝑢𝑏 (Line 18) after removing the initial location ℓ * . We then consider the initial conditions 𝜃 𝑠 and location ℓ 𝑠 for Γ 𝑠 obtained along different transitions (Line 19) originating from the initial location. The InvProp() function is recursively called to obtain the complete inductive AAM 𝜂 for the input Γ.

Example 5. Recall the example in Section 3, specifically Example 4. Here, Γ is an indivisible SCC. After computing the invariant 𝜂 (ℓ 2 ) of the ATS Γ at the initial location ℓ 2 , we consider all transitions {𝜏 4 } starting from the initial location ℓ 2 , as depicted in the figure. Then, we propagate the invariant through the transition 𝜏 4 to ℓ 1 . After project to obtain the remaining sub-ATS Γ 𝑠𝑢𝑏 , composed of ℓ 1 and its self-loop transition, we recursively compute this indivisible SCC to obtain the complete inductive assertion map. □

Our invariant propagation technique applies to all ATS. The main advantage to incorporate this technique is that it allows the generation of invariants only at the initial locations of (sub-)SCCs, thus avoiding the generation of the ivnariants at all locations as adopted in [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]Sankaranarayanan et al. 2004b]. In the case that the directed graph of the input ATS is a cycle, our invariant propagation reaches the highest efficiency that generates the invariant only at the initial location of the cycle and derives invariants at other locations of the cycle by propagation, since the cycle has an explicit topological order after the removal of the initial location. This advantage becomes more prominent in loops with a non-neglectable amount of conditional branches.

Finally, we present the soundness of the invariant propagation in the following theorem.

Theorem 4.1. The assertion maps generated by the invariant propagation algorithm is inductive.

Proof. We prove by an induction on the number 𝑘 of locations in the input ATS Γ that the assertion map obtained by our invariant propagation algorithm for the ATS Γ is inductive.

We firstly consider the base case, i.e., 𝑘 = 1. In this case, 𝐷𝐺 (Γ) has only one location, which is obviously indivisible. Here, the function InitInv(), previously mentioned as applying Farkas' Lemma for conjunctive invariant computation, is called. Therefore, the resulting assertion map is inductive, and its correctness is guaranteed by the prior results.

Assuming that the case when the size of Γ equals 𝑘 holds, we prove that it holds for Γ of size 𝑘 + 1. For an ATS Γ with 𝑘 + 1 locations, if it is divisible, it can be decomposed into several sub-SCCs Γ 𝑠𝑢𝑏 with sizes less than or equal to 𝑘. After the call to function InvProp() at Line 8, we obtain an inductive assertion mapping by the inductive condition. The Merge() function does not affect the inductive condition of the combined mapping. On the other hand, if it is indivisible, then our approach computes the invariant at its initial location and, after projecting away the initial location ℓ * , obtains a sub-ATS Γ 𝑠𝑢𝑏 of size 𝑘. Similarly, the recursive call to invariant propagation at Line 20 and merging the returned results always yields an inductive assertion map by the inductive condition. □

Other Optimizations

In this section, we consider further optimizations. The first is the tackling of infeasible implications (i.e., "-1 ≥ 0") in the application of Farkas' Lemma. This situation has not been handled in the previous approaches in Farkas' Lemma. The infeasible implication is important in the generation of disjunctive invariants since ignoring them would break the internal disjunctive feature of the loop, thus leading to the failure of the generation of the desired disjunctive invariant. A key difficulty to tackle the infeasible implication is that we obtain general polyhedra rather than polyhedral cones in establishing the constraints for invariant generation, and thus cannot directly apply the generator computation over polyhedral cones. To address this difficulty, we show that it suffices to fix the nonlinear parameter 𝜇 multiplied to the template in the Farkas tabular (Figure 1c) to 1 and include the generators of both the polytope and the polyhedral cone of the Minkowski decomposition of the polyhedron resulting from the constraint solving of the PAP after the application of Farkas' Lemma.

As its correctness proof is somewhat technical, we relegate them to Appendix B and Appendix C. The second is the extension of our approach to nested loop. The main difficulty here is how to handle the inner loops in a nested loop. Recall that in the previous section, we transform a non-nested loop into a canonical form and further transforms it into an affine transition system. This cannot be applied to nested loops since the inner loops does not obey this canonical form.

To address this difficulty, we consider to use the standard technique of loop summary to abstract the input-output relationship of the inner loops, and use the loop summaries of inner loops to construct the overall affine transition system for the outer loops.

Given a nested affine while loop 𝑊 , our approach works by first recursively computing the loop summary 𝑆 𝑊 ′ for each inner while loop 𝑊 ′ in 𝑊 (from the innermost to the outermost), and then tackling the main loop body via the control flow of the loop body and the loop summaries 𝑆 𝑊 ′ of the inner loops. Below we fix a nested affine while loop 𝑊 with variable set 𝑋 = {𝑥 1 , . . . , 𝑥 𝑛 } and present the technical details.

The most involved part in our approach is the transformation of the main loop 𝑊 into its corresponding ATS. To address the inner loops, our algorithm works with the control flow graph (CFG) 𝐻 of the loop body of the loop 𝑊 and considers the execution paths in this CFG. The CFG 𝐻 is a directed graph whose vertices are the program counters of the loop body and whose edges describe the one-step jumps between these program counters. Except for the standard semantics of the jumps emitting from assignment statements and conditional branches, for a program counter that represents the entry point of an inner while loop that is not nested in other inner loops, we have the special treatment that the jump at the program counter is directed to the termination program counter of this inner loop in the loop body of 𝑊 (i.e., skipping the execution of this inner loop). An execution path in the CFG 𝐻 is a directed path of program counters that ends in (i) either the termination program counter of the loop body of 𝑊 without visiting a program counter that represents the break statement or (ii) a first break statement without visiting prior break statements. An example is as follows.

Example 6. Consider the janne_complex program from [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF] in Figure 6. The CFG of the program is given in Figure 7 where the nodes correspond to the program counters, the directed edges with guards specifies the jumps and their conditions, and the affine assignments are given in the program counters 𝐴 1 , 𝐴 2 , 𝐴 3 . while ( 𝑥 < 30 ) { while (𝑦 < 𝑥 ) { i f (𝑦 > 5 ) 𝑦 = 𝑦 * 3 ; e l s e 𝑦 = 𝑦 + 2 ; i f ( y >= 10 && y < = 1 2 ) 𝑥 = 𝑥 + 10 ; e l s e 𝑥 = 𝑥 + 1 ; } 𝑥 = 𝑥 + 2 ; 𝑦 = 𝑦 -10 ; } We denote by 𝑊 the outer loop with entry point 𝐸 Outer , and by 𝑊 ′ the inner loop with entry point 𝐸 inner . The execution path starts at the Initial Condition [𝑥, 𝑦], jumps to the next vertices along the edge whose condition is satisfied (e.g., True is tautology, 𝑥 < 30 is satisfied when variable 𝑥 value is less than 30, etc.), and terminates in the Exit statement. The only execution path for the loop body of 𝑊 is 𝐴 𝐼𝑆 → 𝐴 1 , for which we abstract the whole inner loop by 𝐴 𝐼𝑆 . □

Based on the CFG 𝐻 and the execution paths, our approach constructs the ATS for the outer loop 𝑊 as follows. Since the output of an inner while loop 𝑊 ′ in 𝑊 cannot be exactly determined from the input to the loop 𝑊 ′ , we first have fresh output variables 𝑥 𝑊 ′ ,1 , . . . , 𝑥 𝑊 ′ ,𝑛 ′ to represent the output values of the variables 𝑥 𝑊 ′ ,1 , . . . , 𝑥 𝑊 ′ ,𝑛 ′ after the execution of the inner loop 𝑊 ′ . These output variables are used to express the loop summaries of these inner loops.

Then, to get the numerical information from execution paths, we symbolically compute the values of the program variables at each program counter in an execution path. In detail, given an execution path 𝜔 = 𝜄 1 , . . . , 𝜄 𝑘 where each 𝜄 𝑖 is a program counter of the loop body of the loop 𝑊 , our approach computes the affine expressions 𝛼 𝑥,𝑖 and PAPs 𝛽 𝑖 (for 𝑥 ∈ 𝑋 and 1 ≤ 𝑖 ≤ 𝑘) over the program variables in 𝑋 (for which they represent their initial values at the start of the loop body of 𝑊 here) and the fresh output variables. The intuition is that (i) each affine expression 𝛼 𝑥,𝑖 represents the value of the variable 𝑥 at the program counter 𝜄 𝑖 along the execution path 𝜔 and (ii) each PAP 𝛽 𝑖 specifies the condition that the program counter 𝜄 𝑖 is reached along the execution path 𝜔. The computation is recursive on 𝑖 as follows.

Denote the vectors 𝛼 𝑖 := (𝛼 𝑥 1 ,𝑖 , . . . , 𝛼 𝑥 𝑛 ,𝑖 ) and 𝑥 𝑊 ′ = (𝑥 𝑊 ′ ,1 , . . . , 𝑥 𝑊 ′ ,𝑛 ′ ). For the base case when 𝑖 = 1, we have 𝛼 1 = (𝑥 1 , . . . , 𝑥 𝑛 ) and 𝛽 1 = true that specifies the initial setting at the start program counter 𝜄 1 of the loop body of the original loop 𝑊 . For the recursive case, suppose that our approach has computed the affine expressions in 𝛼 𝑖 and the PAP 𝛽 𝑖 . We classify four cases below:

•

𝛼 1 = [𝑥, 𝑦 ], 𝛽 1 = true 𝑥 < 30 ----→ 𝛼 2 = [𝑥, 𝑦 ], 𝛽 2 = 𝛽 1 ∧ 𝑥 < 30 𝐴 𝐼 𝑆 --→ 𝛼 3 = [𝑥 𝑊 ′ , 𝑦 𝑊 ′ ], 𝛽 3 = 𝛽 2 ∧ 𝑆 𝑊 ′ (𝛼 2 , 𝛼 3 ) 𝐴 1 -→ 𝛼 4 = [𝑥 𝑊 ′ + 2, 𝑦 𝑊 ′ -10], 𝛽 4 = 𝛽 3
Fig. 8. The evolution of 𝛼 𝑖 and 𝛽 𝑖 for the execution path of 𝑊 in Figure 7 initial setting 𝛼 1 = [𝑥, 𝑦], 𝛽 1 = true is given in Figure 8. □ After the 𝛼 𝑖 , 𝛽 𝑖 's are obtained for an execution path 𝜔 = 𝜄 1 , . . . , 𝜄 𝑘 from the recursive computation above, we let the PAP Ψ 𝜔 := 𝑖 ∈𝐼 𝛽 𝑖 where the index set 𝐼 is the set of all 1 ≤ 𝑖 ≤ 𝑘 such that the program counter 𝜄 𝑖 corresponds to either a conditional branch or the entry point of an inner while loop, and the vector of affine expression 𝛼 𝜔 := 𝛼 𝑘+1 . Note that the PAP Ψ 𝜔 is the condition that the execution of the loop body follows the execution path 𝜔, and the affine expressions in the vector 𝛼 𝜔 represent the values of the program variables after the execution path 𝜔 of the loop body of 𝑊 in terms of the initial values of the program variables and the fresh variables for the output of the inner while loops in 𝑊 .

Finally, our approach constructs the ATS for the loop 𝑊 and we only present the main points:

• First, for each execution path 𝜔 of the loop body of 𝑊 , we have a standalone location ℓ 𝜔 for this execution path. Recall that we abstract the inner loops, so that the execution paths can be finitely enumerated. • Second, for all locations ℓ 𝜔 , ℓ 𝜔 ′ (from the execution paths 𝜔, 𝜔 ′ ), we have the transition

𝜏 𝜔,𝜔 ′ := (ℓ 𝜔 , ℓ 𝜔 ′ , Ψ 𝜔 ∧ Ψ ′ 𝜔 ′ ∧ x ′ = 𝛼 𝜔 )
which means that if the execution path in the current iteration of the loop 𝑊 is 𝜔, then in the next iteration the execution path can be 𝜔 ′ with the guard condition Ψ 𝜔 ∧ Ψ ′ 𝜔 ′ ∧ x ′ = 𝛼 𝜔 that comprises the conditions for the execution paths 𝜔, 𝜔 ′ and the condition x ′ = 𝛼 𝜔 for the next values of the program variables.

• Third, we enumerate all possible initial locations 𝑙 𝜔 , along with their corresponding initial conditions 𝜃 = 𝐺 ∧ Ψ 𝜔 . To derive loop summary, we follow the standard technique (see e.g. [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF]) to include the input variables 𝑋 in and conjunct the affine assertion 𝑥 ∈𝑋 𝑥 = 𝑥 in into each disjunctive clause of the initial condition 𝜃 . Manually specified initial conditions can also be conjuncted into 𝜃 .

A detailed process that handles break statement is similar to the unnested situation. Again, we can remove invalid transitions by checking whether their guard condition is satisfiable or not.

At the end of the illustration of our algorithms, we discuss possible extensions as follows.

Remark 1 (Extensions). Our approach can be extended in the following ways. To obtain a more precise branch condition representation, one extension is by (i) distinguishing the remainders (e.g., even/odd) modulo a fixed positive integer (e.g. 2) when handling modular arithmetics and (ii) detecting hidden termination phases via the approach in [Ben-Amram and Genaim 2017]. To handle machine integers, another extension is by having a piecewise disjunctive treatment for the cases of overflow and non-overflow. Finally, our approach could be extended to floating point numbers by considering piecewise affine approximations [START_REF] Miné | Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors[END_REF][START_REF] Miné | Symbolic Methods to Enhance the Precision of Numerical Abstract Domains[END_REF].

EXPERIMENTAL EVALUATION

In this section, we present the evaluation of the implementation (referred to as DInvG) of our approach to generate disjunctive affine invariants. We focus on the following two questions (RQ1 and RQ2).

• RQ1: How competitive is DInvG when compared with other approaches?

• RQ2: How effective does invariant propagation enhance our approach?

Experimental Setup

Implementation. We implement our approach (including the algorithmic techniques in Section 4) as a prototype tool based on the Clang Static Analyzer [Clang Static Analyzer 2022]. The implementation includes a front-end for converting C programs into affine transition systems as described in Section 4.1. The front-end first transforms affine loops into the canonical form as shown in Figure 5, and then converts them into the affine transition systems required by the back-end. We also implement the summary approach in Section 4.3. The back-end DInvG is an extension of StInG [START_REF] Sting | StInG: Stanford Invariant Generator[END_REF]] written in C++ and uses PPL 1.2 [START_REF] Bagnara | Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library[END_REF] for polyhedra manipulation (e.g., projection, generator computation, etc.). The back-end generates invariants at the initial location of (sub-)SCCs by the origianl tool StInG and implements invariant propagation method to propagate invariants to other locations. Moreover, the back-end implements the tackling of infeasible implication in the application of Farkas' Lemma and loop summary as described in Section 4.3.

Environment. All experiments are conducted on a machine equipped with a 12th Gen Intel(R) Core(TM) i7-12800HX CPU, 16 cores, 2304 MHz, 9.5GB RAM, running Ubuntu 20.04 (LTS). Following the competition settings of SV-COMP, for studies RQ1 and RQ2, we impose a time limit of 900s.

Benchamarks. We found a total of 114 benchmarks of affine programs, including those with/without disjunctive feature, sourced from: 1) 105 benchmarks from the SV-COMP, ReachSafety-Loop track. We excluded those with arrays, pointers, and other non-numeric features, those with modulus, division, polynomial, and other non-linear operations, and those with complex control flows involving goto statements (as goto will disrupt the regular loop features, making it more difficult for the front-end to extract the transition system). 2) 9 benchmarks from the recent paper [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF], which include complex nested loops and examples with disjunctive features.

Methodology. In RQ1, we compare DInvG utilizing invariant propagation techniques with several state-of-the-art software verifiers, including Veriabs [START_REF] Darke | VeriAbs: A tool for scalable verification by abstraction (competition contribution)[END_REF] (the winner in the reachsafety track of SV-COMP 2023), the well-developed CPAChecker [CPAchecker 2022], and a recent tool from [START_REF] Wang | Solving Conditional Linear Recurrences for Program Verification: The Periodic Case[END_REF].

CPAChecker [START_REF] Cpachecker | CPAchecker: The Configurable Software-Verification Platform[END_REF]] is a well-developed software verifier that is based on bounded model checking and interpolation and has a comprehensive ability to verify various kinds of properties.

Veriabs [START_REF] Darke | VeriAbs: A tool for scalable verification by abstraction (competition contribution)[END_REF]] is a state-of-the-art software verifier that is an integration of various strategies such as fuzz testing, 𝑘-induction, loop shrinking, loop pruning, full-program induction, explicit state model checking and other invariant generation techniques.

OOPSLA23 [START_REF] Wang | Solving Conditional Linear Recurrences for Program Verification: The Periodic Case[END_REF]] is a recent recurrence analysis tool that handles only loops with the ultimate strict alternation pattern that eventually the loop will alternate between different modes periodically and performs good on such class of programs.

In RQ2, we focus on comparing the impact of the invariant propagation technique on the time efficiency. By contrasting the tool's performance when calculating invariants for each location individually against using invariant propagation on SV-COMP benchmarks, we analyze the role of invariant propagation.

Tool Comparison (RQ1)

Our work primarily focuses on the generation of disjunctive invariants, whereas tools like CPAChecker and Veriabs are specifically designed as bug finders for verifying assertions. However, by integrating the PPL library [START_REF] Bagnara | Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library[END_REF] and Z3 [Z3 2023], we use the generated invariants to verify the correctness of assertions. In the SV-COMP examples in affine invariant generation, our approach shows performance advantage when compared with these specialized assertion-checking verification tools. The complete comparison results of DInvG with other tools are presented in Table 1. In the table, Source indicates the source category of the benchmark. The term #Ver. represents the number of examples that were correctly verified by the verifier, and #Unk. (unknown) mainly arises from the following situations: a) The front-end fails to parse correctly, resulting in program crashes. b) Returns Unknown. c) Timeouts. For the benchmarks from [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF], which do not contain assertions to be verified, we set the invariants generated by our DInvG as assertions and test them over the other three tools to obtain results.

From the table, it is evident that DInvG typically requires less than 0.2 seconds averagely for verification, and its overall verification accuracy is very close to that of the SV-COMP winner Veriabs, significantly outperforming Veriabs in terms of time efficiency by 10X to 1000X. This is mainly because Veriabs employs a rich strategy to assist verification, granting it a stronger verification capability but also requiring more time for most examples. Despite that the tool from [START_REF] Wang | Solving Conditional Linear Recurrences for Program Verification: The Periodic Case[END_REF] having the fewest number of verified benchmarks, it outperforms CPAChecker and Veriabs in examples suitable for recurrence analysis. CPAChecker, as the most widely used and comprehensive bounded model checking and interpolation tool, experienced a broad range of timeouts in examples with complex loops that could not be verified within a finite unfolding of loops.

In summary, we conclude that DInvG significantly outperforms other tools such as Veriabs in time efficiency for affine numerical programs, while its verification capability is not inferior to the SV-COMP winner Veriabs. We also conducted an in-depth analysis of the ten cases where our DInvG returns Unknown. Some failures were due to type range constraints not yet implemented in the front-end (2 cases), or more complex property strengthening techniques were required, such as setting the generated invariant as a precondition and iteratively calculating the entire loop's invariant (1 case), dependency on modular arithmetic or dividing program variables into different modulus situations (3 cases), and cases requiring more complex loop generalization (2 cases), exceeding the computational range of the backend PPL library (1 case), and seemingly linear arithmetic but actually exponential iterative calculations (1 case). 7-8 of these cases could be further solved by optimizing the frontend and backend implementations. In the verifiable cases, the preliminary implementation of DInvG has already far surpassed existing methods in efficiency.

Remark 2 (Other Related Approaches). We are unable to have direct comparison with the very related work [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF]; [START_REF] Henry | PAGAI: A Path Sensitive Static Analyser[END_REF]; [START_REF] Lin | Inferring Loop Invariants for Multi-Path Loops[END_REF]; [START_REF] Riley | Multi-Phase Invariant Synthesis[END_REF]; [START_REF] Xie | Proteus: computing disjunctive loop summary via path dependency analysis[END_REF] due to the following reasons. First, the works [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF]; [START_REF] Lin | Inferring Loop Invariants for Multi-Path Loops[END_REF]; [START_REF] Xie | Proteus: computing disjunctive loop summary via path dependency analysis[END_REF] neither publicize their implementation nor report the detailed invariants in some key benchmarks. Second, although the tool PAGAI [START_REF] Henry | PAGAI: A Path Sensitive Static Analyser[END_REF] claims the functionality of disjunctive invariant generation, we find that this functionality could not work in the disjunctive-invariant-generation mode. Third, the tool in Riley and Fedyukovich [2022] accepts only the smtlib format of the CHC solver and has a preprocessing on the original CHC input, making the recovery of the original loop information difficult. We have tried the submodules of SeaHorn [SeaHorn 2015] and Eldarica [START_REF] Eldarica | Eldarica: A model checker for Horn clauses[END_REF]] to transform several examples with simple control flow from the literature into their CHC format, but this tool does not terminate on the CHC inputs of these simple examples. We also note that machine learning approaches [Ryan et al. 2020;[START_REF] Si | Learning Loop Invariants for Program Verification[END_REF][START_REF] Yao | Learning nonlinear loop invariants with gated continuous logic networks[END_REF]] could also generate disjunctive invariants, but we found robustness problem that a slight deviation in a simple program (without changing the branch structure in the loop) can cause these approaches non-terminating. Our approach is based on constraint solving and therefore does not have this robustness issue. □

Comparison in Invariant Propagation (RQ2)

In this section, we compare the performance of DInvG with and without invariant propagation on the aforementioned benchmarks. In Table 2, we present the overall results, where we can clearly observe that the use of invariant propagation leads to a 5X-50X improvement in time efficiency. More specifically, through the scatter plot in Figure 9, we compared the time performance of individual examples before and after the application of invariant propagation techniques. In some cases, invariant propagation led to significant efficiency improvements (10X-1000X). This is due to the fact that for more complex programs, the size of the ATS Γ is larger, and applying invariant propagation techniques on this basis can maximize performance optimization. However, since the tool itself performs efficiently in most examples, the optimization brought by this technique is not apparent in those cases in the graph where the time is below 0.1 seconds. This is because the propagation itself, including the projection of sub-ATS, incurs a certain time cost, which dilutes the time optimization brought about by invariant propagation.

In conclusion, we can summarize that the invariant propagation technique significantly enhances the tool's scalability and yields better optimization results for relatively complex examples.

RELATED WORKS

Below we compare our approach with the most related approaches in the literature. We first have the comparison with the constraint-solving approaches.

• Our approach uses the framework to apply Farkas' Lemma as proposed in [START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF]; [START_REF] Liu | Scalable Linear Invariant Generation with Farkas' Lemma[END_REF]; Sankaranarayanan et al. [2004b] and extend the framework to disjunctive affine invariants, for which our basic contribution is the construction of an affine transition system that utilizes the disjunctive feature from the conditional branches in a loop. Furthermore, we propose invariant propagation to improve the time efficiency, the tackling of infeasible implications in the application of Farkas' Lemma to improve the accuracy, and the use of loop summary to handle nested loops. The recent result [START_REF] Ji | Affine Loop Invariant Generation via Matrix Algebra[END_REF]] also considers Farkas' Lemma, but focuses on conjunctive affine invariants over non-nested affine while loops via the use of eigenvalues and roots of polynomial equations, and hence is orthogonal to our approach. Besides, other approaches on affine invariant 10 2 10 1 10 0 10 1 10 2 10 3 Time of InvProp (s) [2017]; [START_REF] Gulwani | Program analysis as constraint solving[END_REF]; [START_REF] Gupta | InvGen: An Efficient Invariant Generator[END_REF]. The approach [START_REF] Gulwani | Program analysis as constraint solving[END_REF]] solves the quadratic constraints derived from Farkas' Lemma by SAT solvers and bit-vector modeling. The approach [START_REF] Steven De Oliveira | Synthesizing Invariants by Solving Solvable Loops[END_REF]] uses eigenvectors to handle several restricted classes of conjunctive affine invariants.

The tool InvGEN [START_REF] Gupta | InvGen: An Efficient Invariant Generator[END_REF] generates conjunctive affine invariants by an integrated use of abstract interpretation and Farkas' Lemma. These approaches propose completely different techniques, and thus are orthogonal to our approach. • Since our approach targets affine invariant generation, it is incomparable with previous results on polynomial invariant generation [START_REF] Adjé | Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization[END_REF][START_REF] Chatterjee | Polynomial invariant generation for non-deterministic recursive programs[END_REF][START_REF] Chen | Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation[END_REF][START_REF] Cousot | Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming[END_REF]de Oliveira et al. 2016;[START_REF] Hrushovski | Polynomial Invariants for Affine Programs[END_REF][START_REF] Humenberger | Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences[END_REF][START_REF] Kapur | Automatically Generating Loop Invariants Using Quantifier Elimination[END_REF][START_REF] Lin | Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods[END_REF]Rodríguez-Carbonell and Kapur 2004b;Sankaranarayanan et al. 2004a;[START_REF] Yang | Recent advances in program verification through computer algebra[END_REF]. Moreover, most of these approaches consider conjunctive polynomial invariants, and hence do not consider disjunction. It is also worth noting that the previous work [START_REF] Sharma | Simplifying Loop Invariant Generation Using Splitter Predicates[END_REF] proposes a general framework for detecting multiphase disjunctive invariants that can be instantiated with constraint solving. Multiphase disjunctive invariants are a restricted case of our transformation into affine transition systems in the sense that each phase in a multiphase feature cannot go back to previous phases, while in an affine transition system, locations can go back and forth via transitions. Therefore, we consider a wider class of disjunctive invariants as compared with [START_REF] Sharma | Simplifying Loop Invariant Generation Using Splitter Predicates[END_REF].

Second, we compare our approach with the results [START_REF] Lin | Inferring Loop Invariants for Multi-Path Loops[END_REF][START_REF] Xie | Proteus: computing disjunctive loop summary via path dependency analysis[END_REF]] that consider a similar disjunctive pattern to ours. These approaches propose path dependency automata that consider different execution paths of the loop body w.r.t whether each conditional branch in the loop body is entered or not, treat each execution path as a standalone mode, and have transitions between these modes. However, an indispensible ingredient of path dependency automata is the exact estimation of the number of loop iterations sojourning in each mode, and hence is limited to inductive variables (i.e., assignments must be in the form 𝑥 := 𝑥 +𝑐 or 𝑥 := 𝑐 * 𝑥) and strict alternation between different modes. Our approach constructs affine transition systems between different locations derives from the conditional branches, and hence do not have such limitation. Moreover, we extend our approach to handle nested loops via loop summary, while these approaches could not have an adequate support for nested loops.

Third, we compare our control flow transformation with the related notion of control flow refinement [START_REF] Balakrishnan | Refining the control structure of loops using static analysis[END_REF][START_REF] Cyphert | Refinement of path expressions for static analysis[END_REF][START_REF] Gulwani | Control-flow refinement and progress invariants for bound analysis[END_REF][START_REF] Silverman | Loop Summarization with Rational Vector Addition Systems[END_REF] in the literature. These approaches mostly focus on representing the control flow of multiple loop iterations as regular expressions and refine these regular expressions by various approaches such as abstract domains, simulation relation and even invariant generation to reduce infeasible paths. Our control flow transformation considers the loop body within a single loop iteration, and is dedicated to the application of Farkas' Lemma. Thus, our control flow transformation has a different focus compared with these results.

Fourth, we compare our approach with abstract interpretation. Compared with the approaches that generate conjunctive affine invariants via polyhedral abstract domain [START_REF] Bagnara | Precise Widening Operators for Convex Polyhedra[END_REF][START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF][START_REF] Singh | Fast polyhedra abstract domain[END_REF], our approach targets the more general case of disjunctive affine invariants. There are also a bunch of abstract interpretation approaches in disjunctive affine invariant generation, such as the work [START_REF] Gopan | Guided Static Analysis[END_REF] that performs disjunctive partitioning by representing the contribution of each iteration with a separate abstractdomain element, the recent work [START_REF] Boutonnet | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis[END_REF] that distinguishes different disjunctive cases by different entries into the conditional branches w.r.t the input values, and the state-of-the-art tool PAGAI [START_REF] Henry | PAGAI: A Path Sensitive Static Analyser[END_REF]] that may infer disjunctive invariants as disjunctions of elements of the abstract domain via specific iteration algorithm. These approaches are based on abstract interpretation and heuristics different from our disjunctive pattern and techniques, and hence are orthogonal to our approach. It is worth noting that although our invariant propagation has a similar propagation process as abstract interpretation does, they are actually different as abstract interpretation usually requires a repeated iteration until a fixed point is reached, while our invariant propagation does not have such a fixed point computation.

Fifth, we compare our approach with recurrence analysis [START_REF] Farzan | Compositional Recurrence Analysis[END_REF][START_REF] Kincaid | Compositional recurrence analysis revisited[END_REF][START_REF] Kincaid | Non-linear reasoning for invariant synthesis[END_REF]. Recurrence analysis works well over programs with specific structure that ensures closed form solutions. For example, the most related recurrence analysis approach [START_REF] Wang | Solving Conditional Linear Recurrences for Program Verification: The Periodic Case[END_REF] (that also targets disjunctive invariants) solves the exact invariant over the class of loops with (ultimate) strict alternation between different modes. Compared with recurrence analysis, our approach does not require specific program structure to ensure closed form solution, but is less precise over programs that can be solved exactly by recurrence analysis.

Finally, we compare our approach with other methods such as machine learning, inference and data-driven approaches. Unlike constraint solving that can have an accuracy guarantee for the generated invariants based on the constraints, these methods cannot have an accuracy guarantee. Furthermore, machine learning and data-driven approaches themselves cannot guarantee that the generated assertions are indeed invariants. Moreover, our approach can generate invariants without the need of a goal property, while these approaches usually requires a goal property. Note that the invariant generation without a given goal property is a classical setting (see e.g. [START_REF] Michael Colón | Linear Invariant Generation Using Non-linear Constraint Solving[END_REF]; [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF]), and has applications in loop summary and probabilistic program verification (see e.g. [START_REF] Chakarov | Probabilistic Program Analysis with Martingales[END_REF]; [START_REF] Wang | Quantitative analysis of assertion violations in probabilistic programs[END_REF]).

CONCLUSION AND FUTURE WORK

In this work, we have proposed a novel approach to generate affine disjunctive invariants over affine loops via Farkas' Lemma. We first established the transformation from an affine while loop into an equivalent affine transitions system so that existing aprpoaches in Farkas' Lemma can apply. Then we developed optimizations including invariant propagation to improve time efficiency, the tackling of infeasible implications to improve accuracy and the use of loop summary to extend our approach to nested loops. Experimental results show that our approach is competitive with state-of-the-art software verifiers on affine disjunctive invariant generation over affine loops.

One future direction would be to consider extensions of our approach to have linear representations to handle properties in machine integers (such as distinguishing the case of integer overflow and different cases of remainder in handling the modulus information) and floating point numbers (see Remark 1). Another direction is to extend our approach to procedure summary.

A PROCESS OF TRANSFORMATION TO CANONICAL FORM

Here, we provide a detailed demonstration of how to transform the loop body 𝑃 of a non-nested affine program into its canonical form: • For the base case where the program 𝑃 is either a single affine assignment x := F(x) or resp. the break statement, the transformed program C 𝑃 is simply switch {case true : x := F(x); skip; } or resp. switch {case true : x := x; break; }, respectively. • For a sequential composition 𝑅 = 𝑃; 𝑄, the algorithm recursively computes C 𝑃 and C 𝑄 as in Figure 10a and Figure 10b respectively, and then compute C 𝑅 as in Figure 10c for which:

:= F 𝑄,1 (x) ; 𝛿 𝑄,1 ; • • • c a s e 𝜙 𝑄,𝑞 : x := F 𝑄,𝑞 (x) ; 𝛿 𝑄,𝑞 ; } (b) C 𝑄 switch { • • • c a s e 𝜙 𝑃,𝑖 : x := (F 𝑃,𝑖 (x)) ; 𝑏𝑟𝑒𝑎𝑘 ; ( if 𝛿 𝑃,𝑖 = break ) • • • c a s e 𝜙 𝑃,𝑖 ∧ 𝜙 𝑄,𝑗 [F 𝑃,𝑖 (x)/x] : x := F 𝑄,𝑗 (F 𝑃,𝑖 (x)) ; 𝛿 𝑄,𝑗 ; ( if 𝛿 𝑃,𝑖 = skip ) • • • } (c) The sequential case switch { • • • c a s e 𝜙 𝑃,𝑖 ∧ 𝑏 : x := F 𝑃,𝑖 (x) ; 𝛿 𝑃,𝑖 ; • • • c a s e 𝜙 𝑄,𝑗 ∧ ¬𝑏 : x := F 𝑄,𝑗 (x) ; 𝛿 𝑄,𝑗 ; • • • } (d) The conditional case
-For each 1 ≤ 𝑖 ≤ 𝑝 such that 𝛿 𝑃,𝑖 = break, we have the branch x := F 𝑃,𝑖 (x); break; (i.e., the branch already breaks in the execution of 𝑃). -For each 1 ≤ 𝑖 ≤ 𝑝 and 1 ≤ 𝑗 ≤ 𝑞 such that 𝛿 𝑃,𝑖 = skip, we have the branch

x := F 𝑄,𝑗 (F 𝑃,𝑖 (x)); 𝛿 𝑄,𝑗 under the branch condition 𝜙 𝑃,𝑖 ∧ (𝜙 𝑄,𝑗 [F 𝑃,𝑖 (x)/x]) (i.e., the branch continues to the execution of 𝑄). • For a conditional branch 𝑅 = if 𝑏 then 𝑃 else 𝑄, the algorithm recursively computes C 𝑃 and C 𝑄 as in the previous case, and then compute C 𝑅 as in Figure 10d for which:

-For each 1 ≤ 𝑖 ≤ 𝑝, we have the branch x = F 𝑃,𝑖 (x); 𝛿 𝑃,𝑖 ; with branch condition 𝜙 𝑃,𝑖 ∧ 𝑏 (i.e., the branch conditions of 𝑃 is conjuncted with the extra condition 𝑏). -For each 1 ≤ 𝑗 ≤ 𝑞, we have the branch x = F 𝑄,𝑗 (x); 𝛿 𝑄,𝑗 ; with branch condition 𝜙 𝑄,𝑗 ∧ ¬𝑏 (i.e., the branch conditions of 𝑄 is conjuncted with the extra condition ¬𝑏).

B PROOF OF NO ACCURACY LOSS FOR 𝜇=1

To prove that there is no accuracy loss while setting 𝜇 manually to 1, for convenience, we denote the consecution tabular with -1 ≥ 0 as constraint consecution tabular and the consecution tabular without -1 ≥ 0 as transition consecution tabular. Then we prove that constraint consecution tabular is equivalent whether 𝜇 = 1 or 𝜇 = 𝑘, ∀𝑘 > 0.

We scale the leftmost coefficient column 𝑘, 𝜆 𝑖 's to be 1, 𝜆 ′ 𝑖 's by multiplying 1 𝑘 , where 𝜆 ′ 𝑖 = 𝜆 𝑖 𝑘 . The coefficient of invariants after transformation is the same as the previous tabular.

Consider all the constraint consecution tabular and choose the maximum 𝑘 𝑚𝑎𝑥 of their 𝑘's. Then, we scale 𝜆 𝑖 's, 𝑐 𝑙,𝑖 's and 𝑑 ℓ by 𝑘 𝑚𝑎𝑥 and modify 𝜆 ′ 0 to be 𝜆 ′′ 0 = 𝜆 ′ 0 + 𝑘 𝑚𝑎𝑥 𝑘 -1. Note that it's necessary to select the fixed 𝑘 𝑚𝑎𝑥 to scale 𝑐 𝑙,𝑖 's, so that we avoid affecting the solution in the transition consecution tabular as transition consecution tabular is always satisfied if we multiply 𝑐 with fixed constant 𝑘 𝑚𝑎𝑥 .

Thus we prove there is no accuracy loss as we set 𝜇 = 1 by means of coefficient scaling.

C PROOF OF CORRECTNESS OF SOLUTIONS TO INVARIANT SETS IN THE IMPLEMENTATION PART

In the implementation, we utilize decomposition theorem of polyhedra and decompose the solution set of invariant when 𝜇 = 1 to be a polytope 𝑃 and a polyhedral cone 𝐶. Similarly, we denote 𝐹 as the solution set of invariants, which contains the coefficient of invariants at any locations and 𝐹 ′ as the solution set of invariants when 𝜇 = 1 in all the consecution tabular. Then the union of the polytope and polyhedral cone is chosen as our solution set of invariants 𝐹 * = 𝑃 ∪ 𝐶, where 𝐹 ′ = 𝑃 + 𝐶.

Lemma 1. Decomposition theorem of polyhedra. A set 𝑃 of vectors in Euclidean space is a polyhedron if and only if 𝑃 = 𝑄 + 𝐶 for some polytope 𝑄 and some polyhedral cone 𝐶.

  Fig. 3. Example of a clause in the DNF with its generators and invariants

Fig. 4 .

 4 Fig. 4. Process of Invariant Propagation

Fig. 6 .

 6 Fig. 6. The janne_complex program

Fig. 7 .

 7 Fig. 7. The CFG of janne_complex [Boutonnet and Halbwachs 2019]

  Case 1: The program counter 𝜄 𝑖 is an affine assignment statement x := F(x). Then we have that 𝛼 𝑖+1 = 𝛼 𝑖 [F(x)/x] and 𝛽 𝑖+1 := 𝛽 𝑖 . • Case 2: The program counter 𝜄 𝑖 is a conditional branch with branch condition 𝑏 and the next program counter 𝜄 𝑖+1 follows its then-branch. Then the vector 𝛼 𝑖+1 is the same as 𝛼 𝑖 , and the PAP 𝛽 𝑖+1 is obtained as 𝛽 𝑖+1 = 𝛽 𝑖 ∧ 𝑏. • Case 3: The program counter 𝜄 𝑖 is a conditional branch with branch condition 𝑏 and the next program counter 𝜄 𝑖+1 follows its else-branch. The only difference between this case and the previous case is that 𝛽 𝑖+1 is obtained as 𝛽 𝑖+1 := 𝛽 𝑖 ∧ ¬𝑏. • Case 4: The program counter 𝜄 𝑖 is the entry point of an inner while loop 𝑊 ′ of 𝑊 and 𝜄 𝑖+1 is the successor program counter outside 𝑊 ′ in the loop body of 𝑊 . Then 𝛼 𝑖+1 := 𝑥 𝑊 ′ and 𝛽 𝑖+1 := 𝑆 𝑊 ′ (𝛼 𝑖 , 𝑥 𝑊 ′ ). Here we use the ouput variables to express the loop summary. Note that the loop summary 𝑆 𝑊 ′ (see Page 5 for the definition of 𝑆) is recursively computed. Example 7. Continue with the execution path in Example 6. The evolution of 𝛼 𝑖 and 𝛽 𝑖 with the

Fig. 9 .

 9 Fig. 9. Comparison for Invariant Propagation

  switch { c a s e 𝜙 𝑃,1 : x := 𝐹 𝑃,1 (x) ; 𝛿 𝑃,1 ; • • • c a s e 𝜙 𝑃,𝑝 : x := 𝐹 𝑃,𝑝 (x) ; 𝛿 𝑃,𝑝 ; } (a) C 𝑃 switch { c a s e 𝜙 𝑄,1 : x

Fig. 10 .

 10 Fig. 10. The canonical form of transformation (TF) for 𝑃, 𝑄

  Fig. 14. The full janne_complex program after converted

  𝜂 = InitInv(Γ, ℓ * ) 18: Γ 𝑠 = Project(Γ, ℓ * ) 19: for each transition 𝜏 directed from ℓ * to ℓ 𝑡 do

	11:	stack.𝑝𝑢𝑠ℎ(nextNo, ℓ 𝑡 )
	12:	end for
	13:	𝜂 = Merge(𝜂, 𝜂 s )
	14:	end while
	15:	return 𝜂
	16: end if
	17: 20:

  𝑘 𝑐ℓ,1 𝑥 1 +• • •+ 𝑐 ℓ,𝑛 𝑥 𝑛 + 𝑑 ℓ ≥0 𝜆 0 1≥0 𝜆 1 𝑎 11 𝑥 1 +• • •+ 𝑎 1𝑛 𝑥 𝑛 + 𝑎 ′ 11 𝑥 ′ 1 +• • •+ 𝑎 ′ 1𝑛 𝑥 ′ 𝑛 + 𝑏 1 ≥0 . . . 𝑎 𝑚1 𝑥 1 +• • •+𝑎 𝑚𝑛 𝑥 𝑛 +𝑎 ′ Fig. 11. Constraint consecution tabular 1 𝑐 ℓ,1 𝑥 1 +• • •+ 𝑐 ℓ,𝑛 𝑥 𝑛 + 𝑑 ℓ ≥0 𝜆 ′ 𝑎 11 𝑥 1 +• • •+ 𝑎 1𝑛 𝑥 𝑛 + 𝑎 ′ 11 𝑥 ′ 1 +• • •+ 𝑎 ′ 1𝑛 𝑥 ′ 𝑛 + 𝑏 1 ≥0 . . . 𝑚 𝑎 𝑚1 𝑥 1 +• • •+𝑎 𝑚𝑛 𝑥 𝑛 +𝑎 ′ 𝑚1 𝑥 ′ 1 +• • •+𝑎 ′ 𝑚𝑛 𝑥 ′ 𝑛 +𝑏 𝑚 ≥0 -1 𝑘 ≥0 Fig. 12. Transformed constraint consecution tabular 1 𝑘 𝑚𝑎𝑥 • 𝑐 ℓ,1 𝑥 1 +• • •+𝑘 𝑚𝑎𝑥 • 𝑐 ℓ,𝑛 𝑥 𝑛 +𝑘 𝑚𝑎𝑥 • 𝑑 ℓ ≥0 𝜆 ′′

		. . .	. . .	. . .	. . .	. . .
		𝜆 𝑚 𝑚1 𝑥 ′ 1 +• • •+𝑎 ′ 𝑚𝑛 𝑥 ′ 𝑛 +𝑏 𝑚 ≥0
						-1≥0
			(a) 𝜇 = 𝑘, ∀𝑘 > 0
		0 𝜆 ′ 1 . . .	. . .	. . .	. . .	1≥0 . . .
		𝜆 ′
	0 𝜆 ′ 1	𝑎 11 𝑥 1 +• • •+	𝑎 1𝑛 𝑥 𝑛 + 𝑎 ′ 11 𝑥 ′ 1 +• • •+ 𝑎 ′ 1𝑛 𝑥 ′ 𝑛 +	1≥0 𝑏 1 ≥0
	. . .	. . .	. . .	. . .		. . .	. . .
	𝜆 ′ 𝑚	𝑎 𝑚1 𝑥 1 +• • •+	𝑎 𝑚𝑛 𝑥 𝑛 +𝑎 ′ 𝑚1 𝑥 ′ 1 +• • •+𝑎 ′ 𝑚𝑛 𝑥 ′ 𝑛 +	𝑏 𝑚 ≥0
							-1≥0
		Fig. 13. Equivalent constraint transformation tabular

ACKNOWLEDGMENTS

This material is based upon work supported by the National Science Foundation under Grant No. nnnnnnn and Grant No. mmmmmmm. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

Proof. We first consider 𝐹 ⊆ 𝐹 ′′ , which equivalent to prove ∀𝒄 ∈ 𝐹, ∃𝒄 0 ∈ 𝐹 ′ , 𝑘 ∈ 𝑅 such that 𝑘 • 𝒄 0 = 𝒄. We consider the transition consecution tabular. Note that, the consecution tabular is always satisfied if we scale the invariant 𝜂 (ℓ) and 𝜂 (ℓ ′ ) simultaneously.

Then consider the constraint consecution tabular. We have proved if we multiply 𝒄 0 ∈ 𝐹 ′ with 𝑘 𝑚𝑎𝑥 , we can find corresponding 𝒄 = 𝑘 𝑚𝑎𝑥 * 𝒄 0 is the solution to constraint consecution tabular with 𝜇 = 𝑘, ∀𝑘 > 0. (the definition of 𝑘 𝑚𝑎𝑥 and proof is given in Appendix A) Thus, we prove that ∀𝒄 ∈ 𝐹 , there exists 𝒄 0 ∈ 𝐹 ′ and 𝑘 𝑚𝑎𝑥 ∈ 𝑅 such that 𝑘 𝑚𝑎𝑥 * 𝒄 0 = 𝒄 and have 𝐹 ⊆ 𝐹 ′′ .

Secondly, we prove 𝐹 ′′ ⊆ 𝐹 . From the definition of 𝐹 ′′ , if 𝒄 ∈ 𝐹 ′ , we multiply 1 𝑘 to 𝜇 = 1 in the constraint consecution tabular, and 𝑘 • 𝒄 satisfy the transformed tabulars and other transition consecution tabulars. So 𝑘 • 𝒄 ∈ 𝐹 , and we have 𝐹 ′′ ⊆ 𝐹 .

So 𝐹 = 𝐹 ′′ . □

We utilize the decomposition theorem in 𝐹 ′ and have 𝐹 ′ = 𝑃 + 𝐶, where 𝑃 is a polytope and 𝐶 is a polyhedral cone. From the properties of polytope and polyhedral cone, a polytope is a convex hull of finitely many vectors and a polyhedral cone is finitely generated by some vectors.

(2) Note that the addition in the theorem means Minkowski sum, Thus,

Where 𝒑 𝒊 's represents the vectors finitely generate the polytope 𝑃 and 𝑔 𝑖 's represents the vectors finitely generate the polyhedral cone 𝐶. That means that ∀𝑣 ∈ 𝐹

where 𝑖 𝑎 𝑖 = 1 (from the definition of convex hull) and 𝑎 𝑖 , 𝑏 𝑖 ≥ 0, ∀𝑖.

, where 𝑎 ′ 𝑖 = 𝑘𝑎 𝑖 , 𝑘 > 0 and 𝑏 ′ 𝑖 = 𝑘𝑏 𝑖 , 𝑘 > 0. Thus, it's obvious that ∀𝒑 ∈ 𝑃, we have 𝒑 ∈ 𝐹 as we can set 𝒈 𝒊 = 0, ∀𝑖. However, we can not use the similar method to prove ∀𝒄 ∈ 𝐶, 𝒄 ∈ 𝐹 , as the 𝑖 𝑎 𝑖 equal to a non-zero number and 𝑎 𝑖 ≥ 0, ∀𝑖. So to prove the 𝑃 ∪𝐶 is also the solution set of invariants, we should consider the practical implications of invariant.

We have known that

Destruct 𝐹 to be

From the above conclusion, 𝑃 ⊆ 𝐹 , which means ∀𝒑 ∈ 𝑃, 𝒑 𝑇 𝒙 <= 𝑑 ℓ is satisfied. Also, ∀𝒗 ∈ 𝐹, 𝒗 = 𝒑 + 𝒄, 𝒑 ∈ 𝑃, 𝒄 ∈ 𝐶, and (𝒑 + 𝒄) 𝑇 𝒙 <= 𝑑 ℓ .

Consider ∀𝜀 > 0, we have (𝜀𝒑 + 𝒄) 𝑇 𝒙 <= 𝑑 ℓ . Thus, we finally conclude that lim 𝜀→0 (𝜀𝒑 + 𝒄) 𝑇 𝒙 = 𝒄 𝑇 𝒙 <= 𝑑 ℓ , which means for all 𝒄 ∈ 𝐶, 𝒄 is also a solution to invariants. Thus we prove 𝐶 ∈ 𝐹 , and 𝑃 ∪ 𝐶 ∈ 𝐹 . So it's correct to directly use the union of the polytope and the polyhedral cone to represents the solution set of invariants.