Quantified Invariants via SyntaxGuided Synthesis
Abstract
Programs with arrays are ubiquitous. Automated reasoning about arrays necessitates discovering properties about ranges of elements at certain program points. Such properties are formally specified by universally quantified formulas, which are difficult to find, and difficult to prove inductive. In this paper, we propose an algorithm based on an enumerative search that discovers quantified invariants in stages. First, by exploiting the program syntax, it identifies ranges of elements accessed in each loop. Second, it identifies potentially useful facts about individual elements and generalizes them to hypotheses about entire ranges. Finally, by applying recent advances of SMT solving, the algorithm filters out wrong hypotheses. The combination of properties is often enough to prove that the program meets a safety specification. The algorithm has been implemented in a solver for Constrained Horn Clauses, FreqHorn, and extended to deal with multiple (possibly nested) loops. We show that FreqHorn advances stateoftheart on a wide range of public arrayhandling programs.
1 Introduction
Formally verifying programs against safety specifications is difficult. This problem worsens in the presence of data structures like lists, arrays, and maps, which are ubiquitous in realworld applications. For instance, proving an arrayhandling program safe often requires discovering an inductive invariant that is universally quantified over ranges of array elements. Such invariants help to prove the unreachability of error states independently of the size of the array. However, the majority of invariant synthesis approaches are limited to quantifierfree numerical invariants. The approach presented in this paper advances the knowledge by an effective technique to discover quantified invariants over arrays and linear integer arithmetic.
Syntaxguided techniques [3] have recently been applied to synthesize quantifierfree numerical invariants [15, 16, 17, 34] in the approach called FreqHorn. In a nutshell, FreqHorn collects various statistics from the syntactical patterns occurring in the program’s source code and uses them to construct a set of formal grammars that specify a search space for invariants. It is often sufficient to perform an enumerative search over the formulas produced from these grammars and identify a set of suitable inductive invariants among them using an offtheshelf solver for Satisfiability Modulo Theories (SMT). The presence of arrays complicates this reasoning in a few respects: it is hard to find suitable candidates and difficult to prove them inductive.
In this paper, we present a novel technique that extends the approach of enumerative search in general, and its instantiation in FreqHorn in particular, to reason about quantifiers. It discovers invariants over arrays in multiple stages. First, by exploiting the program syntax, it identifies ranges of elements accessed in each loop. Second, it identifies potentially useful facts about individual elements and generalizes them to hypotheses about entire ranges. The SMTbased validation of candidates, which are quantified formulas, is often inexpensive as they are constructed using the same syntactic patterns that appear in the source code. Furthermore, for supporting certain corner cases, our approach allows specifying additional rules that help in generalizing learned properties. The combination of properties proven inductive by an SMT solver is often enough to prove that the program meets a safety specification.
We show that FreqHorn advances stateoftheart on a selection of arrayhandling programs from SVCOMP^{1} and literature. For instance, it can prove completely automatically that an array is monotone after applying a sorting algorithm. Furthermore, FreqHorn is able to discover quantifierfree invariants over integer variables in the program, use them as inductive relatives while checking inductiveness of quantified candidates over arrays; and vice versa.
While a detailed discussion of the related work comes later in the paper (Sect. 6), it is noteworthy that being syntaxguided crucially helps us overcome several limitations of other techniques to verify arrayhandling programs [2, 9, 11, 35]. Most of them avoid inferring quantified invariants explicitly and thus do not produce checkable proofs. As a result, tools are fragile and in practice often output false positives (see Sect. 5 for concrete results). By comparison, our approach never produces false positives, and its results can be validated by existing SMT solvers.

a novel syntaxguided approach to generate universally quantified invariants for programs manipulating arrays;

an algorithm and its fully automated implementation; and

a thorough experimental evaluation comparing our technique with stateoftheart in verification of arrayhandling programs.
The rest of the paper is structured as follows. In Sect. 2, we give background and notation and illustrate our approach on an example. Our main contributions are then presented in Sect. 3 (main algorithm) and Sect. 4 (important design choices). In Sect. 5, we show the evaluation and comparison with stateoftheart. Finally, the related work and conclusion complete the paper in Sects. 6 and 7, respectively.
2 Background
The Satisfiability Modulo Theories (SMT) task is to decide whether there is an assignment m of values to variables in a firstorder logic formula \(\varphi \) that makes it true. We write \(\varphi \implies \psi \), if every satisfying assignment to \(\varphi \) is also a satisfying assignment to some formula \(\psi \). By \( Expr \) we denote the space of all possible quantifierfree formulas in our background theory and by \({ Vars }\) a range of possible variables.
2.1 Programs as Constrained Horn Clauses
To guarantee expected behaviors, programs require proofs, such as inductive invariants, ranking functions, or recurrence sets. It is becoming increasingly popular to consider a verification task as a proof synthesis task which is formulated as a system of SMT formulas involving unknown predicates, also known as constrained Horn clauses (CHC). The synthesis goal is to discover a suitable interpretation of all unknown predicates that make all CHCs true. CHCs offer the advantages of flexibility and modularity in designing verifiers for various systems and languages. CHCs can be constructed in a way that captures the operational semantics of a language in question, and an offtheshelf CHC solver can be used for solving the resulting formulas.
Definition 1
Example 1
Figure 1 gives a program in the C programming language that handles two integer arrays, A and B, both of an unknown size N. The A array has unknown content, and the program first identifies a value m which is smaller or equal to all elements of A (it might be either a minimal element among the content of A or 0). Then, the program populates B by values of A with m subtracted. Interestingly, the order of elements A and B is not preserved, e.g., A[0]  m gets written to B[N  1], and so on. Finally, the program computes the sum s of all elements in B and requires us to prove that s is never negative.
Figure 2 gives a CHC encoding of the program. The system has three uninterpreted predicates, \(\varvec{inv}_1\), \(\varvec{inv}_2\), and \(\varvec{inv}_3\) corresponding to invariants at heads of the three loops. The primed variables correspond to modified variables. Rules B, D, and F encode the loop bodies, and the remaining rules encode the fragments of code before, after, or between the loops. In particular, rule G ensures that after the third loop has terminated, a program state with a negative value of s is unreachable. Before we describe how our technique solves this CHC system (see Sect. 2.2), we briefly introduce the notion of satisfiability of CHCs.
Definition 2
Given a set of uninterpreted relation symbols Open image in new window and a set S of CHCs over Open image in new window , we say that S is satisfiable if there exists an interpretation that assigns to each nary symbol Open image in new window a relation over ntuples and makes all implications in S valid.
In the paper, we assume that a relation assigned by an interpretation is represented by a formula \(\psi \) over at most n free variables.
We call a CHC C inductive when \( rel ( src (C)) = rel ( dst (C)) = \varvec{inv}\) for some \(\varvec{inv}\). While accessing an array in a loop, we assume the existence of an integer counter variable. More formally:
Definition 3
2.2 Illustrating Example
Additionally, the interpretation of \(\varvec{inv}_2\) gets a relational fact about pairs of elements A[0] and \(B[N  1]\), A[1] and \(B[N  2]\), ..., \(A[i1]\) and \(B[N  i  2]\), which again appears as a progress lemma and then gets finalized in an interpretation of \(\varvec{inv}_3\). With these two quantified invariants about all elements of A, and relation about pairs of elements of A and B, it is possible to derive the remaining lemma in the interpretation of \(\varvec{inv}_3\), namely, \(s\ge {0}\); which concludes the proof.
3 Invariants via Enumerative Search
In this work, we aim at discovering a solution for a CHC system S over a set of uninterpreted symbols Open image in new window enumeratively, i.e., by guessing a candidate formula for each Open image in new window , substituting it for all CHCs \(C \in S\) and checking their validity.
3.1 QuantifierFree Invariants
We build on top of an algorithm, called FreqHorn, recently proposed in [17]. Its key insight is an automatic construction of a set of formal grammars \(G(\varvec{inv})\) for each Open image in new window based on either source code, program behaviors, or both. Importantly, these grammars are conjunctionfree: they cannot be used to produce a conjunction of clauses and can give rise to only a finite number of formulas, potentially related to invariants (otherwise, the approach does not guarantee strong convergence). Since invariants are often represented by a conjunction of lemmas, FreqHorn attempts to sample (i.e., recursively apply production rules) each lemma from a grammar in separation, until a combination of them is sufficient for the inductiveness and safety, or a search space is exhausted. FreqHorn relies on an SMT solver to filter out unsuccessfully sampled lemmas.
The construction of formal grammars is biased by the syntax of CHC encoding. First, FreqHorn collects a set of \( Seeds \) by converting the body of each CHC to a Conjunctive Normal Form, extracting, and normalizing each conjunct. Then, the set of seeds could be optionally replenished by a set of behavioral seeds and bounded proofs. They are constructed respectively from the concrete values of variables obtained from actual program runs, and Craig interpolants from unsatisfiable finite unrollings of the CHC systems. Finally, the production rules are created in a way to enable producing seeds and also their \( mutants \) (i.e., syntactically similar formulas to seeds). In general, no specific restriction on a grammarconstruction method is imposed; so in practice, the grammars are allowed to be more (or less) general to enable a broader (or more focused) search space for invariants.
3.2 Quantified Candidates from QuantifierFree Grammars
The main obstacle for applying the enumerative search to generate array invariants is that the grammars do not allow quantifiers. Because grammars are constructed automatically from syntactic patterns which appear in the original programs, in the presence of arrays, we can expect expressions involving only particular elements of arrays (such as ones accessed via a loop counter). However, since each loop repeats certain operations over a range of array elements, we have to generalize the extracted expressions about individual elements to expressions about entire ranges.

