Relaxed Stratification: A New Approach toPractical Complete Predicate Refinement⋆
Tachio Terauchi1 and Hiroshi Unno2
1

JAIST
terauchi@jaist.ac.jp
2
University of Tsukuba
uhiro@cs.tsukuba.ac.jp

Abstract. In counterexample-guided abstraction refinement, a predicate refinement scheme is said to be complete for a given theory if it
is guaranteed to eventually find predicates sufficient to prove the given
property, when such exist. However, existing complete methods requiredeciding if a proof of the counterexample’s spuriousness exists in some finite language of predicates. Such an exact finite-language-restricted predicate search is quite hard for many theories used in practice and incurs
a heavy overhead. In this paper, we address the issue by showing thatthe language restriction can be relaxed so that the refinement process
is restricted to infer proofs from some finite language Lbase ∪ Lext but
is only required to return a proof when the counterexample’s spuriousness can be proved in Lbase . Then, we show how a proof-based refinement algorithm can be made to satisfy the relaxed requirement and becomplete by restricting only the theory-level reasoning in SMT to emit
Lbase -restricted partial interpolants (while such an approach has been
proposed previously, we show for the first time that it can be done for
languages that are not closed under conjunctions and disjunctions). We
also present a technique that uses a property of counterexample patterns
to further improve the efficiency of the refinement algorithm while stillsatisfying the requirement. We have experimented with a prototype implementation of the new refinement algorithm, and show that it is able
to achieve complete refinement with only a small overhead.

1

Introduction

Predicate abstraction with counterexample-guided abstraction refinement (CEGAR) is a promising approach to automated verification of safety (i.e., reachability) properties (see, e.g., [6] for a survey). Briefly, the CEGAR approach works
as follows. Let T be a first-order logic (FOL) theory. The verifier picks somefinite set of predicates from T as the initial candidate predicate set, and iterates
the following two processes until convergence (here, we use the term “predicate”
for an arbitrary formula, and not limited to just atomic predicates).
⋆

This work was supported by MEXT Kakenhi 23220001, 26330082, 25280023, and25730035.

(1) The abstraction process checks if the current candidates form a sufficient
proof of the program’s safety (i.e., an inductive invariant – sometimes called“safe” inductive invariant). If so, then the program is proved safe and theiteration halts. Otherwise, the process generates a counterexample as anevidence that the current candidates are insufficient, and (2) is invoked.
(2) The refinement process analyzes the given counterexample. If the counterexample cannot be proved spurious by predicates from T (i.e., “the counterexample is real”), then the iteration halts and the program is detected to beunsafe. Otherwise, the predicates inferred as a proof of the counterexample’s
spuriousness are added to the candidates, and we repeat from (1).
Note that the verifier halts either when sufficient predicates are inferred to prove
the program safe, or a real counterexample is discovered.
For an unsafe program, the state-of-the-art CEGAR-based verifiers are usually able to eventually discover a real counterexample and converge, by exploring
the state space in a fair manner (if somewhat slowly for ones requiring large counterexamples). By contrast, when a program is safe and the underlying theory
T is sufficient for proving the safety, most verifiers have no guarantee of convergence and can diverge by having the refinement process indefinitely produce
incorrect candidate proofs.
For example, consider the C-like program shown in Figure 1. Here, ndet()
returns a non-deterministic integer. The goal is to verify that the assertion failure
is unreachable, that is, a = b ⇒ y = x whenever line 10 is reached.
Suppose we start the verification process with the 1: void main(void) {candidate set comprising the 2:
int a = ndet();int b = ndet();boolean closure of the pred- 3:
int x = a;int y = b;int z = 0;
while (ndet()) {icates z = 0, a = b and 4:
y++;z++;
y = x. A possible counterex- 5:}
ample is a path that passes 6:
while (z != 0) {through the first loop (lines 7:
8:y--;z--;
4-6) once, reaching line 79:}with the abstract state (a = 10: if (a=b && y!=x) { assert false; }b ⇒ y ≠ x) ∧ z ≠ 0, and then 11: }passes through the second
loop (lines 7-9) once, reaching line 10 with the abstract Fig. 1. A program on which CEGAR may diverge.
state z = 0, which does not
imply a = b ⇒ y = x. A possible proof of the counterexample’s spuriousness (i.e.,
proof that the path is actually safe) is the predicate a = b ⇒ y = x + z. The predicate turns out to be an inductive invariant for the program, and the verification
process halts in the next iteration.
Unfortunately, the refinement process is not guaranteed to infer such a predicate but may choose any predicates that can prove the counterexample’s safety.
For instance, another possibility is the predicate a = b ⇒ y = x + 1. Adding thisto the candidate set is sufficient for proving the safety of the counterexample

but not that of the program, and the abstraction process in the subsequent iteration would return yet another counterexample. For example, it may return the
counterexample that passes the first loop twice, reaching line 7 with the abstractstate a = b ⇒ y ≠ x + 1, and then passes through the second loop twice, reachingline 10 with the abstract state z = 0 again. Then, the refinement process may
choose the predicate a = b ⇒ y = x + 2 to prove the spuriousness of this new
counterexample, which is still insufficient to prove the whole program correct.
The abstract-and-refine iteration may repeat indefinitely in this manner, adding
to the candidates the predicate a = b ⇒ y = x + i in each i-th run of the refinement process. A refinement process is said to be complete (w.r.t. T ) if the
CEGAR process is guaranteed to converge and eventually discover a proof ofthe program’s safety, when one exists in T .
Previous works [7, 11] have proposed to achieve complete refinement in CEGAR by stratifying T into an infinite sequence of predicate languages L0 ⊆ L1 ⊆. . . Lk . . . such that T = ⋃k∈ω Lk , and requiring each i-th run of the refinement
to only infer predicates from the stratum Llvl(i) where lvl (i) is the stratum levelat the i-th CEGAR iteration. By requiring each Lk to be finite3 and raising
the stratum level just when the refinement process reports that no proof exists
for the given counterexample in the current stratum, the approach guarantees
completeness. However, the approach requires the refinement process to exactly
decide if there is a proof of the given counterexample in the current stratum. Indeed, completeness would be lost if the refinement process was allowed to reportthat the current stratum does not have a proof when it actually does. For many
theories used in practice, such as the theory of linear real arithmetic, such anexact finite-language-restricted proof search incurs heavy overhead and is prohibitive (see Section 4, Section 5, and the extended report [18] for analysis anddiscussion).
The first contribution of this paper is the observation that exact finite language restricted proof search is actually unnecessary for completeness. Instead,
we show that the following more relaxed scheme is sufficient: in each i-th run of
the refinement process, we restrict the returned proof to some finite language oflvl(i)
lvl(i)
predicates Lbase ∪ Lext (base and extension) such that the refinement processlvl(i)
may report that no proof exists only when no proof exists in Lbase . There areno further restrictions on the refinement process, and so, the refinement process
may return a proof that is not in Lbase (but in Lbase ∪ Lext ) even if a proof exists
in Lbase , or may report that no proof exists even if a proof exists in Lbase ∪ Lext
(but not in Lbase ). We show that this relaxed approach still ensures completenesswhen the stratum level is raised just when the refinement process reports that
there is no proof in the current stratum, as before, and Lbase grows to eventually
cover T (i.e., L0base ⊆ L1base ⊆ . . . Lkbase . . . such that T = ⋃k∈ω Lkbase ). We formalize this observation in a refinement algorithm scheme called relaxed stratification(contra the exact stratification approach described above) and prove that it isindeed complete.
3

The term “finite predicate language” is used synonymously with “finite set of predicates”.

As the second contribution, we present a concrete refinement algorithm that
implements the relaxed scheme. The algorithm is a modification of the proofbased refinement [5] in which the theory-level reasoning is restricted so thatpartial (tree-)interpolants at that level is restricted to Lbase .4 We also present atechnique that uses a certain property of the counterexample patterns to further
improve the efficiency of the algorithm while still satisfying the requirement of
the scheme. We formalize the refinement algorithm as a constraint solver forrecursion-free Horn-clause constraints [3, 12, 13, 21] which has gained popularity
as the standard format for describing refinement algorithms. We have implemented a prototype of the refinement algorithm, and we show empirically that
it is able to achieve complete predicate refinement with low overhead.
In summary, the paper’s contributions are as follows:– A new scheme for practical complete predicate refinement called relaxedstratification and the proof of its completeness (Section 2).
– A new predicate refinement algorithm as concrete instance of the relaxedstratification scheme (Section 3).
– Experiments with a prototype implementation of the refinement algorithm(Section 4).
The rest of the paper is organized as follows. Section 2 formally defines therelaxed stratification scheme and proves its completeness. Section 3 presents
the concrete refinement algorithm implementing the scheme. Section 4 presents
experimental results with the prototype implementation of the refinement algorithm. We discuss related work in Section 5 and conclude the paper in Section 6.
Supplementary material contains the extended report with proofs and extra materials omitted from the main body of the paper, and the benchmarks used in
the experiments [18].

2

The Relaxed Stratification Scheme

Let T be a FOL theory. For a formula θ in the signature of T (a T -formula), wewrite fvs(θ) for the free variables in θ. A predicate in T is of the form λx1 , . . . , xn .θ
where θ is a T -formula such that fvs(θ) ⊆ {x1 , . . . , xn }. For readability, we often
omit the explicit λ abstraction and treat a formula θ as the predicate λx̄.θ where{x̄} = fvs(θ). We overload T for the set of predicates in T .
2.1

Assumptions on the Abstraction Process

Relaxed stratification only concerns the refinement process part of CEGAR.
We show that the scheme is quite general and can be used in a wide rangeof CEGAR-based verifiers. To this end, we delineate the conditions that the4

While this approach has already been suggested in [7], they require the restricting
language to be closed under conjunctions and disjunctions (see Section 5 for further
discussion).

abstraction process part needs to satisfy. As we shall show below, the conditions
are quite weak and satisfied by virtually any CEGAR-based verifier.
We assume that the abstraction process Abs takes as input a program and afinite set of predicates in T (the set of candidate proofs). For a program M anda finite set of predicates F ⊆ T , we require that Abs(M, F ) either returns safe,
indicating that M has been proved safe using the predicates from F , or returns acounterexample. For generality, we assume that a counterexample is also simply
a program so that, for a counterexample M , we write Abs(M, F ) = safe when F issufficient for the abstraction process to prove the spuriousness of M (in practice,a counterexample is not an arbitrary program, but, e.g., an unwound programslice of the input program, and concrete instances of the relaxed stratification
scheme take advantage of the counterexample structure – cf. Section 3). We
sometimes say that F refutes the counterexample M when Abs(M, F ) = safe.
We require Abs to be monotonic on the candidates, that is, if Abs(M, F ) = safe
and F ⊆ F ′ then Abs(M, F ′ ) = safe (i.e., having more predicates can only increase Abs’s ability to prove). We also require that if Abs(M, F ) = cex(M ′ ) thenAbs(M ′ , F ) ≠ safe, that is, the returned counterexample is actually a counterexample and cannot be refuted by the given predicates. Finally, we require that if
Abs(M, F ) = safe and Abs(M, F ′ ) = cex(M ′ ) then Abs(M ′ , F ) = safe, that is, if
a set of predicates is a proof for program’s safety then it is also a proof for any
counterexample of the program. We say that Abs is sound when it only provessafe programs safe, that is, Abs(M, F ) = safe only if M is safe.5
We note that the assumptions on the abstraction process are quite liberaland do not demand, for example, the process uses the given set of predicatesby decomposing them into atomic predicates and taking their boolean closure,taking the cartesian closure, or using them directly as loop invariants. In Example 1 below, we describe an example abstraction process that uses the predicatesdirectly.
Example 1. Let T be the quantifier-free theory of linear real arithmetic. Let Abs
be the abstraction process that, given a program (or counterexample) M and theset of predicates F ⊆ T , checks if there exists an assignment from each loop-headlocation in M to a predicate in F that forms an inductive invariant of M . Recall
the example from Section 1. Let Mex be the program shown in Figure 1. Then,the map ρ such that ρ(L4) = ρ(L7) = θex1 where θex1 ≡ a = b ⇒ y = x + z is aninductive invariant of Mex , and therefore, Abs(Mex , {θex1 }) = safe.
When given an insufficient set of predicates as the candidates, Abs returns
a counterexample. For instance, as discussed in Section 1, a possible counterexample of Mex is Mexa , shown in Figure 2, that passes through each loop once
to reach line 10. (The semantics of assume (b) is to safely halt if b is false, andproceed otherwise.) Here, a1–a4 label the entry points of the unwound loops.
Viewing them as one-iteration loops where invariants are asserted, it can beseen that ρ such that ρ(ℓ) = θex1 for each ℓ ∈ {a1–a4} is an inductive invariant of Mexa , and therefore Abs(Mexa , {θex1 }) = safe. However, as discussed in5Soundness of Abs is not required for completeness of relaxed stratification.

int a=ndet();int b=ndet();int x=a;int y=b;int z=0;
a1:assume (ndet());
y++;z++;
a2:assume (ndet());
a3:assume (z != 0);y--;z--;
a4:assume (z == 0);
assume (a=b && y!=x);
assert false;

int a=ndet();int b=ndet();int x=a;int y=b;int z=0;b1:assume (ndet());
y++;z++;
b2:assume (ndet());
y++;z++;
b3:assume (ndet());
b4:assume (z != 0);y--;z--;
b5:assume (z != 0);y--;z--;
b6:assume (z == 0);
assume (a=b && y!=x);
assert false;

Mexa

Mexb

Fig. 2. Counterexamples of the program from Figure 1.

Section 1, asserting θ0 at a1, a4, and θ1 at a2, a3 where θ0 ≡ a = b ⇒ y = x
and θ1 ≡ a = b ⇒ y = x + 1 also constitutes a sufficient loop invariant of Mexa .
Therefore, we also have Abs(Mexa , {θ0 , θ1 }) = safe.
Similarly, Mexb shown in Figure 2 is a counterexample that passes througheach loop twice to reach line 10. By reasoning similar to the above, we haveAbs(Mexb , {θex1 }) = Abs(Mexb , {θ0 , θ1 , θ2 }) = safe where θ2 ≡ a = b ⇒ y = x + 2. ▲2.2

The Relaxed Stratification Scheme

We are now ready to formalize the relaxed stratification scheme. The core of thescheme is the relaxed finite-language-restricted refinement process RlxRef thattakes as input a counterexample and a restricting predicate language (Lbase , Lext ),and returns either unsafe indicating that the counterexample is real, a set of predicates F ⊆ Lbase ∪ Lext that proves the safety of the counterexample, or noproof
indicating that it could not find a proof for the counterexample within the given
restriction.
We prepare strata of restricting predicate languages:(L0base , L0ext ), (L1base , L1ext ), . . . (Lkbase , Lkext ), . . .
We require each restricting predicate language to be finite, and the base-part toeventually cover T . Formally, we impose the following condition on the restricting
predicate languages: 1.) for each k ∈ ω, Lkbase ∪ Lkext is a finite subset of T , 2.) forkeach k ∈ ω, Lkbase ⊆ Lk+1
base , and 3.) T = ⋃k∈ω Lbase .
Figure 3 shows the overview of the relaxed stratification verification process.
The verification procedure RlxCegar takes as input the program M to be verified,
and first initializes the candidate predicate set Cands to ∅ (line 2) and therestricting language stratum k to 0 (line 3). Then, it repeats the abstract-andrefine loop (lines 4-10) until convergence. The loop first calls Abs(M, Cands) to01: RlxCegar(M ) =02: Cands := ∅;03: k := 0;
04: while true do05:
match Abs(M ,Cands) with06:
safe → return safe
07:
∣ cex(M ′ ) → match RlxRef(M ′ ,Lkbase ,Lkext ) with08:
unsafe → return unsafe
09:∣ prf(F ) → Cands := Cands ∪ F
10:∣ noproof → k := k + 1
Fig. 3. The relaxed stratification verification process.

check if M can be proved safe with the current candidates. If so, then we exit
the verification process, returning safe (line 6). Otherwise, a counterexample
M ′ is obtained, and we call RlxRef on M ′ and the current restricting language(Lkbase , Lkext ) (line 7). If RlxRef returns unsafe, then the counterexample is real
and we exit the verification process, returning unsafe (line 8). Otherwise, RlxRefeither returns a set of predicates that refutes the counterexample (line 9), or
returns noproof indicating that it has failed to find a proof for the counterexample
in the current language stratum (line 10). In the former case, the returned setof predicates are added to Cands, and in the latter case, the language stratum
is raised to the next level.
We require RlxRef to only report unsafe on a real counterexample, that is,
RlxRef(M, Lbase , Lext ) = unsafe only if ∀F ⊆ T .Abs(M, F ) ≠ safe, and we require the returned proof to be actually a proof of the counterexample, that is
RlxRef(M, Lbase , Lext ) = prf(F ) only if Abs(M, F ) = safe (these conditions are
not particular to relaxed stratification and usually assumed for any refinement
process in CEGAR). In addition, we require RlxRef to only infer proofs from thegiven restricting predicate language and be able to return some proof if the given
counterexample is refutable just in the base part of the language. Formally, we
impose the following additional conditions on RlxRef:– If RlxRef(M, Lbase , Lext ) = prf(F ) then F ⊆ Lbase ∪ Lext ; and– If ∃F ⊆ Lbase .Abs(M, F ) = safe, then RlxRef(M, Lbase , Lext ) = prf(F ′ ) forsome F ′ .
We state and prove the completeness of the relaxed stratification scheme.
Theorem 1 (Completeness). If ∃F ⊆ T .Abs(M, F ) = safe, then RlxCegar(M )terminates and returns safe.
We remind that safety verification is undecidable in general, and our “completeness” only states that the verification terminates under the promise that a proofof the program’s safety exists in T .6
6

