{'fraction_non_alphanumeric': 0.04295405234681827, 'fraction_numerical': 0.008211804125127021, 'mean_word_length': 4.346842878120412, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Formula Slicing: Inductive Invariants from Preconditions

We propose a"formula slicing"method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and many invariants which were valid before a loop are still valid after. Given a precondition of the loop, obtained from the preceding program fragment, we weaken it until it becomes inductive. The weakening procedure is guided by counterexamples-to-induction given by an SMT solver. Our algorithm applies to programs with arbitrary loop structure, and it computes the strongest invariant in an abstract domain of weakenings of preconditions. We call this algorithm"formula slicing", as it effectively performs"slicing"on formulas derived from symbolic execution. We evaluate our algorithm on the device driver benchmarks from the International Competition on Software Verification (SV-COMP), and we show that it is competitive with the state-of-the-art verification techniques.


Introduction
In automated program verification, one crucial task is establishing inductive invariants for loops: properties that hold initially, and also by induction for any number of execution steps.
Abstract-interpretation-based approaches restrict the class of expressible invariants to a predefined abstract domain, such as intervals, octagons, or convex polyhedra (all of which can only express convex properties). Any candidate invariants which can not be expressed in the chosen abstract domain get overapproximated. Traditionally, this restriction applies at all program locations, but approaches such as path focusing [1] limit the precision loss only to loop heads, representing program executions between the loop-heads precisely using first-order formulas. This is still a severe restriction: if a property flows from the beginning of the program to a loop head, and holds inductively after, but is not representable within the chosen abstract domain, it is discarded. In contrast, our idea exploits the insight that many loops in the program affect only a small part of the memory, and many invariants which were valid before the loop are still valid. int x = input(), p = input(); if (p) assume(x >= 0); else assume(x < 0); for (int i=0; i < input(); i++) x *= 2; Consider finding an inductive invariant for the motivating example in Fig. 1. Symbolic execution up to the loop-head can precisely express all reachable states: Yet abstraction in a numeric convex domain at the loop head yields i = 0, completely losing the information that x is positive iff p = 0. Observe that this information loss is not necessary, as the sign of x stays invariant under the multiplication by a positive constant (assuming mathematical integers for the simplicity of exposition). To avoid this loss of precision, we develop a "formula slicing" algorithm which computes inductive weakenings of propagated formulas, allowing to propagate the formulas representing inductive invariants across loop heads. In the motivating example, formula slicing computes an inductive weakening of the initial condition in Eq. 1), which is (p = 0 =⇒ x ≥ 0) ∧ (p = 0 =⇒ x < 0), and is thus true at every iteration of the loop. The computation of inductive weakenings is performed by iteratively filtering out conjuncts falsified by counterexamples-to-induction, derived using an SMT solver. In the motivating example, transition i = 1 from i = 0 falsifies the constraint i = 0, and the rest of the conjuncts are inductive. The formula slicing fixpoint computation algorithm is based on performing abstract interpretation on the lattice of conjunctions over a finite set of predicates. The computation starts with a seed invariant which necessarily holds at the given location on the first time the control reaches it, and during the computation it is iteratively weakened until inductiveness. The algorithm terminates within a polynomial number of SMT calls with the smallest invariant which can be expressed in the chosen lattice. Contributions We present a novel insight for generating inductive invariants, and a method for creating a lattice of weakenings from an arbitrary formula describing the loop precondition using a relaxed conjunctive normal form (Def. 2) and best-effort quantifier elimination (Sec. 4).
We evaluate (Sec. 7) our implementation of the formula slicing algorithm on the "Device Drivers" benchmarks from the International Competition on Software Verification [2], and we demonstrate that it can successfully verify large, real-world programs which can not be handled with traditional numeric abstract interpretation, and that it is competitive with state of the art techniques. Related Work The Houdini [3] algorithm mines the program for a set of predicates, and then finds the largest inductive subset, dropping the candidate non-inductive lemmas until the overall inductiveness is achieved. The optimality proof for Houdini is present in the companion paper [4]. A very similar algorithm is used by Bradley et Al. [5] to generate the inductive invariants from negations of the counter-examples to induction.
Inductive weakening based on counterexamples-to-induction can be seen as an algorithm for performing predicate abstraction [6]. Generalizing inductive weakening to best abstract postcondition computation Reps et al. [7] use the weakening approach for computing the best abstract transformer for any finiteheight domain, which we also perform in Sec. 3.1.
Generating inductive invariants from a number of heuristically generated lemmas is a recurrent theme in the verification field. In automatic abstraction [8] a set of predicates is found for the simplified program with a capped number of loop iterations, and is filtered until the remaining invariants are inductive for the original, unmodified program. A similar approach is used for synthesizing bit-precise invariants by Gurfinkel et Al. [9].
The complexity of the inductive weakening and that of the related template abstraction problem are analyzed by Lahiri and Qadeer [10]. Overview We introduce the necessary background in Sec. 2 and the weakening algorithm in Sec. 3. We define the space of all used weakenings in Sec. 4. We develop the formula slicing algorithm for applying inductive weakening to real programs in Sec. 5, we describe our implementation and the required optimizations and improvements in Sec. 6, and we conclude with the empirical evaluation on the SV-COMP dataset in Sec. 7.

Logic Preliminaries
We operate over first-order, existentially quantified logic formulas within an efficiently decidable theory. A set of all such formulas over free variables in X is denoted by F(X). Checking such formulas for satisfiability is NP-hard, but with modern SMT (satisfiability modulo theories) solvers these checks can often be performed very fast.
A formula is said to be an atom if it does not contain logical connectives (e.g. it is a comparison x ≤ y between integer variables), a literal if it is an atom or its negation, and a clause if it is a disjunction of literals. A formula is in negation normal form (NNF) if negations are applied only to atoms, and it is in conjunctive normal form (CNF) if it is a conjunction of clauses. For a set of variables X, we denote by X a set where the prime symbol was added to all the elements of X. With φ[a 1 /a 2 ] we denote the formula φ after all free occurrences of the variable a 1 have been replaced by a 2 . This notation is extended to sets of variables: φ[X/X ] denotes the formula φ after all occurrences of the free variables from X were replaced with corresponding free variables from X . For brevity, a formula φ[X/X ] may be denoted by φ . We use the brackets notation to indicate what free variables can occur in a formula: e.g. φ(X) can only contain free variables in X. The brackets can be dropped if the context is obvious.
A formula φ(X), representing a set of program states, is said to be inductive with respect to a formula τ (X ∪ X ), representing a transition, if Eq. 2 is valid: That is, all transitions originating in φ end up in φ . We can query an SMT solver for the inductiveness of φ(X) with respect to τ (X ∪X ) using the constraint in Eq. 3, which is unsatisfiable iff φ(X) is inductive.
For a quantifier-free formula φ inductiveness checking is co-NP-complete. However, if φ is existentially quantified, the problem becomes Π p 2 -complete. For efficiency, we shall thus restrict inductiveness checks to quantifier-free formulas.

Program Semantics and Verification Task
Definition 1 (CFA). A control flow automaton is a tuple (nodes, edges, n 0 , X), where nodes is a set of program control states, modelling the program counter, n 0 ∈ nodes is a program starting point, and X is a set of program variables. Each edge e ∈ edges is a tuple (a, τ (X ∪ X ), b), modelling a possible transition, where {a, b} ⊆ nodes, and τ (X ∪ X ) is a formula defining the semantics of a transition over the sets of input variables X and output variables X .
A non-recursive program in a C-like programming language can be trivially converted to a CFA by inlining functions, replacing loops and conditionals with guarded gotos, and converting guards and assignments to constraints over input variables X and output variables X .
A concrete data state m of a CFA is a variable assignment X → Z which assigns each variable an integral value. 1 The set of all concrete data states is denoted by C. A set r ⊆ C is called a region. A formula φ(X) defines a region S of all states which it models (S ≡ {c | c |= φ}). A set of all formulas over X is denoted by F(X). A concrete state c is a tuple (m, n) where m is a concrete data state, and n ∈ nodes is a control state. A program path is a sequence of concrete states c 0 , . . . , c n such that for any two consecutive states c i = (m i , n i ) and c i+1 = (m i+1 , n i+1 ) there exists an edge (n i , τ, n i+1 ) such that m i (X) ∪ m i+1 (X ) |= τ (X ∪ X ). A concrete state s i = (m, n), and the contained node n, are both called reachable iff there exists a program path which contains s i .
A verification task is a pair (P, n e ) where P is a CFA and n e ∈ nodes is an error node. A verification task is safe if n e is not reachable. Safety is traditionally decided by finding a separating inductive invariant: a mapping from program locations to regions which is closed under the transition relation and does not contain the error state.

