1: \begin{abstract}

2:   Automated program verification is a difficult problem. It is

3:   undecidable even for transition systems over Linear Integer

4:   Arithmetic (LIA). Extending the transition system with theory of Arrays,

5:   further complicates the problem by requiring inference and reasoning

6:   with universally quantified formulas. In this paper, we present a

7:   new algorithm, \textsc{Quic3}, that extends IC3 to infer universally

8:   quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3

9:   or an SMT solver as a black box, \textsc{Quic3} carefully manages

10:   quantified generalization (to construct quantified invariants) and

11:   quantifier instantiation (to detect convergence in the presence of

12:   quantifiers). While \textsc{Quic3} is not guaranteed to converge, it

13:   is guaranteed to make progress by exploring longer and longer

14:   executions. We have implemented \textsc{Quic3} within the Constrained

15:   Horn Clause solver engine of Z3 and experimented with it by applying

16:   \textsc{Quic3} to verifying a variety of public benchmarks of array

17:   manipulating C programs.

18: \end{abstract}

19: