Explaining the Effectiveness of Small Refinement
Heuristics in Program Verification with CEGAR
Tachio Terauchi
JAIST
terauchi@jaist.ac.jp

Abstract. Safety property (i.e., reachability) verification is undecidable for Turing-complete programming languages. Nonetheless, recent
progress has lead to heuristic verification methods, such as the ones
based on predicate abstraction with counterexample-guided refinement(CEGAR), that work surprisingly well in practice. In this paper, we investigate the effectiveness of the small refinement heuristic which, forabstraction refinement in CEGAR, uses (the predicates in) a small proofof the given counterexample’s spuriousness [12, 3, 17, 22]. Such a method
has shown to be quite effective in practice but thus far lacked a theoretical backing. Our core result is that the heuristic guarantees certain
bounds on the number of CEGAR iterations, relative to the size of a
proof for the input program.

1

Introduction

The safety property (i.e., reachability) verification problem asks, given a program, if an error state (e.g., given as a line number in the program text) is
unreachable for every execution of the program. The problem is undecidable forTuring-complete programming languages (and intractably hard for many naturaldecidable fragments – e.g., PSPACE-complete for Boolean programs). Despite
the staggering complexity, recent research has lead to heuristic verification methods that work surprisingly well in practice. They have been used to verify nontrivial real-world programs such as operating system device drivers [4, 11], andthe yearly held software verification competition [1] shows an ever increasing variety of programs efficiently verified by the state-of-the-art automated software
verifiers. By contrast, there has been comparatively less progress on explaining why such heuristics work. As a step toward bridging the gap, we presenta theoretical explanation for the effectiveness of a heuristic used in predicate
abstraction with counterexample-guided refinement (CEGAR).
CEGAR is a verification method that iteratively updates a finite set of predicates from some first-order logic (FOL) theory, called the candidate predicate set,
until the candidate set forms a sufficient proof of the given program’s safety (i.e.,
an inductive invariant). In each iteration, a process called abstraction checks if
the current candidate set is sufficient, and if not, a counterexample is generated.
A process called refinement infers a proof of the counterexample’s safety (i.e.,spuriousness) whereby the predicates in the proof are added as new candidates,
and the iteration repeats.
In general, there is more than one proof that refutes the same counterexample, and which proof is inferred by the refinement process can significantly
affect the performance of the overall verification process (cf. Section 2.2 for an
example). A heuristic often used in practice is to infer a small proof (e.g., measured by the sum of the syntactic size of the predicates), and researchers haveproposed methods for inferring a small proof of the given counterexample’s spuriousness [12, 3, 17, 22].1 This paper analyzes the effect such a small refinement
heuristic has on the overall verification performance.
As safety property verification is undecidable, we cannot establish any (finitary) complexity result without some assumption on the input problem instances.
In general, we will state our results relative to the size of a proof of safety for the
input program, and we will try to show that the verification converges quickly
assuming that the input program has a small proof (e.g., polynomial in the sizeof the program). The assumption captures the conventional wisdom that correct
programs are often correct for simple reasons, per Occam’s razor.
Overview of the Main Results. We formalize the small refinement heuristic
to be a refinement process that infers a proof of size at most polynomial inthat of the smallest proof for the given counterexample. Let CegVerifSR bea CEGAR verification with such a refinement process. Let mpfsize(P ) be thesize of the smallest proof of safety for a program P . Our first main result is thefollowing.
Theorem 1. CegVerifSR converges in at most exp(mpfsize(P )) many CEGAR iterations given a program P .
Theorem 1 implies that CegVerifSR is able to verify a program in an exponential number of iterations under the promise that the program has a polynomial
size proof of safety. We prove Theorem 1 under a rather general setting.
Next, we consider a more concrete setting where a program is represented bya control flow graph (CFG) such that the program’s proof is a Floyd-style nodewise inductive invariant [9], the abstraction process uses the Cartesian predicate
abstraction, and the size of a proof is measured by the sum of the syntactic
size of the predicates. We also assume that counterexamples are generated byunfolding each loop an arbitrary but the same number of times (copies of nested
subloops are also unfolded the same number of times) which we show to be
sufficient for the setting (cf. Theorem 9). Under such a setting, we show that
CegVerifSR converges in at most poly(mpfsize(P ))maxhds(P ) many iterations
where maxhds(P ) is the maximum number of loop entries per loop of the CFG(e.g., maxhds(P ) ≤ 1 for reducible CFGs) (Theorem 10). The result implies that,
under such a setting, CegVerifSR is able to verify a program with a constantnumber of loop entries per loop in a polynomial number of iterations under thepromise that the program has a polynomial size proof of safety.
1

In this paper, a “proof” is a set of predicates. Note that this differs from the notionof proofs and proof sizes used in proof complexity [6].

The rest of the paper is organized as follows. We discuss related work next.
Section 2 gives preliminary definitions pertaining to generic CEGAR verification and proves the first main result (Theorem 1). Section 3 gives additional
preliminary definitions pertaining to CFG programs and proves the main result
on CFG programs (Theorem 10). We discuss some limitations of our results in
Section 4, and conclude the paper in Section 5. Appendix contains the proofs
and extra materials omitted from the main body of the paper.
Related Work. Previous works on the small refinement heuristic [12, 3, 17, 22]have presented empirical evidences of the heuristic’s effectiveness in the formof experiments. To our knowledge, this paper is the first work on a theoreticalexplanation for the heuristic’s effectiveness.
A related but somewhat different heuristic proposed for CEGAR is the stratified refinement approach [13, 15, 20] where the proofs inferred in each refinement
step is restricted to some finite set of proofs that is enlarged when the refinement
fails to find a proof in the current set. The proof set is enlarged in such a way
to ensure that the growing strata of proof sets eventually cover the underlying(possibly infinite) space of possible proofs. The stratified approach ensures aneventual convergence of CEGAR iterations under the promise that a proof ofthe program’s safety exists in the underlying proof space, but the previous works
give no results on the iteration bound.

2

Iteration Bound Under a Generic Setting

2.1

Preliminaries

Formulas and Predicates. We write finite sequences in boldface (e.g., x for
x1 , . . . , xn ). Let T be a FOL theory. A term a and formula φ in the signature of
T is defined as follows.
term a ::= x | f (a)formula φ ::= p(a) | ¬φ | φ ∧ φ′ | φ ∨ φ′ | φ ⇒ φ′ | ∃x.φ | ∀x.φ
Here, x is a variable, f is an arity |a| function symbol, and p is an arity |a|predicate symbol of T . As usual, ⇒ binds weaker than ∧ or ∨. For a formula φ,we write fv(φ) for the set of free variables in φ. A predicate in T is of the form
λx.φ where φ is a formula such that {x} = fv(φ). We often omit the explicit
λ abstraction and treat a formula φ as the predicate λx.φ where {x} = fv(φ).
We overload T for the set of predicates in T , and write T (x) for the set of T predicates of arity |x|. We write |=T φ if φ is valid in T . We write ⊤ for tautology
and ⊥ for contradiction. (Note that the term “predicate” is not limited to justatomic predicates as sometimes is in the literature on CEGAR.)
Generic CEGAR. To state Theorem 1 for a general setting, following the styleof [20], we give a definition of CEGAR in terms of generic properties that abstraction and refinement processes are assumed to satisfy, but without specifying
exactly when predicates form a proof of a program or how counterexamples are1: procedure CegVerif(P )2: Cands := ∅;4: repeat3:
match Abs(P ,Cands) with4:
safe → return safe
5:| π → match Ref(π) with
6:
unsafe → return unsafe
7:| F → Cands := Cands ∪ F
8: end repeat
Fig. 1. CegVerifgenerated and refuted (we concretize such notions for CFG programs in Section
3.1).
In general, a counterexample is an “unwound” slice of the given program andis itself considered a program (typically, without loops or recursion). Let γ range
over programs and counterexamples. For a finite set of predicates F ⊆ T , wewrite F ⊢ γ to mean that F is a proof of safety of γ. We often simply say that F isa proof of γ when F ⊢ γ (i.e., omitting “of safety”), and if γ is a counterexample
in addition, we sometimes say that F refutes γ, or F is a proof of spuriousnessof γ. We require the proof relation ⊢ to be monotonic on the predicate set, thatis, if F ⊢ γ and F ⊆ F ′ , then F ′ ⊢ γ (i.e., having more predicates can only
increase the ability to prove). We use F , F ′ , F1 , etc. to range over finite sets ofpredicates.
Figure 1 shows the overview of the verification process. CegVerif takes as
input the program P be be verified, and initializes the candidate predicate set
Cands to ∅ (line 2). Then, it repeats the abstract-and-refine loop (lines 4-8) untilconvergence. Abs is the abstraction process which takes as input a program and afinite set of T -predicates. For a program P and a finite F ⊆ T , Abs(P, F ) either
returns safe, indicating that P has been proved safe using the predicates from F ,or returns a counterexample. In the former case, the verification process halts,
returning safe. Ref is the refinement process, which, given a counterexample π,either returns a proof of π’s safety, or detects that π is irrefutable and returns
unsafe. In the former case, the proof is added to the candidates, and in latter case,the verification halts by returning unsafe. For a run of CegVerif, the number of
CEGAR iterations is defined to be the number of times the abstract-and-refine
loop (lines 4-8) iterated.
We state the required assumptions on the abstraction and refinement processes. We require that if F ⊢ γ then Abs(γ, F ) = safe, and that if Abs(P, F )returns a counterexample π then Abs(π, F ) 6= safe (i.e., Abs proves the safety ofthe program given a sufficient set of predicates, and otherwise returns a counterexample that it cannot prove safe with the given predicates). We also requirethat if F ⊢ P and Abs(P, F ′ ) returns π, then F ⊢ π (i.e., a proof for a programis also a proof for any counterexample of the program). We require that Abs issound in that it only proves safe programs safe, that is, Abs(γ, F ′ ) = safe only if∃F ⊆ T .F ⊢ γ. For the refinement process Ref, we require that Ref(π) returns
F only if F ⊢ π (i.e., the returned proof is actually a proof for the counterexample), and that Ref(π) returns unsafe only if ∀F ⊆ T .F 6⊢ π (i.e., only irrefutablecounterexamples are detected irrefutable). Finally, we require Abs and Ref tohalt on all inputs. We note that these assumptions are quite weak and satisfied
by virtually any CEGAR verifiers.2
It is easy to see that CegVerif is sound in that it only proves safe programs
safe.
Theorem 2 (Soundness). CegVerif(P ) returns safe only if ∃F ⊆ T .F ⊢ P .
Note that Theorem 2 says nothing about how fast (or whether) CegVerifconverges. The main results of the paper (Theorems 1 and 10) show that, when
Ref is made to return a small proof of the given counterexample, CegVerif isguaranteed to converge in a number of iterations bounded by the size of a proof
for the given program.
It is also easy to see that CegVerif is “complete” in the sense that it only
detects unprovable programs unprovable.
Theorem 3 (Completeness). CegVerif(P ) returns unsafe only if ∀F ⊆T .F 6⊢ P .
Since the paper is only concerned with analyzing the behavior of CEGAR when
given a provably safe program, in what follows, we disregard the situation where
the given program is unprovable with the predicates from the background theory.
2.2

Main Result

To demonstrate the usefulness of 1: int a = ndet(); int b = ndet();the small refinement heuristic, we 2: int x = a; int y = b; int z = 0;start with an example on which 3: while (ndet()) {4:
y++;z++;
CegVerif (without the heuris- 5: }tic) may fail to converge despite 6: while (z != 0) {the program having a small proof 7: y--;z--;8: }of safety (taken from [20]). Fig- 9: assert (a!=b || y=x);
ure 2 shows the program Pex . Here,Fig. 2. Pex
ndet() returns a non-deterministic
integer. The goal is to verify thatthe assertion failure is unreachable, that is, a = b ⇒ y = x whenever line 9 isreached. We define a proof of the program to be the set of predicates that canbe used as loop invariants at each of the loop heads (lines 3 and 6) and are sufficient to prove the unreachability (i.e., “safe” inductive invariant). For example,
a possible proof is the singleton set Finv = {a = b ⇒ y = x + z}.
2

We do not impose F ⊢ P ⇔ Abs(P, F ) = safe to allow modeling verifiers whose
abstraction process can prove more from the same predicates than the refinement
process (cf. Section 3.1).

1: int a=ndet(); int b=ndet();2: int x=a; int y=b; int z=0;
3: if (ndet()) {4:
y++;z++;
5: }6: if (z!=0) {7:y--;z--;
8: }9: assert (a!=b||y=x);

1: int a=ndet(); int b=ndet();2: int x=a; int y=b; int z=0;
3: if (ndet()) {4:
y++;z++;
5: }6: if (ndet()) {7:
y++;z++;
8: }9: if (z!=0) {10:
y--;z--;
11: }12: if (z!=0) {13:
y--;z--;
14: }15: assert (a!=b||y=x);π1π2Fig. 3. Counterexamples of Pex

Running CegVerif on the program, Abs may return the counterexample π1
shown in Figure 3 in the first iteration, obtained by unfolding each loop once.
Viewing the unfolded if statements at lines 3 and 6 as one-iteration loops, it
can be seen that Finv is a proof of π1 ’s safety. Thus, Ref(π1 ) may return Finv ,which is also a proof for Pex and would allow CegVerif to converge in the next
iteration.
Unfortunately, the refinement process is not guaranteed to return Finv but
may choose any set of predicates that forms a proof of π1 ’s safety. For example,
another possibility is F1 = {φ0 , φ1 , φ0 ∨ φ1 } whereφ0 ≡ x = a ∧ y = b ∧ z = 0
φ1 ≡ x = a ∧ y = b + 1 ∧ z = 1
Adding F1 to the candidates is sufficient for proving the safety of π1 but notthat of Pex , and so the abstraction process in the subsequent iteration would
return yet another counterexample. For example, it may return π2 shown in
Figure W
3 obtained by unfolding each loop twice. Then, Ref may choose the proof
F2 = { F | F ⊆ {φ0 , φ1 , φ2 }} where φ2 ≡ x = a ∧ y = b + 2 ∧ z = 2 to prove thespuriousness of this new counterexample, which is still insufficient for proving
Pex . The abstract-and-refine loop may repeat
indefinitely in this manner, addingW
to the candidates the predicates Fk = { F | F ⊆ {φi | 0 ≤ i ≤ k}} where φi ≡x = a ∧ y = b + i ∧ z = i in each k-th run of the refinement process.
Here, a key observation is that Finv is a proof of safety for every counterexample π1 , π2 , . . . of Pex . Because the size of Finv is “small” (under a suitable
proof size metric – made more precise below), when using the small refinement
heuristic, the refinement process would have to infer Finv (or other small proof
of Pex ) before producing a large number of incorrect proofs (such as F1 , F2 , . . . ).
Our first main result, Theorem 1, states that the above observation holds ingeneral. The result can be proved for a rather generic notion of proof size. We

assumed that size(·) satisfies the following: there is a constant c > 1 such thatfor all n ≥ 0, |{F ⊆ T | size(F ) ≤ n}| ≤ cn (i.e., there are at most cn proofs ofsize less than or equal to n). We call such a proof size metric generic. The size ofthe smallest proof for γ, mpfsize(γ), is defined to be minF ∈{F ⊆T |F ⊢γ} size(F ).
Definition 1 (Small Refinement Heuristic). We define CegVerifSR to be
CegVerif with the refinement process Ref satisfying the following property:
there is a polynomial f such that for all π and F , if Ref(π) returns F thensize(F ) ≤ f (mpfsize(π)) (i.e., the refinement process returns proofs of size polynomially bounded in that of the smallest proof for the given counterexample).
We are now ready to prove Theorem 1.
Theorem 1. Let the proof size metric be generic. Then, CegVerifSR converges
in at most exp(mpfsize(P )) many CEGAR iterations given a program P .
We informally describe the intuition behind the result. First, as remarked
above, a proof of a program is also a proof of any of its counterexamples. Therefore, under the small refinement heuristic, the inferred proof in each refinement
step is at most polynomially larger than the smallest proof of the program. Then,the result follows from the definition of the generic proof size metric and the factthat the proofs inferred in the refinement process runs must be distinct.

3

Iteration Bound for CFG-Represented Programs

The exponential bound shown in Theorem 1 still seems to have a gap fromthe performance observed with using the small refinement heuristic in practice.
The observation is the motivation for studying a more concrete setting such as
CFG-represented programs.
3.1

Preliminaries

Graphs. A finite directed graph G = (V, E) consists of a finite set of nodes
V and edges E ⊆ V ×V . We write v (G) for V and e(G) for E. For an edgee = (v, v ′ ), we write sc(e) for v (the source of e) and tg(e) for v ′ (the target ofe). Since we only work with finite directed graphs, in what follows, we omit theadjectives and simply write graphs.
We write G \ E for (v (G), e(G) \ E), and G \ V for (V ′ , e(G) ∩ V ′ ×V ′ ) where′V = v (G) \ V . For E ⊆ v (G)×v (G), we write G ∪ E for (v (G), e(G) ∪ E). A
path of G is a finite sequence nodes ̟ = v1 v2 . . . vn such that (vi , vi+1 ) ∈ e(G)for each i ∈ {1, . . . , n − 1}. We write |̟| for the length of ̟ and ̟(i) for thei-th node visited (i.e., ̟ = ̟(1)̟(2) . . . ̟(|̟|)).
CFG Programs. We consider programs represented by control flow graphs(also known as control flow automata [5]). Formally, a control flow graph (CFG)
is a tuple (G, T, vini , verr ) where G is a graph, vini ∈ v (G) is the initial node,verr ∈ v (G) is the error node, and T : e(G) → T (x, x′ ) is the transition

relation where |x| = |x′ |. Roughly, each v ∈ v (G) represents a program location (e.g., a basic block), and for e ∈ E, T (e)(x, x′ ) expresses the statetransition from the location sc(e) to tg(e) where x (resp. x′ ) represents thevalues of the program variables before (resp. after) the transition. A path of
the CFG is a path of G. Without loss of generality, we assume that vini has
no incoming edges, verr has no outgoing edges, and all nodes are reachable
from vini . Let Vals be the set of values. The set of states of the program isStates = Vals|x| . The set of states reached from S ⊆ States by taking an edgee ∈ e(G) is defined to be Post T [e](S) = {s′ ∈ States | s ∈ S∧ |=T T (e)(s, s′ )}.
The set of states reached from S ⊆ States by taking a path ̟, Post ∗T [̟](S), is
defined inductively as Post ∗T [v1 v2 ̟](S) = Post ∗T [v2 ̟](Post T [(v1 , v2 )](S)) andPost ∗T [v](S) = Post ∗T [ε](S) = S.
We say that a program P = (G, T, vini , verr ) is safe if for all paths ̟ of P
such that ̟(1) = vini and ̟(|̟|) = verr , Post ∗T [̟](States) = ∅. In what follows,
we often implicitly assume that |x, x′ | is the arity of the predicates in the rangeof the transition relation of the CFG being discussed where x and x′ are distinct
variables such that |x| = |x′ |.
We note that the class of CFG programs is already Turing complete when T
is the set of quantifier-free predicates in the theory of linear rational arithmetic(QFLRA – quantifier-free theory of linear rational arithmetic) (and is equivalent
to Boolean programs when T is propositional), taking the reachable states fromStates as the computation result. Checking the safety of CFG programs when
T = QFLRA is undecidable.
Loops. We review the notion of loops in a CFG [2]. A loop decomposition of G
is a set {L0 , . . . , Ln } with each Li = (Gi , hdsi ) satisfying 1.) G0 = G, 2.) each
Gi , Gj are either disjoint or one is a subgraph of the other, 3.) each hdsi , hdsj
for i 6= j are disjoint, and 4.) each Li satisfies the following:– Gi is a non-empty subgraph of G;SS– Gi \ ({e ∈ e(Gi ) | tg(e) ∈ hdsi } ∪ j∈Sub(i) e(Gj )) ∪ j∈Sub(i) flatten(Gi , Gj )is acyclic;– hdsi = {v ∈ v (Gi ) | v ′ ∈/ v (Gi ) ∧ (v ′ , v) ∈ e(G)}; and– Gi is strongly connected except for G0
where flatten(Gi , Gj ) = {(sc(e1 ), tg(e2 )) | e1 ∈ e(Gi ) ∧ e2 ∈ e(Gi ) ∧ tg(e1 ) ∈v (Gj ) ∧ tg(e2 ) ∈ v (Gj )} (i.e., the edges formed by “flattening” Gj in Gi ) andSub(i) = {j | Gj is a proper subgraph of Gi }.
Roughly, each loop Li is a subgraph of G comprising the “back edges” Bi ={e ∈ e(Gi ) | tg(e) ∈ hdsi } that take the control flow back to one of the loop
entries, and the “loop body” Gi \ Bi that is acyclic when the nested subloops
are flattened. Note that the loop entries hdsi are the nodes in Gi with incomingedges from nodes outside of the loop. A loop decomposition forms a tree with
L0 as the root and nested subloops as children.3
3

In the literature, L0 is typically not treated as a loop, and a loop decomposition
forms a forest.

A graph is rooted if there is a node with no incoming edges and from which
every node in the graph is reachable. Clearly, the graph underlying a CFG isrooted. The following is a folk theorem (cf. Appendix A.4 for a proof).
Theorem 4. A rooted graph has a loop decomposition.
We define a loop decomposition of a CFG (G, T, vini , verr ) to be a loop decomposition of G. In the following, we assume that each CFG P is associated with
its loop decomposition loops(P ) (e.g., constructed by the algorithm given in Appendix A.4). We write maxhds(P ) for max( ,hds)∈loops(P ) |hds|. We remark that
maxhds(P ) ≤ 1 if P is reducible [2].
Proofs and Counterexamples for CFG Programs. Informally, a counterexample of a CFG is an acyclic CFG obtained by unfolding the loops of the
CFG. To formalize loop unfolding, we introduce a simple graph grammar below.
instr ::= v0 7→ (φ1 :v1 , φ2 :v2 , . . . , φn :vn )t ::= ∅ | {instr} | t1 ∪ t2 | loop (h1 , . . . , hm ) t
Here, in each instruction v0 7→ (φ1 : v1 , . . . , φn : vn ), v1 , . . . , vn are distinct andφi ∈ T (x, x′ ) for each i ∈ {1, . . . , n}. We call v0 the source and v1 , ..., vn thetargets of the instruction. Roughly, v0 7→ (φ1 :v1 , . . . , φn :vn ) expresses the set ofedges {(v0 , v1 ), . . . , (v0 , vn )} such that the transition relation of (v0 , vi ) is φi . A
term t expresses the CFG comprising the edges represented by the instructions
occurring in t. The loop annotations mark subparts of the CFG that correspondto loops, so that loop (h) t expresses a loop with h being the entry nodes and t
representing the union of the loop body, the back edges, and the edges from theloop body to the outer loops. We require the sources of the instructions occurringin a term to be distinct. We refer to Appendix B for the formal correspondence
between CFGs and graph grammar terms. In what follows, we equate a CFG
with the corresponding graph grammar term.
We overload t for the set of instructions occurring in t. We let sc(v0 7→ (φ1 :v1 , . . . , φn : vn ))S = {v0 }, and tg(v0 7→ (φ1 : vS1 , . . . , φn : vn )) = {v1 , . . . , vn }.
We let sc(t) = instr ∈t sc(instr ), and tg(t) = instr ∈t tg(instr ). We let v (t) =sc(t) ∪ tg(t). For sets of nodes V1 and V2 , we write thV1 , V2 i for t with eachsource occurrence of v ∈ V1 replaced by ‘v and each target occurrence of v ∈ V2
replaced by ‘v. For instance, for t = {v0 7→ (⊤:v1 , ⊤:v2 ), v1 7→ (⊤:v0 , ⊤:v3 )},th{v0 }, {v1 , v3 }i = {‘v0 7→ (⊤:‘v1 , ⊤:v2 ), v1 7→ (⊤:v0 , ⊤:‘v3 )}. We write t\V fort with each instruction v0 7→ (v1 : φ1 , . . . , vn : φn ) replaced by v0 7→ (vi1 :φi1 , . . . , vim :φim ) where {vi1 , . . . , vim } = {v1 , . . . , vn }\V , treating an instruction
with empty targets as ∅. For h = h1 , . . . , hn , we write ‘h for ‘h1 , . . . , ‘hn .
Let rewriting contexts be defined as follows.
C ::= [ ] | C ∪ t | loop (h1 , . . . , hm ) C
Loop unfolding is defined by the following rewriting rules.
C[loop (h) t] 99K C[thv (t)\{h}, sc(t)i ∪ loop (‘h) th{h}, {h}i]C[loop (h) t] 99K C[t\{h}]The first rule unfolds the loop once, whereas the second rule “closes” the loop byremoving the back edges. We formalize the counterexamples of a CFG P , cex(P ),to be the acyclic CFGs obtained by applying the above rewriting an arbitrary
number of times, that is, cex(P ) = {π | P 99K∗ π ∧ π is acyclic}.
A proof of a CFG program or counterexample is a set of predicates that
forms a Floyd-style node-wise inductive invariant [9]. More formally, we say thatσ : v (G) → T (x) is a node-wise inductive invariant of γ = (G, T, vini , verr ),written σ ⊢cfg γ, if 1.) σ(vini ) = ⊤, 2.) σ(verr ) = ⊥, and 3.) for each e ∈ e(G),|=T σ(sc(e))(x) ∧ T (e)(x, x′ ) ⇒ σ(tg(e))(x′ ). We say that F is a proof of γ,
written F ⊢cfg γ, if there exists σ : v (G) → F ∪ {⊥, ⊤} such that σ ⊢cfg γ. The
following are immediate from the definition of ⊢cfg .
Theorem 5 (Soundness of ⊢cfg ). If F ⊢cfg γ then γ is safe.
Theorem 6 (Monotonicity of ⊢cfg ). If F ⊢cfg γ and F ⊆ F ′ , then F ′ ⊢cfg γ.
Theorem 7. Suppose F ⊢cfg P . Then, for any π ∈ cex(P ), F ⊢cfg π.
Theorems 5, 6 and 7 justify us to use ⊢cfg for the proof relation ⊢ of CegVerif(cf. Section 2.1).
Next, we concretize the abstraction process and counterexample generation
for CFGs. We present the Cartesian predicate abstraction, a form of predicate
abstraction used in CEGAR, as the abstraction process. Then, we present a
counterexample set that is sound for the abstraction process to generate andrefute (made precise below). We note that, because our result is shown for the
Cartesian predicate abstraction, it also holds for stronger abstraction processes
such as the Boolean predicate abstraction.
V
We write F ∧ for the ∧-closureof F (i.e., { F ′ | F ′ ⊆ F }) and F ∧∨ forW ′the ∧∨-closure of F (i.e., { F | F ′ ⊆ F ∧ }). We write F⊥ for F ∪ {⊥}. For
γ = (G, T, vini , verr ), σ : v (G) → T , and F ⊆ T , we say that σ is a F -Cartesianif 1.)
predicate abstraction node-wise inductive invariant of γ, written σ ⊢F
crt γ, Wσ(vini ) = ⊤,W2.) σ(verr ) = ⊥, and 3.) for each e ∈ e(G), we have σ(sc(e)) = F1 ,σ(tg(e)) = F2 for some F1 ⊆ F⊥ ∧ and F2 ⊆ F⊥ ∧ such that for each φ ∈ F1 ,there is ψ ∈ F2 where |=T φ(x)∧T (e)(x, x′ ) ⇒ ψ(x′ ). We write F ⊢crt γ if there
exists σ such that σ ⊢F
crt γ. Clearly, F ⊢cfg γ implies F ⊢crt γ, and F ⊢crt γ
implies F ∧∨ ⊢cfg γ.
The Cartesian predicate abstraction abstraction process Abscrt (·, F ) is an abstract interpretation [7] over the finite lattice (F ∧∨ , |=T · ⇒ ·) with the abstractstate transformer αF (Post ) that computes the strongest cube over F⊥ impliedin the next state (from the initial abstract state ⊤):V
αF (Post )T [e](φ) = {ψ ∈ F⊥ | |=T φ(x) ∧ T (e)(x, x′ ) ⇒ ψ(x′ )}The abstraction process guarantees 1.) F ⊢crt γ if and only if Abscrt (γ, F ) returns
safe, and 2.) if Abscrt (P, F ) returns a counterexample π, then F 6⊢crt π.
We show that Abscrt satisfies the requirements of the abstraction process
given in Section 2.1.

Theorem 8. Abscrt satisfies the requirements for Abs. That is,– If F ⊢cfg γ then Abscrt (γ, F ) = safe;– If Abscrt (γ, F ) returns π then Abscrt (π, F ) 6= safe;– If F ⊢cfg P and Abscrt (P, F ′ ) returns π then F ⊢cfg π; and– If Abscrt (γ, F ) = safe then ∃F ′ ⊆ T .F ′ ⊢cfg γ.
We say that the set of counterexamples X (P ) ⊆ cex(P ) is sound for Abs if
Abs(P, F ) 6= safe implies that there exists π ∈ X (P ) such that F 6⊢cfg π (i.e.,
generating and refuting only the counterexamples from X (P ) is sufficient forverifying P ). We say X is sound for Abs if X (P ) is sound for Abs for each P .
Let cexsyn (P ) ⊆ cex(P ) be the set of counterexamples obtained by unfolding theloops loops(P ) an arbitrary but the same number of times for each loop (copies
of nested subloops are also unfolded the same number of times – cf. Appendix
C for the formal definition). We show that cexsyn is sound for Abscrt .
Theorem 9. cexsyn is sound for Abscrt .
Theorems 8 and 9 justify us to use Abscrt with cexsyn as the counterexample
generator for the abstraction process of CegVerif (cf. Section 2.1).
We note that, in the setting described above, a counterexample can be a general dag-shaped CFG. While early CEGAR verifiers often restricted the counterexamples to paths [4, 11], more recent verifiers also use dag counterexamples,and researchers have proposed methods for inferring small refinements from suchcounterexamples [8, 10, 19, 16, 22]. Also, we note that, when T is QFLRA, checking the provability for a dag CFG γ (i.e., checking if ∃F ⊆ T .F ⊢cfg γ) is
decidable, whereas it is undecidable for an arbitrary (i.e., cyclic) CFG [14].4
3.2

Main Result

We define the syntactic size of
PF to be the sum of the syntactic sizes of thepredicates, that is, size(F ) = φ∈F |φ| where |φ| is the number of (logical andnon-logical) symbols in φ. We state the main result.
Theorem 10. Let the proof size metric be syntactic, ⊢cfg be the proof relation,
and Abscrt be the abstraction process with cexsyn as the counterexample generator. Then, CegVerifSR converges in poly(mpfsize(P ))maxhds(P ) many CEGAR
iterations given a CFG program P .
We informally describe the intuition behind the result by analyzing the behavior of CegVerifSR on the program Pex from Figure 2, treated as a CFG
program. Figure 4 (a) shows the CFG representation of the program. Here, node
1 is the initial node, node 4 is the error node, and the transition relation is asfollows.
φ1 (x, x′ ) ≡ x′ = a′ ∧ y ′ = b′ ∧ z ′ = 0
φ2 (x, x′ ) ≡ z ′ = z + 1 ∧ y ′ = y + 1 ∧ x′ = x ∧ a′ = a ∧ b′ = b
φ3 (x, x′ ) ≡ x′ = x ∧ y ′ = y ∧ z ′ = z ∧ a′ = a ∧ b′ = b
φ4 (x, x′ ) ≡ z 6= 0 ∧ z ′ = z − 1 ∧ y ′ = y − 1 ∧ x′ = x ∧ a′ = a ∧ b′ = b
φ5 (x, x′ ) ≡ z = 0 ∧ a = b ∧ x 6= y
4

The decidability holds for any theory with effective interpolation (cf. Appendix D).

1

I1
I2

21
22

L0

I2kͲ2

1

I3

I

3

I1

L1

I3

2k

I5

2

I3

I2

I4

31

I5
32

L2

I4kͲ2

3

I5

I4

I
3k

5

4
4

(a)

(b)

Fig. 4. (a) CFG representation of Pex and (b) CFG representation of cexsyn (Pex )where x = x, y, z, a, b and x′ = x′ , y ′ , z ′ , a′ , b′ . Pex has two non-root loops L1
and L2 such that L1 corresponds to the first loop (lines 3-5) and L2 corresponds
to the second loop (lines 6-8) of Figure 2. An element of cexsyn (Pex ) is a CFG
of the form shown in Figure 4 (b) where each loop is unfolded k times for somek > 0. Nodes 21 , . . . , 2k (resp. 31 , . . . , 3k ) are the copies of the entry node of L1(resp. L2 ) created by the unfolding.
Recall that the small refinement heuristic returns a proof of size polynomiallybounded in the size of the smallest proof of the given counterexample. Let f be
the polynomial factor (i.e., Ref returns proofs of size at most f (mpfsize(π)) given
a counterexample π). Then, because Finv is a proof of any counterexample ofPex , a proof returned by Ref in a run of CegVerifSR (Pex ) would be of size
at most f (size(Finv )). Consider the counterexample πn ∈ cexsyn (Pex ) obtainedby unfolding each loop n times where n > f (size(Finv )). It can be seen thatany proof F of πn such that size(F ) ≤ f (size(Finv )) must form a Cartesianpredicate abstraction node-wise inductive invariant of Pex (i.e., F ⊢crt Pex ).
This is because for such a F to not be a ⊢crt -proof of Pex , it must assign distinct
predicates to the unfolded loop heads of each loop, but that is not possible when
the proof size must be at most f (size(Finv )).
More generally, as in Theorem 1, the first key observation used to prove
Theorem 10 is the fact that a proof for the program is a proof for any counterexample of the program. As before, this implies that the small refinement
heuristic ensures that the proofs inferred in the refinement are only polynomially larger than the smallest proof for the program. Then, we use the observation

that, for a CFG program, if a counterexample is “sufficiently large”, then any
small proof for the counterexample becomes a Cartesian predicate abstraction
node-wise inductive invariant for the program, and so CEGAR will have to haltin the next iteration. Finally, the iteration bound follows from the number ofcounterexamples in cexsyn that are within such a sufficiently large size.
We remark that it is actually sufficient for the proof size metric to only satisfy
size(F ) ≥ |F | for Theorem 10 to hold (i.e., at least the number of predicates in
F ). Also, as remarked before, the result also holds for stronger abstraction processes such as the Boolean predicate abstraction. Meanwhile, as we shall further
discuss in Section 4, a limitation of the result is that it only considers counterexamples where all loops are unfolded the same number of times. This implies thatthe abstraction process may generate large counterexamples in relatively earlystages of the verification, especially when the program contains nested loops(cf. Appendix C).
We end the section by showing that the proof size metric is crucial to theresult. That is, under the generic proof size metric (cf. Section 2.2), we canonly guarantee an exponential bound (which is ensured by the generic result ofTheorem 1), even when the rest of the setting is left unchanged from Theorem 10.
Theorem 11. Let the proof size metric be generic, ⊢cfg be the proof relation,
and Abscrt be the abstraction process with cexsyn as the counterexample generator. Then, there exists a CFG program P with a proof F ⊢cfg P on which
CegVerifSR may take exp(size(F )) many CEGAR iterations to converge.

4

Limitations

While we believe that the paper’s results are a step toward understanding theeffectiveness of the small refinement heuristic, we still have ways to go to get thewhole picture. Below, we discuss some limitations of our work.
First, we do not account for the cost of the abstraction process and the refinement process (i.e., we only show bounds on the number of CEGAR iterations).
For instance, the running time of the abstraction process typically grows as thenumber of candidate predicates grows. Also, previous work has suggested thatinferring a small proof of a counterexample may be computationally expensive(cf. Appendix F of [20]), and while there has been much progress on efficient algorithms for inferring a small proof of a counterexample [12, 3, 17, 22], explaining
why such algorithms work well in practice seems to be no easier than explaining
the efficiency of the overall verification process.5
Secondly, in our setting of CFG programs, the counterexample form is rather
restricted. That is, we only consider counterexamples obtained by unfolding the5

In a sense, this paper poses and studies the question “assuming we have such algorithms for inferring small refinements, what can be said about the overall verification
efficiency?”. Note that a possible outcome of the study can be a negative result; forexample, showing that inferring small refinements is hard because otherwise it would
give an efficient algorithm to some provably hard verification problem.

program’s loops, and unfolding only the same number of times for every (copyof) loops (i.e., cexsyn ). By contrast, an actual CEGAR verifier is often more
liberal about the counterexample forms, and for example, may allow arbitrary
unfoldings or paths as counterexamples.6

5Conclusion

We have presented a theoretical explanation for the effectiveness of the small
refinement heuristic used in program verification with CEGAR, which, to ourknowledge, is the first of its kind. Specifically, we have formalized the small
refinement heuristic to be a refinement process that returns a proof whose size ispolynomially bounded in that of the smallest proof for the given counterexample,
and shown that CEGAR with such a refinement is guaranteed to converge in a
number of iterations bounded by the size of a proof of the given program. We
have presented the results under a rather generic setting of CEGAR, and undera more concrete setting for CFG-represented programs.
Acknowledgements. We thank the anonymous reviewers for useful comments.
This work was supported by MEXT Kakenhi 26330082 and 25280023, and JSPS
Core-to-Core Program, A.Advanced Research Networks.

References
1. International competition on software verification (SV-COMP). http://sv-comp.
sosy-lab.org/.
2. A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, andTools. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1986.
3. A. Albarghouthi and K. L. McMillan. Beautiful interpolants. In N. Sharygina and
H. Veith, editors, CAV, volume 8044 of Lecture Notes in Computer Science, pages
313–329. Springer, 2013.
4. T. Ball and S. K. Rajamani. The SLAM project: debugging system software via
static analysis. In J. Launchbury and J. C. Mitchell, editors, POPL, pages 1–3.
ACM, 2002.
5. D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Softwaremodel checking via large-block encoding. In FMCAD, pages 25–32. IEEE, 2009.
6. S. A. Cook. The complexity of theorem-proving procedures. In M. A. Harrison,
R. B. Banerji, and J. D. Ullman, editors, STOC, pages 151–158. ACM, 1971.
7. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model forstatic analysis of programs by construction or approximation of fixpoints. In R. M.
Graham, M. A. Harrison, and R. Sethi, editors, POPL, pages 238–252. ACM, 1977.
8. J. Esparza, S. Kiefer, and S. Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. JSAT, 5(1-4):27–56, 2008.
6

It is easy to reduce any CFG program to an equivalent one whose unfoldings/paths
would coincide with cexsyn (e.g., by encoding program locations in transition relation– cf. Appendix E). But, such a reduction is likely to affect the cost of the abstraction
process and the refinement process.

9. R. W. Floyd. Assigning meanings to programs. In Symposia in Applied Mathematics, volume 19, pages 19–32, 1967.
10. B. S. Gulavani, S. Chakraborty, A. V. Nori, and S. K. Rajamani. Refining abstract
interpretations. Information Processing Letters, 110(16):666–671, 2010.
11. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions fromproofs. In N. D. Jones and X. Leroy, editors, POPL, pages 232–244. ACM, 2004.
12. K. Hoder, L. Kovács, and A. Voronkov. Playing in the grey area of proofs. In
J. Field and M. Hicks, editors, POPL, pages 259–272. ACM, 2012.
13. R. Jhala and K. L. McMillan. A practical and complete approach to predicate
refinement. In H. Hermanns and J. Palsberg, editors, TACAS, volume 3920 ofLecture Notes in Computer Science, pages 459–473. Springer, 2006.
14. N. Kobayashi. Personal communication, 2012.
15. K. L. McMillan. Quantified invariant generation using an interpolating saturation
prover. In C. R. Ramakrishnan and J. Rehof, editors, TACAS, volume 4963 of
Lecture Notes in Computer Science, pages 413–427. Springer, 2008.
16. P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for Horn-clauseverification. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of Lecture
Notes in Computer Science, pages 347–363. Springer, 2013.
17. C. Scholl, F. Pigorsch, S. Disch, and E. Althaus. Simple interpolants for linear
arithmetic. In DATE, pages 1–6. IEEE, 2014.
18. R. Tarjan. Testing flow graph reducibility. In STOC, pages 96–107, 1973.
19. T. Terauchi. Dependent types from counterexamples. In M. V. Hermenegildo and
J. Palsberg, editors, POPL, pages 119–130. ACM, 2010.
20. T. Terauchi and H. Unno. Relaxed stratification: A new approach to practicalcomplete predicate refinement. In J. Vitek, editor, ESOP, volume 9032 of Lecture
Notes in Computer Science, pages 610–633. Springer, 2015.
21. H. Unno and N. Kobayashi. Dependent type inference with interpolants. In
A. Porto and F. J. López-Fraguas, editors, PPDP, pages 277–288. ACM, 2009.
22. H. Unno and T. Terauchi. Inferring simple solutions to recursion-free Horn clauses
via sampling. In C. Baier and C. Tinelli, editors, TACAS, volume 9035 of Lecture
Notes in Computer Science, pages 149–163. Springer, 2015.

A

ProofsA.1

Proof of Theorem 2

Theorem 2. CegVerif(P ) returns safe only if ∃F ⊆ T .F ⊢ P .
Proof. Immediate from the fact that Abs(P, F ) returns safe only if ∃F ⊆ T .F ⊢
P.
⊓
⊔
A.2

Proof of Theorem 3

Theorem 3. CegVerif(P ) returns unsafe only if ∀F ⊆ T .F 6⊢ P .
Proof. We show the contrapositive. Suppose F ⊢ P . Then F ⊢ π for any π
returned by Abs(F ′ , P ) for some F ′ . Hence, for any counterexample π passed to
Ref in the run of CegVerif(P ), F ⊢ π. Therefore, by the property of Ref thatit returns unsafe only if given a counterexample π such that ∀F ⊆ T .F 6⊢ π, itfollows that CegVerif(P ) does not return unsafe.
⊓
⊔

A.3

Proof of Theorem 1

The following lemma states that each run of the refinement process returns a
new proof.
Lemma 1 (Progress). Suppose Abs(P, F ) returns π and Ref(π) returns F ′ .
Then, F ′ 6⊆ F .
Proof. Because Ref(π) returns F ′ , we have F ′ ⊢ π. Also, because Abs(P, F )returns π, we have Abs(π, F ) 6= safe, and so F 6⊢ π. Therefore, F 6= F ′ , and by
the monotonicity of ⊢, it follows that F ′ 6⊆ F .
⊓⊔Theorem 1. Let the proof size metric be generic. Then, CegVerifSR converges
in at most exp(mpfsize(P )) many CEGAR iterations given a program P .
Proof. Let FP be a proof of P such that mpfsize(P ) = size(FP ). Then, for any
counterexample π of P (i.e., Abs(P, F ′ ) returns π for some F ′ ), FP ⊢ π, andtherefore mpfsize(π) ≤ size(FP ). There are at most cf (mpfsize(P )) proofs of size
at most f (size(FP )). Therefore, by Lemma 1, CegVerifSR converges in at mostexp(mpfsize(P )) many CEGAR iterations.
⊓⊔
A.4

Proof of Theorem 4

Algorithm 1 Loop Decomposition Construction
Input: Rooted graph G
Output: Loop Decomposition of G
1: decomp := {(G, ∅)};
2: Process(G);3: return decomp
4: procedure Process(G′ )5:{G1 , . . . , Gm } = Scc(G′ );6:for each cyclic Gi do
7:
hds = {v ∈ v (Gi ) | v ′ ∈/ v (Gi ) ∧ (v ′ , v) ∈ e(G)};8:decomp := decomp ∪ {(Gi , hds)};
9:
Process(Gi \ hds)
10:
end for
11: end procedure

Theorem 4. A rooted graph has a loop decomposition.
The result is well known for reducible graphs [18].7 Below, we provide a proof
for the general (i.e., possibly irreducible) case.
7

For a reducible graph, each loop has only one entry node.

Proof. Algorithm 1 builds the loop decomposition decomp by first initializing it
to contain just L0 = (G, ∅), and then calling the recursive procedure Process
on the given graph. In Process, the helper procedure Scc returns the set ofstrongly connected components of the given graph.
Because G is rooted, hds in the for each block of Process is always nonempty, and therefore, the recursive call to Process is on a smaller graph, andthe algorithm terminates. Then, by induction on the recursive call depth, itfollows that the constructed decomp is a loop decomposition of G.
⊓⊔
A.5

Proof of Theorem 5

Theorem 5. If F ⊢cfg γ then γ is safe.
Proof. Let γ = (G, T, vini , verr ). Suppose σ ⊢cfg γ where σ : v (G) → F ∪{⊥, ⊤}. Let ̟ be a path of γ such that ̟(1) = vini and ̟(|̟|) = verr .
Let σ̟ : {1, . . . , |̟|} → F ∪ {⊥, ⊤} be such that σ̟ (i) = σ(̟(i)) for eachi ∈ {1, . . . , |̟|}. Then, for any prefix ̟′ of ̟, by induction on the lengthof ̟′ , we have Post ∗T [̟′ ](States) ⊆ {s ∈ States | |=T σ̟ (|̟′ |)(s)}. Therefore,
Post ∗T [̟](States) ⊆ {s ∈ States | |=T σ̟ (|̟|)(s)} = ∅.
⊓⊔A.6

Proof of Theorem 6

Theorem 6. If F ⊢cfg γ and F ⊆ F ′ , then F ′ ⊢cfg γ.
Proof. Immediate from the definition of ⊢cfg .
A.7

⊓
⊔

Proof of Theorem 7

Theorem 7. Suppose F ⊢cfg P . Then, for any π ∈ cex(P ), F ⊢cfg π.
Proof. Let P = (G, T, vini , verr ). Let π ∈ cex(P ) where π = (Gπ , Tπ , vini , verr ).
Suppose σ ⊢cfg P where σ : v (G) → F ∪ {⊥, ⊤} Let σπ : v (Gπ ) → F ∪ {⊥, ⊤}such that σπ (v ′ ) = σ(v) where v ′ ∈ v (Gπ ) is the copy of the node v ∈ v (G)created by the unfolding. Then, from the construction of π, we have σπ ⊢cfg π.
⊓⊔
A.8

Proof of Theorem 8

Theorem 8. Abscrt satisfies the requirements for Abs. That is,(1) If F ⊢cfg γ then Abscrt (γ, F ) = safe;(2) If Abscrt (γ, F ) returns π then Abscrt (π, F ) 6= safe;(3) If F ⊢cfg P and Abscrt (P, F ′ ) returns π then F ⊢cfg π; and(4) If Abscrt (γ, F ) = safe then ∃F ′ ⊆ T .F ′ ⊢cfg γ.
Proof. We show each (1)-(4).

(1) Immediate from the fact that F ⊢cfg γ implies F ⊢crt γ.
(2) Suppose Abscrt (γ, F ) returns π. Then, F 6⊢crt π. Hence, we have Abscrt (π, F ) 6=
safe.
(3) Suppose F ⊢cfg P and Abscrt (P, F ′ ) returns π. Then, π ∈ cex(P ), and by
Theorem 7, we have F ⊢cfg π.
(4) Immediate from the fact that F ⊢crt γ implies F ∧∨ ⊢cfg γ.
⊓⊔
A.9

Proof of Theorem 9

Theorem 9. cexsyn is sound for Abscrt .
Proof. Suppose that F ⊢cfg π for all π ∈ cexsyn (P ). It suffices to show thatAbs(P, F ) = safe.
Then, for some “sufficiently large” π ∈ cexsyn (P ), we have F ⊢cfg π. Therefore, by the construction of a Cartesian predicate abstraction node-wise inductive
invariant from a proof of a sufficiently large counterexample (cf. Appendix A.10),
we have F ⊢crt P , and so Abscrt (P, F ) = safe.
⊓
⊔
A.10

Proof of Theorem 10

Theorem 10. Let the proof size metric be syntactic, ⊢cfg be the proof relation,
and Abscrt be the abstraction process with cexsyn as the counterexample generator. Then, CegVerifSR converges in poly(mpfsize(P ))maxhds(P ) many CEGAR
iterations given a CFG program P .
Proof. Let FP be a proof of P = (G, T, vini , verr ) such that mpfsize(P ) =size(FP ). Then, for any counterexample π of P (i.e., Abscrt (P, F ) returns π
for some F ), FP ⊢ π, and so mpfsize(π) ≤ size(FP ). Let lim = (f (size(FP )) +2)maxhds(P ) + 1 (“+2” accounts for {⊥, ⊤}). Let πlim be a counterexample incexsyn (P ) obtained by unfolding the loops at least lim many times. We showthat for any F such that F ⊢cfg πlim and size(F ) ≤ f (size(FP )), F ⊢crt P . (Wecall such a counterexample πlim sufficiently large.) Then, the result follows fromthe fact that there are only lim many counterexamples in cexsyn (P ) that are
obtained by unfolding the loops at most lim many times, and the fact that nocounterexample is returned more than once by the refinement process in a runof CegVerifSR .
Let πlim = (Glim , Tlim , vini , verr ). Let σlim : v (Glim ) → F ∪ {⊥, ⊤} be suchthat size(F ) ≤ f (size(FP )) and σlim ⊢cfg πlim . Let k ≥ lim be the number oftimes the loops are unfolded in πlim . We construct σ : v (G) → F ∧∨ such thatσ ⊢F
crt P by “folding” the unfolded loops in a bottom up manner. We initializeσ = σlim , and γ = πlim . We iteratively fold γ from leaf loops, while maintaining
the property that σ ⊢F
crt γ. Then, the result follows from the fact that γ becomes
P at the root of the folding process.
Let γ and σ be the current CFG and its Cartesian predicate abstraction node′′′
wise inductive invariant (i.e., σ ⊢F
crt γ). Let γ = C[t1 ∪t2 ∪. . . tk ∪tk \{hk })] whereh0 = h, t0 = t, hi+1 = ‘(hi ), ti ′ = ti hv (ti )\{hi }, sc(ti )i, and ti+1 = ti hhi , hi ifor each i ∈ {0, . . . , k − 1}. Let γ ′ = C[loop (h) t]. That is, γ ′ is obtainedby folding the unfolded loop of γ. We construct σ ′ : v (γ ′ ) → F ∧∨ such that′σ ′ ⊢Fcrt γ as follows. Because ran(σlim ) = F ∪ {⊥, ⊤}, for some 1 ≤ i1 <i2 ≤ (f (size(FP )) + 2)|h| + 1 ≤ k, σlim (hi1 ) = σlim (hi2 ) for each h ∈ {h}. By
construction, σlim (hi ) = σ(hi ) for each i ∈ {1, . . . , k} and h ∈ {h}. We set
Wi2
σ(v i ) for each v ∈ sc(t), and σ ′ (v) = σ(v) for each v ∈ v (γ) \ sc(t).
σ ′ (v) = i=1′
Then, it can be seen that σ ′ ⊢F⊓⊔
crt γ .
A.11

Proof of Theorem 11

Theorem 11. Let the proof size metric be generic, ⊢cfg be the proof relation,
and Abscrt be the abstraction process with cexsyn as the counterexample generator. Then, there exists a CFG program P with a proof F ⊢cfg P on which
CegVerifSR may take exp(size(F )) many CEGAR iterations to converge.
Proof. We show that Pex from Figure 4 is such a program. As remarked before,
we have Finv ⊢cfg Pex where Finv = {a = b ⇒ y = x + z}. For each k > 0, let
πk ∈ cexsyn (PexW) be the counterexample obtained by unfolding each loop k times,
and let Fk = { F | F ⊆ {φi | 0 ≤ i ≤ k}} where φi ≡ x = a ∧ y = b + i ∧ z = i.
S
Then, Fk ⊢cfg πk for each k > 0, and ji=1 Fi 6⊢crt πk for each k > j > 0.
Let ℓ > 0. Define size as follows: size(Finv ) = ℓ, size(Fk ) = ⌊log k⌋ fork ∈ {1, . . . , 2ℓ − 1}, and size(F ′ ) = ℓ + syntactic(F ′ ) for F ′ ∈ P(T ) \ ({Finv } ∪{Fk | 1 ≤ k ≤ 2ℓ − 1}) where syntactic(F ′ ) is the syntactic size of F ′ . Note thatsize is a generic proof size metric. Then, CegVerifSR takes 2size(Finv ) iterations
to converge when Abscrt returns the counterexamples π1 , ...π2ℓ −1 in the first2ℓ − 1 iterations and Ref returns the proofs F1 , . . . , F2ℓ −1 before returning Finv .
⊓⊔B

Correspondence of CFGs and CFG Graph Grammar

For an instruction instr = v0 7→ (φ1 : v1 , . . . , φn : vn ), we write e(instr ) for{(v0 , v1 ), . . . , (v0 , vn )}, and trans(instr ) for the map T such S
that and T ((v0 , vi )) =φi for each iS∈ {1, . . . , n}. For a term t, we write e(t) for instr ∈t e(instr ), andtrans(t) for instr ∈t trans(instr ).
We define loops(t) inductively as follows: loops({instr }) = ∅, loops(t1 ∪ t2 ) =loops(t1 ) ∪ loops(t2 ), and loops(loop (h) t) = loops(t) ∪ {(G, {h})} where G =(sc(t), e(t) ∩ sc(t)×sc(t)). Then, a CFG (G, T, vini , verr ) is said to correspond toa term t when v (G) = v (t), e(G) = e(t), T = trans(t), and loops(G) = loops(t).

C

Formal Definition of cexsyn

For a term t and k > 0, we define tk be t with each loop annotation added theunfolding counter k. More formally, we inductively define counter annotation as
follows: instr k = instr, (t1 ∪ t2 )k = t1 k ∪ t2 k , and (loop (h) t)k = loop k (h) (tk ).

We let the rewriting relation respect the counter annotation, so that eachloop is unfolded the number of times it is annotated:C[loop k (h) t] 99Kct C[thv (t)\{h}, sc(t)i ∪ loop k−1 (‘h) th{h}, {h}i]C[loop 0 (h) t] 99Kct C[t\{h}]Note that in the first rule, the counter annotations in t are carried over tothv (t)\{h}, sc(t)i, and so the nested copies of loops created in the unfolding will
also be unfolded the number of times as specified by the annotations in t.
Then, cexsyn (P ) is defined to be the set of CFGs obtained by applying
the above reduction to convergence from a term P k for some k > 0. That is,cexsyn (P ) = {π | P k 99K∗ct π ∧ k > 0 ∧ π contains no loop}.
Example. Consider the program P below (left).

L1: while (b1) {if (b2) {L2:while (b3) { s1; }} else {L3:
while (b4) { s2; }}}if (b1) {if (b2) {if (b3) { s1; }if (b3) { s1; }} else {if (b4) { s2; }if (b4) { s2; }}}if (b1) {if (b2) {if (b3) { s1; }if (b3) { s1; }} else {if (b4) { s2; }if (b4) { s2; }
}
}

P

π

P has three non-root loops: L1 , L2 , and L3 . The loops L2 and L3 arenested inside L1 . Assuming that the CFG-representation of P preserves the loop
structure, the counterexample π obtained by unfolding the loops twice (i.e.,
P 2 99K∗ct π) is shown above (right). Note that the outer loop L1 is unfolded
twice, and the inner loops L2 and L3 are each unfolded twice per each unfoldingof L1 (and so each four times total).

D

Deciding Provability of Acyclic CFGs

We show an algorithm for deciding the provability of acyclic CFGs that is basedon a reduction to recursion-free Horn-clause constraint solving [21, 19].
First, we define effective interpolation. Given T -formulas φ and ψ, we say thata T -formula θ is an interpolant of φ and ψ if fv(θ) ⊆ fv(φ)∩fv(ψ), |=T φ ⇒ θ, and|=T θ ⇒ ψ. We say that T is effectively interpolating if there exists an algorithm
A such that, given T -formulas φ and ψ, A(φ, ψ) returns an interpolant of φand ψ if one exists, and otherwise returns No. By abuse of terminology, for“quantifier-free theories”, we restrict φ, ψ, θ to be quantifier-free formulas of T
in the definition above. QFLRA is known to be effectively interpolating.8
Recursion-free Horn-clause Constraints. A predicate variable application
is of the form Q(x) where Q is a predicate variable of arity |x|. A Horn clausehc is of the form φ ∧ β1 ∧ · · · ∧ βn ⇒ α where φ is a T -formula, each βi isa predicate variable application, and α is a predicate variable application or⊥. A Horn-clause constraint set (HCCS) H is a finite set of Horn clauses. We
write pv(H) for the predicate variables in H. We say that H is recursion-free if{(Q, Q′ ) | ψ ∧ . . . Q(x) . . . ⇒ Q′ (y) ∈ H} is acyclic.
We say that ρ : pv(H) → T is a solution of H, written ρ ⊢ H, if |=T ρ(hc)for each hc ∈ H, where ρ(hc) is hc with each predicate variable application Q(x)replaced by ρ(Q)(x). Previous works [21, 19] have shown algorithms for solving
recursion-free HCCSs for effectively interpolating T .9
Reduction. We reduce provability of an acyclic CFG to solving a recursionfree HCCS. Let γ = (G, T, vini , verr ). For each v ∈ v (G), let Qv be a distinct
predicate variable of arity |x|. Let Hγ be the set of Horn clauses {Qv (x) ∧T ((v, v ′ ))(x, x′ ) ⇒ Qv′ (x′ ) | (v, v ′ ) ∈ e(G)} ∪ {⊤ ⇒ Qvini (x), Qverr (x) ⇒ ⊥}.
Because G is acyclic, Hγ is recursion-free. Also, by construction, we have ∃ρ :pv(Hγ ) → F ∪ {⊥, ⊤}.ρ ⊢ Hγ if and only if F ⊢cfg γ.

E

Reducing CFG to one-loop CFG

Let P = (G, T, vini , verr ). We give a polynomial time transformation of P intoa CFG P † such that (1) P † is safe if and only if P is safe, and (2) cexsyn (P † ) =cex(P † ).
For each v ∈ v (G), let φv be a T -predicate of some fixed arity (i.e., |pc|)
satisfying |=T φv (pc) ⇒ ¬φv′ (pc) for each v, v ′ ∈ v (G) such that v 6= v ′ . The
transformation works for any theories that have such predicates. For example,
for QFLRA, it suffices to let φv = λpc.pc = num(v) where num(·) assigns a
distinct rational constant to each v ∈ V .
Let y = pc, x and y ′ = pc ′ , x′ where y, y ′ are distinct variables such that′|y | = |y|. We define G† and T † as follows.
v (G† ) = {vini † , verr † , vloop † }e(G† ) = {(vini † , vloop † ), (vloop † , vloop † ), (vloop † , verr † )}T † ((vini † , vloop † )) = λy, y ′ .φvWini (pc ′ )T † ((vloop † , vloop † )) = λy, y ′ . e∈e(G) φsc(e) (pc) ∧ T (e)(x, x′ ) ∧ φtg(e) (pc ′ )T † ((vloop † , verr † )) = λy, y ′ .φverr (pc)8This differs from the notion of interpolants from mathematical logic which requires
the non-logical symbols of θ to appear in φ and ψ. But, this definition is often usedin the verification literature and is sufficient for the purpose.
9
We remark that the converse also holds, that is, any algorithm for solving recursionfree HCCS gives an interpolation algorithm for the corresponding theory. This isbecause θ is an interpolant of φ and ψ if and only if {Q 7→ λx.θ} is a solution of{φ ⇒ Q(x), Q(x) ∧ ¬ψ ⇒ ⊥} where {x} = fv(φ) ∩ fv(ψ).

It is easy to see that P † = (G† , T † , vini † , verr † ) satisfies the conditions (1) and(2) given above. We note that (2) follows because P † has only one non-root
loop. Also, it can be seen that the the syntactic size of the smallest proof of P †is polynomial in the size of G, the syntactic sizes of φv ’s, and the syntactic size ofthe smallest proof of P . This follows because σ ⊢cfgWP implies σ † ⊢cfg P † whereσ † (vini † ) = ⊤, σ † (verr † ) = ⊥, and σ † (vloop † ) = λy. v∈v (G) φv (pc) ∧ σ(v)(x).