Invariant and Inductive Invariant
A set of concrete states is called a state-space, and is defined using a mapping from nodes to regions. A mapping I : nodes → F(X) is an invariant if it contains all reachable states, and an inductive invariant if it is closed under the transition relation: that is, it satisfies the conditions for initiation and consecution: Initiation: I(n 0 ) = Consecution: for all edges (a, τ, b) ∈ edges, for all X, X I(a)(X) ∧ τ (X ∪ X ) =⇒ (I(b)) (X ) (4) Intuitively, the initiation condition dictates that the initial program state at n 0 (arbitrary contents of memory) is covered by I, and the consecution condition dictates that under all transitions I should map into itself. Similarly to Eq. 3, the consecution condition in Eq. 4 can be verified by checking one constraint for unsatisfiability using SMT for each edge in a CFA. This constraint is given in Eq. 5, which is unsatisfiable for each edge (a, τ, b) ∈ edges iff the consecution condition holds for I.

Abstract Interpretation Over Formulas
Program analysis by abstract interpretation [11] searches for inductive invariants in a given abstract domain: the class of properties considered by the analysis (e.g. upper and lower bounds on each numeric variable). The run of abstract interpretation effectively interprets the program in the given abstract domain, performing operations on the elements of an abstract domain instead of concrete values (e.g. the interval x ∈ [1, 2] under the transition x += 1 becomes x ∈ [2, 3]). We define the abstract domain D ≡ 2 L ∪ {⊥} to be a powerset of the set of formulas L ⊆ F(X) with an extra element ⊥ attached. A concretization of an element d ∈ D is a conjunction over all elements of d, or a formula false for ⊥.
Observe that D forms a complete lattice by using set operations of intersection and union as meet and join operators respectively, and using syntactical equality for comparing individual formulas. The syntactic comparison is an overapproximation as it does not take the formula semantics into account. However, this comparison generates a complete lattice of height L + 2.

Large Block Encoding
The approach of large block encoding [12] for model checking, and the approach of path focusing [1] for abstract interpretation are based on the observation that by compacting a control flow and reducing a number of abstraction points, analysis precision and sometimes even analysis performance can be greatly improved. Both approaches utilize SMT solvers for performing abstraction afterwards.
A simplified version of compaction is possible by applying the following two rules to a CFA until a fixed point is reached: -Two consecutive edges (a, s 1 , b) and (b, s 2 , c) with no other existing edge entering or leaving b get replaced by a new edge (a, ∃X. s 1 [X /X]∧s 2 [X/X], c). -Two parallel edges (a, s 1 , b) and (a, s 2 , b) get replaced by (a, s 1 ∨ s 2 , c).
In our approach, this pre-processing is used on the CFA obtained from the analyzed program.

Counterexample-to-Induction Weakening Algorithm
The approaches [3,5,8,9] mentioned in Sec. 1 are all based on using counterexamples to induction for filtering the input set of candidate lemmas. For completeness, we restate this approach in Alg. 1.
In order to perform the weakening without syntactically modifying φ during the intermediate queries, we perform selector variables annotation: we replace each lemma l i ∈ φ with a disjunction s i ∨ l i , using a fresh boolean variable s i . Observe that if all selector variables are assumed to be false the annotated formula φ annotated is equivalent to φ, and that assuming any individual selector s i is equivalent to removing (replacing with ) the corresponding lemma l i from φ. Such an annotation allows us to make use of incrementality support by SMT solvers, by using the solving with assumptions feature.
Alg. 1 iteratively checks input formula φ for inductiveness using Eq. 3 (line 13). The solver will either report that the constraint is unsatisfiable, in which case φ is inductive, or provide a counterexample-to-induction represented by a model M(X ∪ X ) (line 14). The counterexample-driven algorithm uses M to find the set of lemmas which should be removed from φ, by removing the lemmas modelled by M in ¬φ (line 20). The visualization of such a filtering step for a formula φ consisting of two lemmas is given in Fig. 2.
As shown in related literature [4], Alg. 1 terminates with the strongest possible weakening within the linear number of SMT calls with respect to φ annotated .

From Weakenings to Abstract Postconditions
As shown by Reps et Al. [7], the inductive weakening algorithm can be generalized for the abstract postcondition computation for any finite-height lattice.
For given formulas ψ(X), τ (X ∪X ), and φ(X) consider the problem of finding a weakeningφ ⊆ φ, such that all feasible transitions from ψ through τ end up in φ. This is an abstract postcondition of ψ under τ in the lattice of all weakenings of φ (Sec. 2.4). The problem of finding it is very similar to the problem of finding an inductive weakening, as similarly to Eq. 3, we can check whether a given weakening of φ is a postcondition of ψ under τ using Eq. 6, Alg. 1 can be adapted for finding the strongest postcondition in the abstract domain of weakenings of the input formula with very minor modifications. The required changes are accepting an extra parameter ψ, and changing the queried constraint (line 6) to Eq. 6. The found postcondition is indeed strongest [7].
Model M identifies a counter-example to induction. From M |= ¬L 2 (X ) we know that the lemma L 2 has to be dropped. As weakening progresses, the shaded region in the left box is growing, while the shaded region in the right box is shrinking, until there are no more counterexamples to induction.

The Space of All Possible Weakenings
We wish to find a weakening of a set of states represented by φ(X), such that it is inductive under a given transition τ (X ∪ X ). For a single-node CFA defined by initial condition φ and a loop transition τ such a weakening would constitute an inductive invariant as by definition of weakening it satisfies the initial condition and is inductive. We start with an observation that for a formula in NNF replacing any subset of literals with results in an over-approximation, as both conjunction and disjunction are monotone operators. E.g. for a formula φ ≡ (l a ∧ l b ) ∨ l c such possible weakenings are , l b ∨ l c , and l a ∨ l c .
The set of weakenings defined in the previous paragraph is redundant, as it does not take the formula structure into account -e.g. in the given example if l c is replaced with it is irrelevant what other literals are replaced, as the entire formula simplifies to . The most obvious way to address this redundancy is to convert φ to CNF and to define the set of all possible weakenings as conjunctions over the subsets of clauses in φ CNF . E.g. for the formula φ ≡ l a ∧ l b ∧ l c possible weakenings are l a ∧ l b , l b ∧ l c , and l a ∧ l c . This method is appealing due to the fact that for a set of lemmas the strongest (implying all other possible inductive weakenings) inductive subset can be found using a linear number of SMT checks [5]. However (Sec. 2.1) polynomial-sized CNF conversion (e.g. Tseitin encoding) requires introducing existentially quantified boolean variables which make inductiveness checking Π p 2 -hard. The arising complexity of finding inductive weakenings is inherent to the problem: in fact, the problem of finding any non-trivial ( = ) weakening within the search space described above is Σ p 2 -hard (see proof in Appendix A).
Definition 2 (Relaxed Conjunctive Normal Form (RCNF)). A formula φ(X) is in relaxed conjunctive normal form if it is a conjunction of quantifier-free formulas (lemmas).
For example, the formula φ ≡ l a ∧ (l b ∨ (l c ∧ l d )) is in RCNF. The overapproximation comes from the fact that non-atomic parts of the formula are grouped together: the only possible non-trivial weakenings for φ are l a and l b ∨ (l c ∧ l d ), and it is impossible to express l a ∧ (l b ∨ l c ) within the search space. We may abuse the notation by treating φ in RCNF as a set of its conjuncts, and writing l ∈ φ for a lemma l which is an argument of the parent conjunction of φ, or φ 1 ⊆ φ 2 to indicate that all lemmas in φ 1 are contained in φ 2 , or φ for the number of lemmas in φ. For φ in RCNF we define a set of all possible weakenings as conjunctions over all sets of lemmas contained in φ. We use an existing, optimal counter-example based algorithm in order to find the strongest weakening of φ with respect to τ in the next section.
A trivially correct conversion to a relaxed conjunctive normal is to convert an input formula φ to a conjunction {φ}. However, this conversion is not very interesting, as it gives rise to a very small set of weakenings: φ and . Consequently, with such a conversion, if φ is not inductive with respect to the transition of interest, no non-trivial weakening can be found. On the other extreme, φ can be converted to CNF explicitly using associativity and distributivity laws, giving rise to a very large set of possible weakenings. Yet the output of such a conversion is exponentially large.
We present an algorithm which converts φ into a polynomially-sized conjunction of lemmas. The following rules are applied recursively until a fixpoint is reached: Factorization When processing a disjunction over multiple conjunctions we find and extract a common factor. E.g.
. Explicit expansion with size limit A disjunction L, where each l ∈ L is a conjunction, can be converted to a conjunction over disjunctions over all elements in the cross product over L.
Applying such an expansion results in an exponential blow-up, but we only perform it if the resulting formula size is smaller than a fixed constant, and we limit the expansion depth to one.
Eliminating Existentially Quantified Variables The formulas resulting form large block encoding (Sec. 2.5) may have intermediate (neither input nor output), existentially bound variables. In general, existential quantifier elimination (with e.g. Fourier-Motzkin) is exponential. However, for many cases such as simple deterministic assignments, existential quantifier elimination is easy: e.g.
∃t. x = t + 3 ∧ t = x + 2 can be trivially replaced by x = x + 5 using substitution. We use a two-step method to remove the quantified variables: we run a best-effort pattern-matching approach, removing the bound variables which can be eliminated in polynomial time, and in the second step we drop all the lemmas which still contain the existentially bound variables. The resulting formula is an over-approximation of the original one.

Formula Slicing: Overall Algorithm
We develop the formula slicing algorithm in order to apply the inductive weakening approach for generating inductive invariants in large, potentially non-reducible programs with nested loops.
"Classical" Houdini-based algorithms consist of two steps: candidate lemmas generation, followed by counterexample-to-induction-based filtering. However, in our case candidate lemmas representing postconditions depend on previous filtering steps, and careful consideration is required in order to generate unique candidate lemmas which do not depend on the chosen iteration order.
Abstract Reachability Tree In order to solve this problem we use abstract reachability tree [13] (ART) as a main datastructure for our algorithm. For the simplicity of notation we introduce the projection function π i , which projects the i th element of the tuple. An ART describes the current invariant candidate processed by the analysis for a fixed CFA (nodes, edges, n 0 , X), and is defined by a set of nodes T . Each node t ∈ T is a triple, consisting of a CFA node n ∈ nodes, defining which location t corresponds to, an abstract domain element d ∈ D, defining the reachable state space at t, and an optional backpointer b ∈ (T ∪ {∅}), defining the tree structure. The tree topology has to be consistent with the structure of the underlying CFA: node a ∈ T can have a backpointer to the node b ∈ T only if there exists an edge (π 1 (a), , π 1 (b)) in the CFA. The starting tree node t 0 is (n 0 , , ∅).
An ART is sound if the output of each transition over-approximates the strongest postcondition: that is, for each node t ∈ T with non-empty backpointer b = π 3 (t), an edge e = (π 1 (b), τ, π 1 (t)) must exist in edges, and the abstract domain element associated with t must over-approximate the strongest postcondition of b under τ . Formally, the following must hold: ∃X. π 2 (b) ∧ τ =⇒ π 2 (t) (recall that priming is a renaming operation [X/X ]). A node b ∈ T is fully expanded if for all edges (π 1 (t), τ, n) ⊆ edges there exists a node t ∈ T , where π 1 (t) = n, and π 2 (t) over-approximates the strongest post-condition of A sound labelled ART where all nodes are either fully expanded or covered represents an inductive invariant.
The transfer relation for the formula slicing is given in Alg. 3. In order to generate a successor for an element (n a , d, b), and an edge (n a , τ, n b ) we first traverse the chain of backpointers up the tree. If we can find a "sibling" element s where π 1 (s) = n a 2 by following the backpointers, we weaken s until inductiveness (line 4) relative to the new incoming transition τ , and return that as a postcondition. Such an operation effectively performs widening [11] to enforce convergence. Alternatively, if no such sibling exists, we convert ∃X. ∧τ to RCNF form (line 6), and this becomes a new element of the abstract domain.
The main fixpoint loop performs the following calculation: for every leaf in the tree which is not yet expanded or covered, all successors are found using the transfer relation defined in Alg. 3, and for each newly created element, coverage relation is checked against all elements in the same partition. A simplified version of this standard fixpoint iteration on ART is given in Alg. 2.
Observe that our algorithm has a number of positive features. Firstly, because our main datastructure is an ART, in case of a counterexample we get a path to a property violation (though due to abstraction used, not all taken transitions are necessarily feasible, similarly to the leaping counterexamples of LoopFrog [14]). Secondly, our approach for generating initial candidate invariants ensures uniqueness, even in the case of a non-reducible CFA. Expand. 10: for all edge e ∈ edges where π1(e) = π1(t) do 11: T ← T ∪ { TransferRelation(e, t) } 12: E ← E ∪ {t} 13: Check Coverage. 14: for all t1 ∈ (T \ C) where π1(t1) = π1(t) do 15: if π2(t1) =⇒ π2(t) then 16:  As a downside, tree representation may lead to the exponential state-space explosion (as a single node in a CFA may correspond to many nodes in an ART). However, from our experience in the evaluation (Sec. 7), with a good iteration order (stabilizing inner components first [15]) this problem does not occur in practice.

Example Formula Slicing Run
Consider running formula slicing on the program in Fig. 3, which contains two nested loops. The corresponding edge encoding is given in Eq. 7: Similarly to Eq. 3, we can check candidate invariants A(X), B(X) for inductiveness by posing an SMT query shown in Eq. 8. The constraint in Eq. 8 is unsatisfiable iff {A : A(X), B : B(X)} is an inductive invariant (Sec. 2.3).
Eq. 8 is unsatisfiable iff all of the disjunction arguments are unsatisfiable, and hence the checking can be split into multiple steps, one per analyzed edge. Each postcondition computation (Alg. 3) either generates an initial seed invariant candidate, or picks one argument of Eq. 8, and weakens the right hand side until the constraint becomes unsatisfiable. Run of the formula slicing algorithm on the example is given below: -Traversing τ 1 , we get the initial candidate invariant

Implementation
We have developed the Slicer tool, which runs the formula slicing algorithm on an input C program. Slicer performs inductive weakenings using the Z3 [16] SMT solver, and best-effort quantifier elimination using the qe-light Z3 tactic. The source code is integrated inside the open-source verification framework CPAchecker [17], and the usage details are available at http://slicer. metaworld.me. Our tool can analyze a verification task (Sec. 2.2) by finding an inductive invariant and reporting true if the found invariant separates the initial state from the error property, and unknown otherwise. We have implemented the following optimizations: Live Variables We precompute live variables, and the candidate lemmas generated during RCNF conversion (Alg. 3, line 6) which do not contain live variables are discarded. Non-Nested Loops When performing the inductive weakening (Alg. 3, line 4) on the edge (N, τ, N ) we annotate and weaken the candidate invariants on both sides (without modifications described in Sec. 3.1), and we cache the fact that the resulting weakening is inductive under τ . CFA Reduction We pre-process the input CFA and we remove all nodes from which there exists no path to an error state.

Syntactic Weakening Algorithm
A syntactic-based approach is possible as a faster and less precise alternative which does not require SMT queries. For an input formula φ(X) in RCNF, and a transition τ (X ∪ X ), syntactic weakening returns a subset of lemmas in φ, which are not syntactically modified by τ : that is, none of the variables are modified or have their address taken. For example, the lemma x > 0 is not syntactically modified by the transition y = y + 1 ∧ x ≥ 1, but it is modified by x = x + 1.

Experiments and Evaluation
We have evaluated the formula slicing algorithm on the "Device Drivers" category from the International Competition on Software Verification (SV-COMP) [2].
The dataset consists of 2120 verification tasks, of which 1857 are designated as correct (the error property is unreachable), and the rest admit a counter-example.
All the experiments were performed on Intel Xeon E5-2650 at 2.00 GHz, and limits of 8GB RAM, 2 cores, and 600 seconds CPU time per program. We compare the following three approaches: Slicer-CEX (rev 21098) Formula slicing algorithm running counterexamplebased weakening (Sec. 3). Slicer-Syntactic Same, with syntactic weakening (Sec. 6.1). Predicate Analysis (rev 21098) Predicate abstraction with interpolants [18], as implemented inside CPAchecker [19]. We have chosen this approach for comparison as it represents state-of-the-art in model checking, and was found especially suitable for analyzing device drivers. PAGAI [20] (git hash e44910) Abstract interpretation-based tool, which implements the path focusing [1] approach.
In Tab. 1 we show overall precision and performance of the four compared approaches. As formula slicing is over-approximating, it is not capable of finding counterexamples, and we only compare the number of produced safety proofs.
From the data in the table we can see that predicate analysis produces the most correct proofs. This is expected since it can generate new predicates, and it is driven by the target property. However, formula slicing and abstract interpretation have much less timeouts, and they do not require target property annotation, making them more suitable for use in domains where a single error property is not available (advanced compiler optimizations, multi-property verification, and boosting another analysis by providing an inductive invariant). The programs verified by different approaches are also different, and formula slicing verifies 22 programs predicate analysis could not.
The performance of the four analyzed approaches is shown in the quantile plot in Fig. 4a. The plot shows that predicate analysis is considerably more time consuming than other analyzed approaches. Initially, PAGAI is much faster than other tools, but around 15 seconds it gets overtaken by both slicing approaches. Though the graph seems to indicate that PAGAI overtakes slicing again around 100 seconds, in fact the bend is due to out of memory errors.
The quantile plot also shows that the time taken to perform inductive weakening does not dominate the overall analysis time for formula slicing. This can be seen from the small timing difference between the syntactic and counterexamplebased approaches, as the syntactic approach does not require querying the SMT solver in order to produce a weakening.
Finally, we present data on the number of SMT calls required for computing inductive weakenings in Fig. 4b. The distribution shows that the overwhelming majority of weakenings can be found within just a few SMT queries.

Conclusion and Future Work
We have proposed a "formula slicing" algorithm for efficiently finding potentially disjunctive inductive invariants in programs, which performs abstract interpreta-  tion in the space of weakenings over the formulas representing the "initial" state. We have demonstrated that it could verify many programs other approaches could not, and that the algorithm can be run on real programs.
The motivation for our approach is addressing the limitation of abstract interpretation which forces it to perform abstraction after each analysis step, which often results in a very rough over-approximation. Thus we believe our method is well-suited for augmenting numeric abstract interpretation.
As with any new inductive invariant generation technique, a possible future work is investigating whether formula slicing can be used for increasing the performance and precision of other program analysis techniques, such as kinduction, predicate abstraction or property-directed reachability. An obvious approach would be feeding the invariants generated by formula slicing to a convex analysis running abstract interpretation or policy iteration [21]. Furthermore, the inductive weakening approach could also be used for the generalization of the k-induction algorithm over multiple properties. If we check a set of properties P for inductiveness under the loop transition τ , and P is not inductive, the weakening can find the largest inductive subset.

A Complexity of Finding a Non-Trivial Inductive
Weakening Over Literals As we have mentioned in Sec. 4, a more expressive space of weakenings over formulas is to consider replacing any subset of literals with after a NNF conversion. In this appendix we show that it leads to a number of undesirable properties, including the absence of strongest inductive weakening (Ex. 1), and Σ p 2 complexity for finding any non-trivial inductive weakening (Thm. 1).
Example 1 (No Strongest Inductive Weakening). Consider a program over four Boolean variables a, b, c, d and the transition relation Consider finding the weakening of φ ≡ (a ∧ b) ∨ (c ∧ d), Both the {a}-weakening (b∨(c∧d)) and the {c}-weakening ((a∧b)∨d) are inductive, but their intersection is not a weakening of φ and there is no inductive weakening stronger than either of these.
Proof (Belonging to Σ p 2 ). Let S be some subset of literals of φ. Letφ be the weakening of φ where all literals in S are replaced with . Checking thatφ is inductive with respect to τ is in co-NP, therefore the problem of finding a non-trivialφ is in Σ p We show completeness by constructing from an arbitrary closed ∃ * ∀ * formula ψ a loop τ and a precondition I such that the existence of a non-trivial ( ≡ ) weakening of the precondition is equivalent to the truth of ψ. Without loss of generality, let ψ have m Boolean variables x 0 , . . . , x m−1 bound by the existential quantifier and n Boolean variables y 0 , . . . , y n−1 bound by the universal one: ψ ≡∃x 0 , . . . , x m−1 . ∀y 0 , . . . , y n−1 .G(x 0 , . . . , x m−1 , y 0 , . . . , y n−1 ) Let us denote the bitvector (x 0 , . . . , x m−1 ) as X and the bitvector (y 0 , . . . , y n−1 ) as Y . Let enc : B m → [0, 2 m − 1] denote the function for standard integer encoding of the X bitvector, x 0 being the lowest-order bit and x m−1 the highestorder one. Let succ : B m \ { m } → B m be the successor function such that enc(succ(X)) = 1 + enc(succ(X)), which is only defined for non-overflowing values. Now we define the transition system over the set of boolean variables X and the overflow bit o. Let the initial state I(X, o) be X = ⊥ ∧ o = ⊥, and let the transition relation τ (X, X , o, o ) to be:  In plain terms, the transition relation may increment X as long as it is not overflowing and the guard can be falsified for some Y , and X is forced to stay constant on overflow or when it reaches someX such that ∀Y.G(X, Y ). Initialization and transition relation for the transition system, and the corresponding program are shown in Fig. 4.

Lemma 1.
There exists a non-trivial ( ≡ ) inductive invariant for the program in Fig. 4 if and only if ψ (Eq. 9) is satisfiable.
Observe that τ can be satisfied for all possible values of X by a suitable choice of X . Let f (X) be the largest (under enc) possible value of X which satisfies τ (X, X , o, o ).
Proof. Sufficient Condition. Assume ψ is satisfiable for someX. ThenX is a fixed point under f (as it satisfies G for all possible values of Y ). Consider the set of values defined by R ≡ ¬o ∧ enc(X) ≤X}. It is inductive, since the largest value in R set maps to itself under f , and all other values map to the "next" (under enc) value in R. It is also non-trivial, since the bit o is defined not to be .
Proof. Necessary Condition. Assume there exists a non-trivial inductive invariant for the program in Fig. 4. At every transition, X either stays constant or is incremented by 1. Since we have assumed the existence of a non-trivial inductive invariant, there existsX such that it is a fixpoint under f and enc(X) ≤ 2 m − 1 (otherwise the entire state space is reachable, and the only possible inductive invariant is ). This is only possible if ∀Y.G(X, Y ) (otherwisex may be incremented). But this is exactly the condition for ψ being satisfiable.