a set of quantified integer variables \({ QVars }(\varvec{inv})\), which are introduced by our algorithm and do not appear in \({ Vars }(\varvec{inv})\);

a range formula over \({ QVars }(\varvec{inv}) \cup { IntVars }(\varvec{inv})\); and

a quantifierfree cell property over \({ QVars }(\varvec{inv}) \cup { Vars }(\varvec{inv})\).
A naive idea for getting a range formula and a cell property is to sample them separately, and then to bind them together using some \({ QVars }(\varvec{inv})\). But it would result in a large search space. Algorithm 1 gives a more tailored procedure on the matter. The central role in this process is taken by an analysis of the loop counters which are used to access array elements (line 3). This analysis is performed once for each loop before the main verification process, and thus its results are reused in all iterations of the verification process.
Once grammars, \({ QVars }\), and ranges are detected, our approach proceeds to sample candidates and to check them with an SMT solver. The general flow of this algorithm is illustrated in Algorithm 2. For each Open image in new window , it initiates a set \( Lemmas (\varvec{inv})\) (line 2). Then it iteratively guesses lemmas until a combination of them is inductive and safe, or a search space is exhausted (lines 3–4).
Compared to the baseline approach from [17], our new algorithm fixes a shape for the candidates for arrays. At the same time, it permits to sample quantifierfree candidates (line 6): they could be either formulas over counters or any other variables in the loop, or even formulas over isolated array elements (if, e.g., accessed by a constant). Then (line 8), Algorithm 2 propagates candidates through all available implications in CHCs using quantifier elimination and identifies lemmas among the candidates. This step is similar to the baseline approach from [17], but for completeness of presentation, we provide the pseudocode in Algorithms 3 and 4. The only differences are (1) in the implementation of the candidate propagation for array candidates and (2) in the weakening of failed candidates (both in Algorithm 3, to be discussed in Sects. 4.3 and 4.4, respectively).
Both successful and unsuccessful candidates are “blocked” from their grammars to avoid resampling them in the next iterations. This fact together with the property of grammars being conjunctionfree gives the main hint for proving the following theorem.
Theorem 1
Algorithm 2 always makes a finite number of iterations, and if it returns with SAT then the CHC system is satisfiable.
Next section discusses a particular instantiation of important subroutines that make our invariant synthesizer effective in practice.
4 Design Choices
Our main contribution is a completely automated algorithm for finding quantified invariants for arrayhandling loops. In this section, we first show how by exploiting the program syntax we can identify ranges of elements accessed in each loop (Sect. 4.1). Second, we present an intuitive justification to why our candidates can often be proved as lemmas by an offtheshelf SMT solver (Sect. 4.2). Finally, we extend our algorithm to handle more complicated cases of multiple loops (Sects. 4.3–4.4), and benchmarks of the tiling [9] technique, which are adapted from the industrial code of battery controllers (Sect. 4.5).
4.1 Discovery of Progress Lemmas
We start with the simplest scenario of a single loop handling just one array. Let S be a system of CHCs over a set of uninterpreted relation symbols Open image in new window . Let Open image in new window correspond to a loop, in which arrays are accessed using some counter variable i (counters are automatically identified by posing and solving queries of forms (1) and (2)).
Recall that we do not necessarily require the array elements to be accessed directly by i, and we allow an access function f to identify relationships between i and an index of the accessed element. However, we assume that the counter is unique in the loop because it is the case in most of the practical applications. In principle, our algorithm can be extended to loops handling several independent counters (although it is rare in practice), with the help of additionally discovered lemmas that describe relationships among counters. We leave a discussion about this to future work.
Definition 4
A range of \(\varvec{inv}\) and a counter i is a formula over \({ IntVars }(\varvec{inv})\) and a free variable v having form \(L< v \wedge v < U\), such that either of formulas \(L < i\) or \(i < U\) is a lemma for \(\varvec{inv}\). A progress lemma is either a formula \(L< v \wedge v < i\) (if \(L < i\) is a lemma), or a formula \(i< v \wedge v < U\) (if \(i < U\) is a lemma).
Both ranges and progress ranges can be identified statically. Let \(C_1\) and \(C_2\) be two CHCs, such that \(\varvec{inv}= rel ( dst (C_1)) = rel ( src (C_2)) = rel ( dst (C_2))\) and \(\varvec{inv}\ne rel ( src (C_1))\). It is common in practice that \(body(C_1)\) identifies a symbolic bound b on the initial value of i: it could be either a lower bound (if i increments in \(body (C_2)\)) or an upper bound (if i decrements). In this case, a progress range of \(\varvec{inv}\) is simply computed as a lemma for \(\varvec{inv}\) over i and b. A range of \(\varvec{inv}\) can often be constructed as a conjunction of the progress range with the negation of the termination condition of \(body(C_2)\).^{2}
Example 2
For the CHCencoding of the program is shown in Fig. 2, the ranges of \(\varvec{inv}_1, \varvec{inv}_2\) and \(\varvec{inv}_3\) are all equal to \(1< v < N\). The progress range of \(\varvec{inv}_1\) is \(i< v < N\), and the progress ranges of \(\varvec{inv}_2\) and \(\varvec{inv}_3\) are \(1< v < i\).
If a progress candidate is proven inductive, we call it a progress lemma.
4.2 SMTBased Inductiveness Checking
We rely on recent advances of SMT solving to identify successful candidates, a conjunction of which is directly used to prove the desired safety specification. In general, solving quantified formulas for validity is a hard task, however, in certain cases, the initiation and inductiveness queries can be simplified and reduced to a sequence of (sometimes even quantifierfree) formulas over integer arithmetic. We illustrate such proving strategy, inspired by the tiling approach [9], on the following example.
Example 3
In general, we cannot always conduct proofs that easily. Often, the prerequisite for success is the commonality of an access function f in the candidate and the body of the CHC. Fortunately, our algorithm ensures that all access functions used in the candidates are borrowed directly from bodies of CHCs. Thus, in many cases, FreqHorn is able to check large amounts of candidates quickly.
4.3 Strategy of Lemma Propagation
Definition 5
Example 4
Note that this formula is not going to be immediately learned as a lemma, but instead should be checked by the solver for inductiveness. Intuitively, such a candidate represents some facts about array elements that were accessed during a loop that has terminated. If after the propagation it appeared that the candidate uses the entire range then we refer to such candidate to as a finalized candidate.
4.4 Weakening Strategy
Whenever a finalized candidate cannot be proven inductive, we often do not want to withdraw it completely. Instead, our algorithm runs weakening and proposes regress candidates. The main idea is to calculate a range of elements which have not been touched by the loop yet. This is an inverse of the procedure outlined in Sect. 4.1.
Definition 6
We call candidates that use regress ranges in their left sides as regress candidates. Clearly, a regress candidate is weaker than the corresponding finalized candidate. Thus, from the failure to prove inductiveness of the finalized candidate it does not follow that the regress candidate is not inductive; and it makes sense to try proving it in the next iteration.
4.5 Learning from Subranges
Lemma 1
Example 5
Figure 3 shows a program from the tiling benchmark suite [9]. If lemmas \(\forall j \,.\,0< j < N \implies A[2*j1] = 0 \vee A[2*j1] \le m\) and \(\forall j \,.\,0< j < N \implies A[2*j2] = 0 \vee A[2*j2] \le m\) are discovered, then formula \(\forall j \,.\,0 \le j < 2*N1 \implies A[j] = 0 \vee A[j] \le m\) is also a lemma.
5 Evaluation
We have implemented our algorithm on top of the FreqHorn^{3} tool. It takes a system of CHCs with arrays as input and performs an enumerative search as presented in Sect. 4. The tool uses Z3 [12] to solve SMT queries.
We have evaluated FreqHorn on 137 satisfiable CHCtranslations of publicly available C programs (whose assertions are safe) taken from the SVCOMP ReachSafety Array subcategory and literature. These programs include variations of standard array copying, initializing, maximum, minimum, sorting, and tiling benchmarks. Among these 137 benchmarks, 79 have a single loop, and 58 have multiple loops, including 7 that have nested loops. These programs are encoded using the theories of Arrays, Linear (LIA) and Nonlinear Integer Arithmetic (NIA). Our experiments have been performed on an Ubuntu 18.04 machine running at 2.5 GHz and having 16 GB memory, with a timeout of 100 s for every benchmark. FreqHorn solved 129 benchmarks within the timeout, of which 73 solved benchmarks had a single loop and 56 had multiple loops.
Compare to 129 benchmarks solved by FreqHorn, only 81 were solved by Spacer, 108 – by VeriAbs, 70 – by VIAP, and 48 – by Booster.
FreqHorn solved 54 benchmarks on which Spacer diverged. Our intuition is that Spacer works poorly on programs with nondeterministic assignments and NIA operations, which our tool can handle.
FreqHorn solved 27 benchmarks on which VeriAbs diverged. VeriAbs failed to solve programs with nested loops and when array values were dependent on access indices. Furthermore, it decided one of the programs as unsafe, Timewise, FreqHorn significantly outperformed VeriAbs on all benchmarks. Importantly, the short time taken by FreqHorn includes the time for generating a checkable witness – quantified invariant – an essence that VeriAbs cannot produce by design. On the other side, VeriAbs solved several benchmarks after merging loops. No quantified invariant satisfying the FreqHorn’s restrictions exists for these benchmarks before this program transformation.
FreqHorn solved 60 programs on which VIAP diverged. VIAP decided one program as unsafe. There were no programs on which FreqHorn took more time than VIAP. Finally, FreqHorn solved 83 programs on which Booster diverged. And again, Booster decided two programs as unsafe.
6 Related Work
Our algorithm for quantified invariant synthesis extends the prior work on checking satisfiability of CHCs [15, 16, 17], where solutions do not permit quantifiers. It works in a similar – enumerateandcheck – manner, but there are two crucial changes: (1) introduction of quantifiers, to formulate hypotheses over a subset of array indices, and (2) a generalization mechanism, to derive properties that may hold over the entire range of array indices.
Many existing approaches for verifying programs over arrays are extensions of wellknown techniques for programs over scalar variables to quantified invariants. For example, by extending predicates with Skolem variables in predicate abstraction [30], by exploiting the MCMT [19] framework in lazy abstraction with interpolants [1] and its integration with acceleration [2], and, recently, QUIC3 [22], that extends IC3 [8, 14] to universally quantified invariants. Apart from the skeletal similarity, however, these approaches rely on orthogonal techniques.
Partitioning of arrays has also been used to infer invariants in many different ways. It refers to splitting an array into symbolic segments, and may be based on syntax [20, 23, 25] or semantics [10, 31]. Invariants may be inferred for each segment separately and generalized for the entire array. The partitioning need not be explicit, as in [13]. However, most of these techniques (except [13, 31]) are restricted to contiguous array segments, and work well when different loop iterations write to disjoint array locations or when the segments are nonoverlapping. Tiling [9], a propertydriven verification technique, overcomes these limitations for a class of programs by inferring array access patterns in loops. But identifying tiles of array accesses is itself a difficult problem, and the approach is currently based on heuristics developed by observing interesting patterns.
There are a number of approaches that verify array programs without inferring quantified invariants explicitly. A straightforward way is to smash all array elements into a single memory location [4], but it is quite imprecise. Every array element might also be considered a separate variable, but it is not possible with unknown array sizes. There are also techniques that abstract an array to a fixed number of elements, e.g. kdistinguished cell abstraction [32, 33] and kshrinkability [24, 29]. Such abstractions usually reduce array modifying loops with unknown bounds to a known, small bound. It may even be possible to get rid of such loops altogether, by accelerating (computing transitive closures of) transition relations involving array updates in that loop [7]. Along similar lines, VIAP [35] resorts to reasoning with recurrences instead of loops. It translates the input program, including loops, to a set of firstorder axioms, and checks if they derive the property. But all these techniques do not obtain quantified invariants explicitly, unlike ours. Besides, many of these transformations produce an abstraction of the original program, i.e., they do not preserve safety.
Alternatively, there are approaches that use sufficiently expressive templates to infer quantified invariants over arrays [5, 21, 27]. However, the templates need to be supplied manually. For instance, [6] uses a template space of quantified invariants and reduces the problem to quantifierfree invariant generation. Thus, universally quantified solutions for unknown predicates in a CHC system may be obtained by extending a generic CHC solver to handle quantified predicates. Learning need not be limited to usersupplied templates; one may do away with the templates entirely and learn only from examples and counterexamples [18]. Alternatively, [36] chooses a template upfront and refurbishes it with constants or coefficients appearing in the program source. Similarly, [28] proposes to infer array invariants without any user guidance or any userdefined templates or predicates. Their method is based on automatic analysis of predicates that update an array and allows one to generate firstorder invariants, including those that contain alternations of quantifiers. But it does not work for nested loops. By comparison, our technique supports multiple as well as nested loops, enables candidate propagation between loops and, more importantly, generates the grammar automatically from the syntactical constructions appearing in the program’s source.
7 Conclusion
We have presented a new algorithm to synthesize quantified invariants over array variables, systematically accessed in loops. Our algorithm implements an enumerative search that guesses invariants based on syntactic constructions which appear in the code and checks their initiation, inductiveness, and safety with an offtheshelf SMT solver. Key insights behind our approach are that individual accesses to array elements performed in the loop can be generalized to hypotheses about entire ranges, and the existing SMT solvers can be used to validate these hypotheses efficiently. Our implementation on top of a CHC solver FreqHorn confirmed that such strategy is effective on a variety of practical examples. In a vast majority of cases, our tool outperformed competitors and provided checkable guarantees that prevented from reporting false positives.
Footnotes
 1.
Software Verification Competition, http://svcomp.sosylab.org/.
 2.
Thus, we explicitly require guards of loops to have the forms of an inequality, which is the most common array access pattern.
 3.
The source code and benchmarks are available at https://github.com/grigoryfedyukovich/aeval/tree/rnd.
 4.
 5.
The time taken for every benchmark is available at: http://bit.ly/2VS5Mtf.
Notes
Acknowledgements
This work was supported in part by NSF Grant 1525936. Any opinions, findings, and conclusions expressed herein are those of the authors and do not necessarily reflect those of the NSF.
References
 1.Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 46–61. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642287176_7CrossRefzbMATHGoogle Scholar
 2.Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an accelerationbased verification framework for array programs. In: Cassez, F., Raskin, J.F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 18–23. Springer, Cham (2014). https://doi.org/10.1007/9783319119366_2CrossRefzbMATHGoogle Scholar
 3.Alur, R., et al.: Syntaxguided synthesis. In: FMCAD, pp. 1–17. IEEE (2013)Google Scholar
 4.Bertrane, J., et al.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Program. Lang. 2(2–3), 71–190 (2015)CrossRefGoogle Scholar
 5.Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant Synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540697381_27CrossRefGoogle Scholar
 6.Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642388569_8CrossRefGoogle Scholar
 7.Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 157–172. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642026584_15CrossRefzbMATHGoogle Scholar
 8.Bradley, A.R.: SATbased model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642182754_7CrossRefGoogle Scholar
 9.Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs by tiling. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 428–449. Springer, Cham (2017). https://doi.org/10.1007/9783319667065_21CrossRefGoogle Scholar
 10.Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL, pp. 105–118 (2011)Google Scholar
 11.Darke, P., et al.: VeriAbs: verification by abstraction and test generation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part I. LNCS, vol. 10806, pp. 457–462. Springer, Cham (2018). https://doi.org/10.1007/9783319899633_32CrossRefGoogle Scholar
 12.de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540788003_24CrossRefGoogle Scholar
 13.Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246–266. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642119576_14CrossRefzbMATHGoogle Scholar
 14.Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125–134. IEEE (2011)Google Scholar
 15.Fedyukovich, G., Bodík, R.: Accelerating syntaxguided invariant synthesis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part I. LNCS, vol. 10805, pp. 251–269. Springer, Cham (2018). https://doi.org/10.1007/9783319899602_14CrossRefGoogle Scholar
 16.Fedyukovich, G., Kaufman, S., Bodík, R.: Sampling invariants from frequency distributions. In: FMCAD, pp. 100–107. IEEE (2017)Google Scholar
 17.Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained horn clauses using syntax and data. In: FMCAD, pp. 170–178. IEEE (2018)Google Scholar
 18.Garg, P., Löding, C., Madhusudan, P., Neider, D.: Learning universally quantified invariants of linear data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 813–829. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642397998_57CrossRefGoogle Scholar
 19.Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642142031_3CrossRefGoogle Scholar
 20.Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL, pp. 338–350 (2005)Google Scholar
 21.Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235–246. ACM (2008)Google Scholar
 22.Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248–266. Springer, Cham (2018). https://doi.org/10.1007/9783030010904_15CrossRefGoogle Scholar
 23.Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: PLDI, pp. 339–348 (2008)Google Scholar
 24.Jana, A., Khedker, U.P., Datar, A., Venkatesh, R., Niyas, C.: Scaling bounded model checking by transforming programs with arrays. In: Hermenegildo, M.V., LopezGarcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 275–292. Springer, Cham (2017). https://doi.org/10.1007/9783319631394_16CrossRefGoogle Scholar
 25.Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540733683_23CrossRefGoogle Scholar
 26.Komuravelli, A., Gurfinkel, A., Chaki, S.: SMTbased model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17–34. Springer, Cham (2014). https://doi.org/10.1007/9783319088679_2CrossRefGoogle Scholar
 27.Kong, S., Jung, Y., David, C., Wang, B.Y., Yi, K.: Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 328–343. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642171642_23CrossRefGoogle Scholar
 28.Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–485. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642005930_33CrossRefGoogle Scholar
 29.Kumar, S., Sanyal, A., Venkatesh, R., Shah, P.: Property checking array programs using loop shrinking. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part I. LNCS, vol. 10805, pp. 213–231. Springer, Cham (2018). https://doi.org/10.1007/9783319899602_12CrossRefGoogle Scholar
 30.Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540246220_22CrossRefGoogle Scholar
 31.Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 282–299. Springer, Heidelberg (2015). https://doi.org/10.1007/9783662460818_16CrossRefGoogle Scholar
 32.Monniaux, D., Alberti, F.: A simple abstraction of arrays and maps by program translation. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 217–234. Springer, Heidelberg (2015). https://doi.org/10.1007/9783662482889_13CrossRefGoogle Scholar
 33.Monniaux, D., Gonnord, L.: Cell morphing: from array programs to arrayfree horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361–382. Springer, Heidelberg (2016). https://doi.org/10.1007/9783662534137_18CrossRefGoogle Scholar
 34.Prabhu, S., Madhukar, K., Venkatesh, R.: Efficiently learning safety proofs from appearance as well as behaviours. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 326–343. Springer, Cham (2018). https://doi.org/10.1007/9783319997254_20CrossRefGoogle Scholar
 35.Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Piskac, R., Rümmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 38–49. Springer, Cham (2018). https://doi.org/10.1007/9783030035921_3CrossRefGoogle Scholar
 36.Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 88–105. Springer, Cham (2014). https://doi.org/10.1007/9783319088679_6CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.