This notion of completeness is the same as the one from previous works [7, 11].

Also, assuming that Abs is sound (cf. Section 2.1), it is easy to see that
RlxCegar is also sound in that it only proves safe programs safe (in fact, thisholds independently of the behavior of RlxRef).
Theorem 2 (Soundness). If Abs is sound, then RlxCegar(M ) returns safe only
if M is safe.
Example 2. We show how the relaxed stratification scheme would ensure theconvergence of a verifier on the program Mex from Example 1. Suppose that werun RlxCegar(Mex ), and for contradiction, it diverges by generating the following
infinite series of refinements discussed in Section 1:
a = b ⇒ y = x, a = b ⇒ y = x + 1, . . . a = b ⇒ y = x + i, . . .
By the definition of RlxCegar, it must be the case that the restricting predicate
lvl(i)
lvl(i)
language at the i-th CEGAR iteration is (Lbase , Lext ) such that y = x + i ∈lvl(i)
lvl(i)
Lbase ∪ Lext where lvl (i) is the restricting language stratum level in the i-thlvl(i)
lvl(i)
iteration. Because each Lbase ∪ Lext is finite, the stratum level of the language
must have been raised infinitely many times. Therefore, a = b ⇒ y = x + z ∈ Ljbase
for some j because T = ⋃k∈ω Lkbase .
But, as argued in Example 1, a = b ⇒ y = x + z is a sufficient proof of Mex ’ssafety, and therefore also that of its counterexamples. Therefore, by the fact that
RlxRef refutes any counterexample refutable in the base part of the given restricting language, for any counterexample M ′ of Mex , RlxRef(M ′ , Ljbase , Ljext ) =prf(F ′ ) for some F ′ ⊆ Ljbase ∪ Ljext . Then, because Ljbase ∪ Ljext is finite, RlxCegar
must have eventually inferred a sufficient set of predicates that constitutes a
proof of Mex ’s safety without further raising the language stratum.
▲

3

Concrete Refinement Algorithm Instances

We show how to implement the relaxed finite-language-restricted refinement
process RlxRef. In fact, we describe a technique that takes as module an exact
Lbase -restricted refinement algorithm and turn it into a relaxed (Lbase , Lbase ∧∨ )restricted refinement algorithm. (We write L∧∨ for the closure of L under conjunctions and disjunctions.) We focus on the case where the given counterexample is spurious.7
Following the recent trend [17, 3, 8, 2, 1, 13, 12, 21], we formalize the refinement algorithm as a constraint solver for recursion-free Horn-clause constraints.
Specifically, we present a relaxed (Lbase , Lext )-restricted constraint solver thattakes as module an exact Lbase -restricted constraint solver (cf. Section 3.1 forthe definition of exact/relaxed finite-language-restricted constraint solvers). We
review Horn-clause constraints in Section 3.1, and describe the constraint solver,that we call RlxSolveA, in Section 3.2.
7Detecting if the counterexample real and returning unsafe if so can be handled via
usual unrestricted refinement (cf. Section 4).

We also present a technique that takes as module a relaxed (Lbase , Lext )restricted constraint solver, an unrestricted constraint solver AU , and a positive
integer parameter ℓ, and turn them into a relaxed (Lbase , LB(Lbase ∪Lext , AU , ℓ))restricted constraint solver where LB(L, AU, ℓ) is a certain finite language ofpredicates determined by L, AU , and ℓ. We formalize the technique as the constraint solver RlxSolveB, described in Section 3.3. The technique applies the relaxed finite-language-restricted constraint solver provided as the module to onlya small subset of the constraint solving problem, and can be used to improvethe efficiency of the given relaxed finite-language-restricted constraint solver.
We remind that the exact finite-language-restricted proof search is an inherently expensive process (cf. Section 5, Section 4, and the extended report [18]),
and the key idea in these constraint solvers is to use the expensive exact finitelanguage-restricted proof search process (given as a module) only on small subparts of the problem. This is made possible thanks to the relaxed requirement on
the language restriction where the refinement process is not required to exactly
decide the existence of a restricted solution for the whole problem. Informally,
the trick is to choose the subproblems just large enough to guarantee that if asubproblem is not Lbase solvable then neither is the whole and that there canonly be finitely many solutions for the whole obtainable from Lbase -restricted
solutions for the subproblems.
3.1

Horn Clause Constraints

For concreteness, in what follows, we assume that the underlying theory T is
the quantifier-free theory of linear real arithmetic (QFLRA). However, the techniques presented in Sections 3.2 and 3.3 can be applied to any quantifier-freetheory.
A formula θ in the signature of QFLRA comprises atomic predicate p of theform a1 x1 + a2 x2 ⋅ ⋅ ⋅ + an xn ≤ an+1 where a1 , . . . , an+1 ∈ Z, and is closed under theusual boolean operations ¬, ∧, ∨, and ⇒. As usual, we let ¬ bind the tightest and⇒ the weakest. A literal l is either an atomic predicate or its negation. A clause
C is a disjunction of literals. A conjunctive normal form (CNF) is a conjunctionof clauses. We often use a set to represent a clause or a CNF so that {l1 , . . . , ln }represents l1 ∨ ⋅ ⋅ ⋅ ∨ ln and {C1 , . . . , Cn } represents C1 ∧ ⋅ ⋅ ⋅ ∧ Cn . We write  forcontradiction and ⊺ for tautology. We write ⊧ θ when θ is valid in T .
Horn Clauses and Horn-Clause Constraints. A predicate variable application is of the form P (x̄) where P is a predicate variable of arity ∣x̄∣. A Hornclause hc is of the form θ ∧ B1 ∧ ⋅ ⋅ ⋅ ∧ Bn ⇢ H where θ is a formula in T , each Bi
is a predicate variable application, and H is a predicate variable application or. We call H the head of the Horn clause, and θ ∧ B1 ∧ ⋅ ⋅ ⋅ ∧ Bn the body. A Hornclause whose head is  is called a root clause.
A Horn-clause constraint set (HCCS) H is a finite set of Horn clauses. We
write pvs(H) for the predicate variables in H. We write leaves(H) for the setof predicate variables in H that do not occur as a head in H. We define ↝H to
be the relation {(P, Q) ∣ θ ∧ . . . P (x̄) . . . ⇢ Q(ȳ) ∈ H}. We say that a Horn clauseθp1 ⇢ P (x̄)θp2 ∧ P (x̄) ⇢ P (x̄′ )P (x̄) ⇢ Q(x̄)θp3 ∧ Q(x̄) ⇢ Q(x̄′ )θp4 ∧ Q(x̄) ⇢ 

θp1 ⇢ P1 (x̄)θp2 ∧ P1 (x̄) ⇢ P2 (x̄′ )P2 (x̄) ⇢ Q1 (x̄)θp3 ∧ Q1 (x̄) ⇢ Q2 (x̄′ )θp4 ∧ Q2 (x̄) ⇢ 

θp1 ⇢ P1 (x̄)θp2 ∧ P1 (x̄) ⇢ P2 (x̄′ )θp2 ∧ P2 (x̄) ⇢ P3 (x̄′ )P3 (x̄) ⇢ Q1 (x̄)θp3 ∧ Q1 (x̄) ⇢ Q2 (x̄′ )θp3 ∧ Q2 (x̄) ⇢ Q3 (x̄′ )θp4 ∧ Q3 (x̄) ⇢ 

Hex

Hexa

Hexb

Fig. 4. HCCS examples.

θ ∧ B1 ∧ ⋅ ⋅ ⋅ ∧ Bn ⇢ H is conjunctive if θ is a conjunction of literals. We say thatan HCCS H is conjunctive if each hc ∈ H is conjunctive.
We say that H is recursion-free if ↝H is acyclic. We say that a recursion-free
HCCS H is tree-like [12, 13] if 1.) there is exactly one root clause in H and every
P ∈ pvs(H) can reach a predicate variable occurring in the body of the root clausevia ↝∗H ; and 2.) for any P ∈ pvs(H), at most one hc ∈ H contains P in its body, atmost one hc ∈ H contains P as its head, and no hc ∈ H has multiple occurrences of
P . For a tree-like HCCS H, we define the depth of H, depth(H), to be the lengthof the longest ↝H path. For η a mapping from predicate variables to predicate
variables, we write η(hc) for the Horn clause hc with each predicate variableapplication P (x̄) replaced by η(P )(x̄). We write η(H) for {η(hc) ∣ hc ∈ H}. We
say that a tree-like HCCS H′ is an unwound instance of a (possibly recursive)
HCCS H if there exists a mapping η from pvs(H′ ) to pvs(H) such that η(H′ ) ⊆ H.
Constraint Solutions and Restricted Constraint Solvers. For σ a mapping from predicate variables to predicates in T , we write σ(hc) for hc with eachpredicate variable application P (x̄) replaced by θ[x̄/ȳ] where σ(P ) = λȳ.θ. We
say that the map σ from pvs(H) to predicates in T is a solution of H, writtenσ ⊧ H, if for each hc ∈ H, ⊧ σ(hc), interpreting ⇢ as ⇒. We define ran(σ), therange of σ, to be the set of predicates {σ(P ) ∣ P ∈ dom(σ)}.
We focus on constraint solving algorithms for tree-like HCCSs (they can beextended to arbitrary recursion-free HCCSs by adopting the technique from [13]).
We say that an algorithm is an unrestricted constraint solver if given a tree-like
HCCS H, it returns a solution of H or decides that H has no solution. We saythat an algorithm is an exact L-restricted constraint solver if given a tree-like
HCCS H, it decides if there is a solution σ of H such that ran(σ) ⊆ L and returns
such a solution if so. We say that an algorithm is a relaxed (Lbase , Lext )-restrictedconstraint solver if given a tree-like HCCS H, it either returns a solution σ of H
such that ran(σ) ⊆ Lbase ∪ Lext or returns noproof indicating that it has failed tofind a solution, with the requirement that it returns some solution (whose range
is in Lbase ∪ Lext ) if there exists a solution σ ′ of H such that ran(σ ′ ) ⊆ Lbase .

Example 3. Consider the HCCS Hex shown in Figure 4. Here, x̄ = a, b, x, y, z,x̄′ = a′ , b′ , x′ , y ′ , z ′ , andθp1 ≡ x = a ∧ y = b ∧ z = 0
θp2 ≡ z ′ = z + 1 ∧ y ′ = y + 1 ∧ x′ = x ∧ a′ = a ∧ b′ = bθp3 ≡ z ≠ 0 ∧ z ′ = z − 1 ∧ y ′ = y − 1 ∧ x′ = x ∧ a′ = a ∧ b′ = bθp4 ≡ z = 0 ∧ a = b ∧ x ≠ y
Hex is not tree-like (in fact, ↝S is cyclic). Figure 4 shows HCCSs Hexa andHexb that are tree-like. In addition, they are unwound instances of Hex becauseηa (Hexa ) ⊆ Hex and ηb (Hexb ) ⊆ Hex where ηa = {P1 ↦ P, P2 ↦ P, Q1 ↦ Q, Q2 ↦ Q}
and ηb = {P1 ↦ P, P2 ↦ P, P3 ↦ P, Q1 ↦ Q, Q2 ↦ Q, Q3 ↦ Q}.
Recall the predicates θext1 , θ0 , θ1 , θ2 from Example 1. Let the maps σa1 , σa2 ,
σb1 , and σb2 be defined as below.
σa1 = {P ↦ θex1 ∣ P ∈ pvs(Hexa )}σb1 = {P ↦ θex1 ∣ P ∈ pvs(Hexb )}σa2 = {P ↦ θ0 ∣ P ∈ {P1 , Q2 }}∪ {P ↦ θ1 ∣ P ∈ {P2 , Q1 }}σb2 = {P ↦ θ0 ∣ P ∈ {P1 , Q3 }}∪ {P ↦ θ1 ∣ P ∈ {P2 , Q2 }}∪ {P ↦ θ2 ∣ P ∈ {P3 , Q1 }}Then, σa1 and σa2 are solutions of Hexa , and σb1 and σb2 are solutions of Hexb .
▲Relating Refinement Process to Constraint Solving. We relate constraint
solving to refinement process. Roughly, the relationship says that, for any counterexample, there is a corresponding tree-like HCCS such that the range of its
solutions are the proofs of the counterexample’s spuriousness. We further assume that such a tree-like HCCS is always an unwound instance of some fixed“generator” HCCS determined by the given program.
We formalize the relationship. Let M be a program. We assume that there
exists an HCCS Hgen(M ) such that for any counterexample M ′ of M (i.e.,Abs(M, F ) = cex(M ′ ) for some F ), there exists an unwound instance HM ′ ofHgen(M ) that satisfies the following:– if σ ⊧ HM ′ then Abs(M ′ , ran(σ)) = safe (i.e., the range of a solution of HM ′is a proof of M ′ ’s spuriousness); and– if Abs(M ′ , F ) = safe then ∃σ. ran(σ) ⊆ F ∧σ ⊧ HM ′ (i.e., if M ′ can be refutedby F , then there is a solution for HM ′ whose range is in F ).
Hence, the task of implementing a relaxed language restricted refinement process
RlxRef for the restricting language (Lbase , Lext ) is now reduced to implementing
a relaxed (Lbase , Lext )-restricted constraint solver.
We remark that the relationship stated above is quite general and many
CEGAR-based verifiers [17, 8, 2, 1, 13, 12, 21] use the relationship to implement
the refinement process as a constraint solver for tree-like HCCSs. For example,
refuting a counterexample in a typical CEGAR-based verification of sequentialimperative programs is equivalent to solving a tree-like HCCS of the form below
where x̄ are the variables in the program, and each θi is a formula on x̄ and x̄′ that
expresses the semantics of symbolically executing the corresponding segment(e.g., basic block) in the path:θ1 ⇢ P1 (x̄)θi ∧ Pi (x̄) ⇢ Pi+1 (x̄′ )θ2 ∧ P1 (x̄) ⇢ P2 (x̄′ )⋮⋮Pn (x̄) ⇢ In such a verification, the generator HCCS Hgen(M ) can be described as follows.
Let x̄ be the variables in the program. For each node a in the program’s control
flow graph (CFG), we associate a predicate variable Pa of arity ∣x̄∣. For eachedge from node a to node b in the CFG, we add to Hgen(M ) the Horn clauseθab ∧ Pa (x̄) ⇢ Pb (x̄′ ) where θab is a formula on x̄ and x̄′ expressing the effectof symbolically executing the CFG path from a to b (with x̄ representing thecurrent and x̄′ representing the post state). For the entry node a, we add theHorn clause θinit ⇢ Pa (x̄) where θinit is a formula on x̄ expressing the program’s
initial state. Finally, for each error node a (i.e., assert false statement), we
add the Horn clause Pa (x̄) ⇢ .
Example 4. Recall the program Mex from Example 1. The corresponding generator HCCS Hgen(Mex) is Hex from Example 3. Roughly, the predicate variable
P in the HCCS represents the program states at the time when the first loop is
entered, and Q represents the states when the second loop is entered.
Recall the counterexamples Mexa and Mexb from Example 1, and the treelike HCCSs Hexa and Hexb from Example 3. Hexa corresponds to Mexa and Hexb
corresponds to Mexb . Indeed, as shown in Example 1, {θex1 } (resp. {θ0 , θ1 }) isa proof of Mexa , and Hexa has the corresponding solution σa1 (resp. σa2 ) from
Example 3. Similarly, the solutions σb1 and σb2 of Hexb and the proofs {θex1 }and {θ0 , θ1 , θ2 } of Mexb correspond.
▲
3.2

The Constraint Solver RlxSolveA

RlxSolveA is a relaxed (Lbase , Lbase ∧∨ )-restricted constraint solver. It is parameterized by an exact Lbase -restricted constraint solver that it takes as module.
Let us fix the exact solver, AE Lbase , and write RlxSolveA[AE Lbase ] for RlxSolveAparameterized by the exact solver. Note that Lbase ∧∨ is finite for a finite Lbase .
We briefly overview the construction of RlxSolveA. First, we leverage theequivalence of solving tree-like HCCS and tree interpolation [13] to reduce theproblem to tree interpolation. Then, we adopt the standard proof-based interpolation technique that obtains interpolants from resolution proofs generated
via SMT solving [10], except that we modify the SMT solver to use the exact
Lbase -restricted solver AE Lbase for the theory solver so as to infer Lbase -restricted(partial) interpolants at the theory level of the resolution proof. As we shall show,
this guarantees that if the SMT solver fails to prove, then no Lbase solution exists, and conversely, any inferred solution is guaranteed to be in Lbase ∧∨ .

We describe the approach more formally. First, we review tree interpolation.
The tree interpolation problem takes as input (V, E, Θ) where (V, E) is a finite
directed tree with the node set V and (v, v ′ ) ∈ E denoting that the node v isa direct child of the node v ′ , and the map Θ labels each node v ∈ V with the
T -formula Θ(v). The goal is to find a map I from V to T -formulas, called a treeinterpolant of (V, E, Θ), that satisfies the following.
– I(vrt ) =  for the root node vrt ;– for each v ∈ V , ⊧ Θ(v) ∧ ⋀(v′ ,v)∈E I(v ′ ) ⇒ I(v); and– for each v ∈ V , fvs(I(v)) ⊆ (⋃(v′ ,v)∈E ∗ fvs(Θ(v ′ ))) ∩ (⋃(v′ ,v)∉E ∗ fvs(Θ(v ′ ))).
We reduce constraint solving for a tree-like HCCS to tree interpolation as follows.8 Let H be the input tree-like HCCS. We transform H to an equivalent
HCCS that satisfies: 1.) for each predicate variable P ∈ pvs(H), there exists a
vector of fresh variables x̄P such that P only occurs in the form P (x̄P ), and 2.)
the only sharing of variables among Horn clauses are x̄P ’s between two Hornclauses both containing P . Then, the transformed H is reduced to the tree interpolation problem (VH , EH , ΘH ) where– VH = pvs(H) ∪ {vrt } where vrt ∉ pvs(H);– EH =↝H ∪{(P, vrt ) ∣ θ ∧ . . . P (x̄P ) . . . ⇢  ∈ H};– For each P , ΘH (P ) = θP if θP ∧⋀i Bi ⇢ P (x̄P ) ∈ H and otherwise ΘH (P ) = ;and– ΘH (vrt ) = θrt where θrt ∧ ⋀i Bi ⇢  ∈ H.
The theorem below follows from the construction, and shows the one-to-one
correspondence between the tree interpolants of (VH , EH , ΘH ) and the solutionsof H.
Theorem 3 ([13]). Let H be a tree-like HCCS. Let σ and I be such that I(vrt ) = and for each P ∈ pvs(S), σ(P ) = λx̄P .I(P ). Then, σ ⊧ H if and only if I is atree interpolant of (VH , EH , ΘH ).
Example 5. Recall the tree-like HCCS Hexa from Example 3. The corresponding
tree interpolation problem (V, E, Θ) is shown below where each x̄P1 , x̄P2 , x̄Q1 ,x̄Q2 is a quintuple of fresh variables.
V = {vrt , P1 , P2 , Q1 , Q2 }E = {(P1 , P2 ), (P2 , Q1 ), (Q1 , Q2 ), (Q2 , vrt )}Θ(P2 ) = θp2 [x̄P1 /x̄][x̄P2 /x̄′ ]Θ(P1 ) = θp1 [x̄P1 /x̄]Θ(Q2 ) = θp3 [x̄Q1 /x̄][x̄Q2 /x̄′ ]Θ(Q1 ) = x̄P2 = x̄Q1
Θ(vrt ) = θp4 [x̄Q2 /x̄]▲Now, the relaxed (Lbase , Lbase ∧∨ )-restricted constraint solving problem is reduced to relaxed (Lbase , Lbase ∧∨ )-restricted tree interpolation. That is, we would
like to find tree interpolants restricted to Lbase ∪ Lbase ∧∨ (i.e., Lbase ∧∨ ), with theguarantee to return one if there exists a Lbase -restricted tree interpolant.
8

The reduction is adopted from [13].

AE Lbase (Hthy(C ,V ,E ,Θ) ) = σ∀P.λx̄P .I(P ) = σ(P )(V, E, Θ) ⊢itp C ∶ I

ThyC ∈ Θ(v)Hyp

I(vrt ) = ⎧′∗⎪⎪C↑ ′ if (v, v ) ∈ E∀v ′ .I(v ′ ) = ⎨ v⎪otherwise⎪⎩⊺(V, E, Θ) ⊢itp C ∶ I⎧⎪⎪I1 (v) ∧ I2 (v)∀v.I3 (v) = ⎨⎪⎪⎩I1 (v) ∨ I2 (v)(V, E, Θ) ⊢itp C1 ∨ C2 ∶ I3

(V, E, Θ) ⊢itp p ∨ C1 ∶ I1
(V, E, Θ) ⊢itp ¬p ∨ C2 ∶ I2
Res

if p ∈ outs(v)otherwise

Fig. 5. The tree interpolation rules.

Next, we describe the process of relaxed (Lbase , Lbase ∧∨ )-restricted tree interpolation. In what follows, we assume familiarity with lazy SMT and the proofbased technique for obtaining interpolants from resolution proofs [16, 10]. Let(V, E, Θ) be the tree interpolation instance to be solved. In an ordinary proofbased tree interpolation, one looks for tree interpolants by having the SMT solver
check the unsatisfiability of ⋀v∈V Θ(v) and analyzing the output resolution proof
to compute the interpolant. However, this decides the existence of, and infers,
a tree interpolant from the entire T , and is unsuitable for our task (i.e., thisresults in an unrestricted constraint solver).
Instead, we modify the SMT solver so that its theory-level reasoning is delegated to the exact Lbase -restricted constraint solver AE Lbase . More specifically,
when the SMT solver builds a model of possible (propositional) satisfying assignment ¬C, instead of passing the model to a theory solver as in ordinary SMT,
we build a “fragment” HCCS Hthy(C ,V ,E ,Θ) that just contains the part of thetree interpolation problem touched by the literals in C. Formally,
Hthy(C ,V ,E ,Θ) = {¬C↡v ∧ ⋀(P,v)∈E P (x̄P ) ⇢ Hv ∣ v ∈ V }where C↡v is the set of literals of C over atomic predicates occurring in Θ(v),and Hv =  if v = vrt and Hv = Q(x̄Q ) if v is a predicate variable Q. We pass
Hthy(C ,V ,E ,Θ) to AE Lbase to decide if it has a Lbase restricted solution, and if
so, we set the obtained solution as the partial tree interpolant for the theorylevel resolution proof nodes where C occurs as the theory lemma. Otherwise,
we can safely reject that the whole problem as having no Lbase -restricted treeinterpolant and return noproof. To generate the tree interpolant for the whole,
we adopt the proof-based approach that builds the tree interpolant in a bottom
up manner following the rules shown in Figure 5.9 Here, outs(v) is the set of
atomic predicates occurring outside of the subtree rooted at v (i.e., outs(v) =9

We assume that each Θ(v) is CNF (if not, they can be transformed so via the Tseitintransformation [19]).

{p ∣ p occurs in Θ(v ′ ) where (v ′ , v) ∉ E ∗ }), and C↑v is the set of literals of C
over the atomic predicates occurring outside of the subtree rooted at v (i.e.,C↑v = {p ∈ C ∣ p ∈ outs(v)} ∪ {¬p ∈ C ∣ p ∈ outs(v)}). The rules Hyp for clausesin the input tree and Res for resolution steps extend the analogous rules fromthe standard proof-based interpolation [10] to tree interpolation. As describedabove, Thy uses the Lbase -restricted solution computed by the exact solver forthe partial tree interpolant. As we show in Theorems 4 and 5 below, this achieves
the desired relaxed (Lbase , Lbase ∧∨ )-restricted tree interpolation.
First, we show that any tree interpolant obtained by the method is restricted
to Lbase ∧∨ .
Theorem 4. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose (V, E, Θ) ⊢itp  ∶ I. Then, I is a tree interpolantof (V, E, Θ), and for all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase ∧∨ .
Next, we prove that if there is a Lbase -restricted tree interpolant for the given
tree interpolation instance, then the method infers some tree interpolant (andby Theorem 4 above, such a tree interpolant will be restricted to Lbase ∧∨ ).
Theorem 5. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose there is a tree interpolant I of (V, E, Θ) such thatfor all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase . Then, (V, E, Θ) ⊢itp  ∶ I ′ for some I ′ .
We note that Hthy(C ,V ,E ,Θ) is always a conjunctive HCCS and is often muchsmaller than the input HCCS. Therefore, the expensive exact Lbase -restrictedconstraint solver AE Lbase is only applied to small conjunctive HCCSs, thereby
making its job easier. Also, we note that, while we have presented RlxSolveA to beparameterized by an exact Lbase -restricted constraint solver passed as module,
the algorithm actually works even if a relaxed (Lbase , Lext )-restricted constraint
solver is used in place of the exact Lbase -restricted constraint solver.10 Therefore,
RlxSolveA can actually be parameterized by RlxSolveA itself, but the solvers mustbe “primed” by some exact solver (e.g., RlxSolveA[RlxSolveA[AE Lbase ]]).
Minimizing Theory Lemmas. When ¬C is given as a possible propositionalmodel by the SMT solver, we use the exact finite-language-restricted constraint
solver AE Lbase to find a solution for Hthy(C ,V ,E ,Θ) . But, using C directly as
the theory lemma after AE Lbase finds a solution could result in the SMT solver
producing many propositional models and lead to bad performance. (This isanalogous to using C directly as the theory lemma in an ordinary lazy SMT
solving when the theory solver finds ¬C unsatisfiable.) Instead, we let AE Lbase
return the subset of the literals of C that it used to find the solution, and use
it to obtain a smaller theory lemma. (We refer to the extended report [18] formore detail.)
10

More precisely, it becomes a relaxed (Lbase , Lext ∧∨ )-restricted constraint solver when
passed a relaxed (Lbase , Lext )-restricted constraint solver.

3.3

The Constraint Solver RlxSolveB

RlxSolveB is a relaxed (Lbase , LB(Lbase ∪Lext , AU , ℓ))-restricted constraint solver
which takes as module a relaxed (Lbase , Lext )-restricted constraint solver, an unrestricted constraint solver AU, and a positive integer parameter ℓ. LB(L, AU, ℓ)
is a finite language of predicates determined by L, AU , and ℓ.
We informally describe RlxSolveB. We select some fraction of predicate variables in a certain “fair” manner based on the parameter ℓ and use the relaxed(Lbase , Lext )-restricted solver provided as a module to look for solutions to justthe selected predicate variables. After restricted solutions are obtained for theselected predicate variables, we use AU to look for unrestricted solutions to theremaining predicate variables, and return the combined solution as the solution
for the input HCCS. Note that this technique reduces the number of predicate
variables that the given relaxed (Lbase , Lext )-restricted solver needs to solve for,and therefore can be used to improve the performance of a relaxed (Lbase , Lext )restricted solver. The key observation we use here is that HCCSs solved in arefinement process are all unwound instances of a fixed “generator” HCCS (i.e.,
Hgen(M )). As we shall show next, the observation can be used to guaranteethat the result is a relaxed finite-language-restricted solver, when the predicate
variable selection is done in a certain proper way.
We describe the constraint solving algorithm in detail. In what follows, we
extend the definition of a tree-like HCCS (cf. Section 3.1) so that the root clausecan be a Horn clause whose head is of the form P (x̄) where P does not occur
anywhere else in the HCCS. For such an HCCS H, we say that P is the root of
H and write root(H) = P (root(H) =  for H with a -head root clause).
01: RlxSolveB[AR(Lbase ,Lext ) , AU , ℓ](H) =02: let Y = partition(ℓ, H) in
03: let A = ⋃H′ ∈Y {root(H′ )} ∖ {} in
04: let HA = rewrite(H, A) in
05: match AR(Lbase ,Lext ) (HA ) with
06:
noproof → return noproof07:∣ sol(σA ) → return sol(σA ∪ ⋃H′ ∈Y AU (σA (H′ )))Fig. 6. The overview of RlxSolveB.

Let RlxSolveB be parameterized by the relaxed (Lbase , Lext )-restricted constraint solver AR(Lbase ,Lext ) , the unrestricted constraint solver AU , and the positive integer ℓ. Figure 6 shows the overview of RlxSolveB. RlxSolveB first partitions
the input HCCS H into a set of tree-like HCCSs of depth at most ℓ in a top-downmanner (line 2). Formally, partition is defined as follows.
partition(ℓ,H) =if depth(H) ≤ ℓ then {H}else let H′ , X = subtrees(ℓ, H) in{H′ } ∪ ⋃H∈X partition(ℓ, H)

Here, subtrees(ℓ, H) returns the pair (H′ , X) such that 1.) H′ is the largest treelike subset of H containing the root clause of H and depth(H′ ) = ℓ, and 2.) X
is the set of subtrees of H rooted at each leaf of H′ . It is easy to see that Y
partitions H (i.e., H = ⋃ Y and ∀H1 , H2 ∈ Y.H1 ≠ H2 ⇒ H1 ∩ H2 = ∅), and thateach H′ ∈ Y is a tree-like HCCS of depth at most ℓ. In fact, the partition is thecoarsest of such partitions, where the only HCCSs in the partition having depth
less than ℓ are the ones whose leaf predicate variables do not appear anywhere
else in the partition.
By construction, only the root predicate variables are shared by different
HCCSs in Y (more precisely, a root of one HCCS appears as a leaf in another
HCCS). RlxSolveB selects these shared predicate variables to be the ones toinfer restricted solutions (line 3). It can be seen that the fraction of the selected
predicate variables, that is ∣A∣/∣pvs(H)∣, is inversely proportional to the size of adepth ℓ tree-like subset of H, and decreases rapidly as ℓ is increased.
To infer restricted solutions to A, RlxSolveB constructs the HCCS HA suchthat pvs(HA ) = A, and solutions of HA correspond exactly to the solutions of
H restricted to A (i.e., σ ⊧ HA if and only if ∃σ ′ .σ ′ ↾A = σ ∧ σ ′ ⊧ H ). This isdone by the operation rewrite(H, A) (line4), defined to be the application of thefollowing rewriting relation ↠ to H until convergence.
H′ ∪ {Φ1 ⇢ P (x̄), Φ2 ∧ P (ȳ) ⇢ H} ↠ H′ ∪ {Φ2 ∧ Φ1 [ȳ/x̄] ⇢ H}
Here, P ∈ pvs(H) ∖ A, and Φi ’s range over Horn clause bodies. (We assume thateach Horn clause in H is over disjoint variables. Otherwise, we transform H intosuch a form by variable renaming.)
Then, RlxSolveB calls AR(Lbase ,Lext ) to find a Lbase ∪ Lext -restricted solutionfor HA (line 5). If AR(Lbase ,Lext ) returns noproof then no Lbase solution exists for
HA by the property of AR(Lbase ,Lext ) , and by the construction above, it can beshown that no Lbase solution exists for the input HCCS H either, and we safely
return noproof (line 6) (see Theorem 7 for the proof). Otherwise, we obtain asolution σA for HA , and RlxSolveB calls AU on each element of the partition
with the solution σA substituted (i.e., AU (σA (H′ )) for each H′ ∈ Y ).11 This
gives solutions for the remaining predicate variables in H, and we return theunion of σA and these solutions as the final solution (line 7).
We argue that the produced solution is indeed a solution of H. Let Y ={H1 , . . . , Hn }. Note that the only predicate variables shared by different elements in Y are A. Therefore, σA (H1 ),. . . ,σA (Hn ), and HA are over disjoint
predicate variables, and their solutions are over disjoint domains. Then, because
Y partitions H, it follows that σA ∪ ⋃H′ ∈Y AU (σA (H′ )) is a solution of H.
To show that RlxSolveB is a relaxed finite-language-restricted constraint solver,
it remains to show that the obtained solution is restricted to a finite languageof predicates. We show that it is restricted to LB(Lbase ∪ Lext , AU , ℓ) which is
11Here, we extend the notion of substitution so that the result is tree-like: for P ∈dom(σA ), σA (Φ ⇢ P (x̄)) = ¬σA (P )[x̄/ν̃(P )] ∧ σA (Φ) ⇢ .

defined as follows. Let L be a finite language. We define LB(L, AU, ℓ) as follows.
LB(L, AU, ℓ) = L ∪ ⋃H′ ∈X ran(AU (H′ ))where
X = {σ(H′ ) ∣ H′ ∈ unwds(ℓ, Hgen(M )) and σ ⪰L H′ }Here, M is the program being verified (i.e., the input to the top-level procedure
RlxCegar), unwds(ℓ, H) is the set of unwound instances of H of depth at most ℓ,and σ ⪰L H if and only if σ is a map from the leaves and the root of H to thepredicates in L (i.e., dom(σ) = leaves(H)∪{root(H)}∖{} and ran(H) ⊆ L). Notethat Hgen(M ) is a constant for the entire run of RlxCegar(M ), and unwds(ℓ, H)is finite for any H and ℓ. Therefore, LB(L, AU, ℓ) is a finite language that isdetermined by L, AU and ℓ.
We formally prove that RlxSolveB is indeed a relaxed (Lbase , LB(Lbase ∪Lext , AU , ℓ))-restricted constraint solver. First, we prove that the solution returned is indeed a solution of the input HCCS and that it is restricted to
LB(Lbase ∪ Lext , AU , ℓ).
Theorem 6. Suppose RlxSolveB[AR(Lbase ,Lext ) , AU , ℓ](H) returns sol(σ). Then,σ ⊧ H and ran(σ) ⊆ LB(Lbase ∪ Lext , AU, ℓ).
Next, we show that some solution is returned if there exists a Lbase -restricted
solution to the given HCCS (and by Theorem 6, such a solution is restricted to
LB(Lbase ∪ Lext , AU , ℓ)).
Theorem 7. Suppose that there exists σ such that σ ⊧ H and ran(σ) ⊆ Lbase .
Then, RlxSolveB[AR(Lbase ,Lext ) , AU, ℓ](H) infers some σ ′ such that σ ′ ⊧ H.
Example 6. Recall the HCCS Hexa from Example 3. Running RlxSolveB on Hexa
with ℓ = 2, we have Y = partition(2, Hexa ) = {H1 , H2 , H3 } where
H1 = {θp3 ∧ Q1 (x̄) ⇢ Q2 (x̄′ ), θp4 ∧ Q2 (x̄) ⇢ }
H2 = {θp2 ∧ P1 (x̄) ⇢ P2 (x̄′ ), P2 (x̄) ⇢ Q1 (x̄)}
H3 = {θp1 ⇢ P1 (x̄)}
Then, the shared predicate variables that are selected to be restricted are A ={root(H1 ), root(H2 ), root(H3 )} ∖ {} = {P1 , Q1 }. And, HA = rewrite(Hexa , A) is
as shown below.
HA = {θp3 ∧ Q1 (x̄) ∧ θp4 [x̄′ , x̄′′ /x̄, x̄′ ] ⇢ , θp2 ∧ P1 (x̄) ⇢ Q1 (x̄′ ), θp1 ⇢ P1 (x̄)}
where x̄′′ is a quintuple of fresh variables. RlxSolveB then calls AR(Lbase ,Lext )on HA to obtain a restricted solution for A. Suppose the returned solution isσA = {P ↦ a = b ⇒ y = z + x ∣ P ∈ {P1 , Q1 }}. Then, σA is applied to each elementof the partition and we obtain σA (H1 ), σA (H2 ), and σA (H3 ) shown below.
σA (H1 ) = {θp3 ∧ (a = b ⇒ y = x + z) ⇢ Q2 (x̄′ ), θp4 ∧ Q2 (x̄) ⇢ }σA (H2 ) = {θp2 ∧ (a = b ⇒ y = x + z) ⇢ P2 (x̄′ ), a = b ∧ y ≠ x + z ∧ P2 (x̄) ⇢ }σA (H3 ) = {a = b ∧ y ≠ x + z ∧ θp1 ⇢ }

AU is called on σA (H1 ), σA (H2 ), and σA (H3 ) to infer unrestricted solutions
to the remaining predicate variables. Suppose we have obtained the solutions
σ1 = {Q2 ↦ a = b ⇒ z ≠ −1 ∧ y = x + z}, σ2 = {P2 ↦ a = b ⇒ y = x + z}, and σ3 = ∅for σA (H1 ), σA (H2 ), and σA (H3 ) respectively. Finally, RlxSolveB returns the
combined map, σA ∪ σ1 ∪ σ2 ∪ σ3 , as the solution inferred for the input HCCS
Hexa .
▲

4

Implementation and Experiments

We have implemented the new refinement algorithms RlxSolveA and RlxSolveB
described in Section 3. The refinement algorithms require an exact finite-languagerestricted constraint solver and an unrestricted constraint solver to be provided
as modules. An unrestricted constraint solver finds unrestricted solutions to thegiven tree-like HCCS. This is the ordinary constraint solving for tree-like HCCSs
which is a well-studied problem, and we use the existing technique that iteratively solve the constraints one predicate variable at a time by using interpolation
as a blackbox process (see [20, 4, 17] for details).12
Exact Finite-Language-Restricted Constraint Solver. For the exact solver,
we use a simple approach in which the finite predicate languages are represented
by predicate templates containing unknowns of bounded range. We use an SMT
solver13 to find an assignment to the unknowns within the bound that makes
the templates into an actual solution. Below, we informally describe the processby an example, and defer the detailed description to the extended report [18].
Example 7. Recall the program Mex from Example 1. Let Lbase be the finite language of predicates consisting of conjunctions of at most two atomic predicateswhose numeric constants are bounded in the range {−1, 0, 1}. We represent thelanguage by the bounded predicate template shown below
λa, b, x, y, z. c1 a + c2 b + c3 x + c4 y + c5 z + c6 ≤ 0∧
c7 a + c8 b + c9 x + c10 y + c11 z + c12 ≤ 0
where ci ’s are unknown constants each associated with the bound {−1, 0, 1}.
Bounded predicate templates can concisely represent a finite language of predicates.14
Let ξ be a bounded predicate template. To check if the given HCCS H has asolution in the language represented by ξ, we make a solution template σξ thatmaps each predicate variable in H to a copy of ξ with fresh unknowns. Then,
we check if there exists an assignment to the unknowns within the bounds thatmakes the solution template into an actual solution of H, that is, we look for
assignments to the unknowns within the bounds that satisfy ∀hc ∈ σξ (H). ⊧ hc.
12

The implementation uses MathSAT 5 (http://mathsat.fbk.eu/) for the backend
interpolation process.
13
The implementation uses Z3 (http://z3.codeplex.com/).
14
Note that such a language is generally not closed under conjunctions or disjunctions.

For QFLRA, the latter can be done by applying the Motzkin’s transposition
theorem [15] to reduce the problem to the satisfiability problem for quantifierfree non-linear real arithmetic, and using an SMT solver to solve the resulting
problem.
▲
We note that the exact finite-language-restricted constraint solving is a highly
expensive process and using it directly solve the whole HCCS is prohibitive.
Indeed, as we show in the experiments, the exact solver fails to scale even on
relatively small constraint sets (see also the discussion in Section 5 and thecomplexity theoretic analysis in the extended report [18]).
Experiment Setup. We have experimented with the new refinement algorithms
by using them in the refinement process of MoCHi [8]. MoCHi is a state-of-the-art
software model checker for higher-order functional programs based on predicate
abstraction, CEGAR, and higher-order-recursion-scheme (HORS) model checking. MoCHi verifies assertion safety of OCaml programs. A verifier for functional
programs such as MoCHi is suited for experimenting with the new refinement
algorithm because Horn-clause constraints generated in such a verifier often contain non-trivial tree-like structure. (Intuitively, this is because the constraints
express the flow of data in the program, and data often flow in a complex way
in a functional program, e.g., passed to and returned from recursive functions,captured in closures, etc.)
The new refinement algorithms RlxSolveA and RlxSolveB are parametric. For
this experiment, we parameterize them as follows to obtain a single refinement
algorithm:
RlxSolveB[RlxSolveA[AE Lbase ], AU , 4]Here, the exact Lbase -restricted constraint solver AE Lbase and the unrestricted
solver AU are the ones described above. That is, we use RlxSolveB parameterized to use as modules the relaxed (Lbase , (Lbase )∧∨ )-restricted constraint solver
RlxSolveA (itself parameterized by the exact Lbase -restricted constraint solver
AE Lbase ) and the unrestricted constraint solver AU , and with the parameterℓ = 4. The strata of restricting predicate languages are built “dynamically” as
the CEGAR iteration progresses, by starting from a small fixed (L0base , L0ext )and enlarging the current (Lbase , Lext ) whenever the refinement algorithm returns noproof by using the unrestricted refinement process.15
We compare the new refinement algorithm with two other refinement methods: 1.) the ordinary (incomplete) unrestricted predicate search, and 2.) exact
finite-language-restricted predicate search. The unrestricted predicate search algorithm is AU , and the exact finite-language restricted predicate search algorithm is AE. For AE, we give (the Lbase part of) the same restricting predicate
language given to the new algorithm when solving the corresponding HCCS.
We have ran the three refinement algorithms on 318 HCCSs generated byrunning MoCHi on 139 programs, measuring the time spent in each run of the15

Formally, this is done by having a non-decreasing preorder of restricting predicate
languages where the limit of any ω-chain is T , and when noproof is returned, thelanguage raised to the least one containing the predicate inferred by AU.

refinement process. The benchmark programs are mostly taken from the previous work on MoCHi [8, 14, 22, 9]. To obtain the benchmark HCCS set, we ran
MoCHi on each benchmark program with the new refinement algorithm until
completion or timeout and recorded the HCCS given as the input to each run of
the refinement process. We also compare the overall verification speed of MoCHi
when using the three refinement algorithms. This is done by running MoCHi
with each of the refinement algorithm on the 139 benchmark programs. We haverun the experiments on a machine with 2.69 GHz i7-4600U processor with 16
GB of RAM, with the time limit of 100 seconds. The benchmark programs, thebenchmark HCCSs and the experiment results data are available online [18].
Experiment Aim and Hypothesis. Because of the overhead from computing
restricted proofs, we expect the individual refinement runs to be slower with
the new refinement algorithm compared to an ordinary incomplete approach
which only does unrestricted refinement, but faster than the more naı̈ve complete
approach that directly applies the exact finite-language-restricted proof search
to the entire refinement problem. The main purpose of the experiment is totest this hypothesis. We also compare the overall verification speeds, but we
do not expect a significant improvement on this aspect because of the inherent
complexity of the verification problem. (For any sound and QFLRA-complete
verifier, one can always find a program on which the verifier takes arbitrarily
long time.)
Experiment Results and Analysis. Figure 7 shows the plots comparing thethe run times of the new refinement algorithm (New Algorithm), the unrestrictedrefinement algorithm (Unrestricted), and the exact finite-language-restricted refinement algorithm (Exact) on each of the 318 benchmark HCCSs. As we haveexpected, the unrestricted refinement algorithm is the fastest of the three. The
new algorithm performs quite competitively, however, and shows that it is able
to achieve completeness with only a low overhead. Also, the plots show thatthe exact finite-language-restricted refinement algorithm is significantly slower,
timing out on many instances that the other two algorithms were able to solve
quickly.
Figure 8 shows the plots comparing the run times of the overall verification
process on each of the 139 benchmark programs for each refinement algorithm.
The plots show that there is no clear winner in this comparison and none of
the three outperformed the others on all benchmarks (while the unrestrictedrefinement edged out in the number of instances solved within the time limit,
it also timed out on some instances the complete methods were able to solve).
This is due to the inherent undecidability of the program verification problem,
and the fact that the speed of overall verification depends heavily on subtle
heuristic choices made by MoCHi. Such issues are largely outside of the scopeof this paper, but they give interesting insights into what would be the goodheuristics to use with the new refinement algorithm. For instance, an interesting
behavior we have observed is that the stratified approaches (New Algorithm andExact) sometimes infer more useless predicates than the ordinary unrestrictedrefinement because a stratified approach needs to add predicates to raise the lan-

100

10

10

1

1

Exact

Unrestricted

100

0.1

0.1

0.01

0.01

0.001
0.001

0.01

0.1

1

10

0.001
0.001

100

0.01

0.1

1

10

100

NewAlgorithm

NewAlgorithm

100

100

10

10

1

1

Exact

Unrestricted

Fig. 7. Run time comparison of the refinement algorithms on benchmarks HCCSs

0.1

0.1

0.01

0.01

0.001
0.001

0.01

0.1

1

NewAlgorithm

10

100

0.001
0.001

0.01

0.1

1

10

100

NewAlgorithm

Fig. 8. Run time comparison of the refinement algorithms on benchmarks programs

guage stratum till it reaches the level where a proof of the given program exists.
Because MoCHi does eager predicate abstraction, its performance degrades exponentially in the number of predicates that are added to the candidate predicate
set. This seems to have had a large negative impact on the stratified approaches.
A possible way to address the issue maybe is to have MoCHi take a more lazy
approach to predicate abstraction, or allow the language strata “coarseness” tobe dynamically adjustable so that we can immediately jump to a large predicate
language when it seems beneficial.

5

Related Work

Previous work [7, 11] has considered an exact stratification approach which requires the refinement process to exactly decide if a proof of the given counterex-

ample’s spuriousness exists in the current finite language stratum. As remarked
before, an issue with exact stratification is the high cost of exact finite-languagerestricted proof search. As we have shown empirically in Section 4, the exact
finite-language-restricted proof search suffers from high overhead. (We also showcomplexity theoretic evidences for the inherent hardness of the exact search in
the extended report [18].) We note that relaxed stratification is a generalizationof exact stratification. That is, exact stratification is a special case of relaxedstratification where Lext = ∅.
We note that the interpolation technique that limits the theory-level reasoning to only emit restricted partial interpolants (cf. Section 3.2) has also been
proposed in [7]. But, they target exact stratification and therefore requires the
restricting language to be closed under conjunctions and disjunctions (so thatL∧∨ = L), which substantially reduces the applicability of the technique.16

6

Conclusion

We have presented a new approach to complete predicate refinement, called
relaxed stratification, where the background theory is stratified into a sequenceof finite predicate languages(L0base , L0ext ), (L1base , L1ext ), . . . (Lkbase , Lkext ), . . .
such that each run of the refinement process is restricted to only infer predicates from the current stratum Lbase ∪ Lext . Contrary to previous approaches
to complete refinement, the refinement process is neither required to decide theexistence of a proof for the given counterexample in Lbase ∪Lext nor in Lbase , but
is only required to return some proof if one exists in Lbase . We have proved thatthe approach is complete despite the relaxed requirement, assuming that thestrata of Lbase ’s grow to eventually cover the predicates of the underlying theory. We have shown that the relaxed requirement can be used to build practicalrefinement algorithms that have low overhead and the completeness guarantee.

References
1. S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing
software verifiers from proof rules. In J. Vitek, H. Lin, and F. Tip, editors, PLDI,
pages 405–416. ACM, 2012.
2. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement
for verifying multi-threaded programs. In T. Ball and M. Sagiv, editors, POPL,
pages 331–344. ACM, 2011.
16

Contrary to [7], in QFLRA, it is insufficient to only look for an atomic interpolant(i.e., a separating hyperplane) when interpolating between even just conjunctionsof literals (i.e., polytopes) under a finite-language restriction. For example, consider
interpolating between y ≤ 1 ∧ 2x + y ≤ −3 ∧ x ≤ −1 and y + x ≥ 1 under the restrictionthat interpolants’ constants are in {−1, 0, 1}.

3. A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses over
LI+UIF. In H. Yang, editor, APLAS, volume 7078 of Lecture Notes in Computer
Science, pages 188–203. Springer, 2011.
4. M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In M. V.
Hermenegildo and J. Palsberg, editors, POPL, pages 471–482. ACM, 2010.
5. 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.
6. R. Jhala and R. Majumdar. Software model checking. ACM Computing Surveys,
41(4), 2009.
7. 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.
8. N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for
higher-order model checking. In M. W. Hall and D. A. Padua, editors, PLDI,
pages 222–233. ACM, 2011.
9. T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination
verification for higher-order functional programs. In Z. Shao, editor, ESOP, volume8410 of Lecture Notes in Computer Science, pages 392–411. Springer, 2014.
10. K. L. McMillan. An interpolating theorem prover. Theoretical Computer Science,
345(1):101–121, 2005.
11. 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.
12. P. Rümmer, H. Hojjat, and V. Kuncak. Classifying and solving horn clauses forverification. In E. Cohen and A. Rybalchenko, editors, VSTTE, volume 8164 of
Lecture Notes in Computer Science, pages 1–21. Springer, 2013.
13. 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.
14. R. Sato, H. Unno, and N. Kobayashi. Towards a scalable software model checker
for higher-order programs. In E. Albert and S. Mu, editors, PEPM, pages 53–62.
ACM, 2013.
15. A. Schrijver. Theory of linear and integer programming. Wiley, 1998.
16. R. Sebastiani. Lazy satisability modulo theories. JSAT, 3(3-4):141–224, 2007.
17. T. Terauchi. Dependent types from counterexamples. In M. V. Hermenegildo and
J. Palsberg, editors, POPL, pages 119–130. ACM, 2010.
18. T. Terauchi and H. Unno. Relaxed stratification: A new approach to practicalcomplete predicate refinement. 2015. http://www.jaist.ac.jp/~ terauchi.
19. G. S. Tseitin. On the complexity of derivation in propositional calculus. Studies
in constructive mathematics and mathematical logic, 2(115-125):10–13, 1968.
20. 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.
21. H. Unno and T. Terauchi. Inferring simple solutions to recursion-free horn clauses
via sampling. In TACAS, 2015. To appear.
22. H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In R. Giacobazzi and R. Cousot, editors,
POPL, pages 75–86. ACM, 2013.