1: \begin{abstract}

2:   We present an SMT-based symbolic model checking algorithm for safety

3:   verification of recursive programs.

4: %

5:   The algorithm is modular and analyzes procedures individually.

6:   Unlike other SMT-based approaches, it maintains both

7:   \emph{over-} and \emph{under-approximations} of procedure

8:   summaries. Under-approximations are used to analyze procedure calls without

9:   inlining. Over-approximations are used to block

10:   infeasible counterexamples and detect convergence to a proof.

11: %

12:   We show that for programs and properties over a decidable theory, the algorithm

13:   is guaranteed to find a counterexample, if one exists. However, efficiency

14:   depends on an oracle for quantifier elimination (QE). % Given such an

15:   % oracle, the queries for individual procedures and the inferred

16:   % approximations of the summaries depend only on the variables in

17:   % scope.

18:   % This makes the algorithm significantly more efficient than

19:   % existing

20:   % SMT-based algorithms which unroll the call-graph.

21: %

22:   For Boolean Programs, the algorithm is a polynomial decision

23:   procedure, matching the worst-case bounds of the best BDD-based

24:   algorithms.

25: %

26:   For Linear Arithmetic (integers and rationals), we give an efficient

27:   instantiation of the algorithm by applying QE \emph{lazily}.  We use

28:   existing interpolation techniques to over-approximate QE and

29:   introduce \emph{Model Based Projection} to under-approximate QE.

30: %

31:   Empirical evaluation on SV-COMP benchmarks shows that our algorithm

32:   improves significantly on the state-of-the-art.

33: \end{abstract}

34: