Automating Induction for Solving Horn Clauses
Hiroshi Unno, Sho Torii, and Hiroki Sakamoto
University of Tsukuba{uhiro,sho,sakamoto}@logic.cs.tsukuba.ac.jp

a ct ** Consi

se
eu

um
e

*

at e d1* Easy toed
Rnt

Abstract. Verification problems of programs in various paradigms canbe reduced to problems of solving Horn clause constraints on predicate variables that represent unknown inductive invariants. This paper presents a novel Horn constraint solving method based on inductive
theorem proving: the method reduces Horn constraint solving to validity checking of first-order formulas with inductively defined predicates,
which are then checked by induction on the derivation of the predicates.
To automate inductive proofs, we introduce a novel proof system tailored to Horn constraint solving, and use a PDR-based Horn constraint
solver as well as an SMT solver to discharge proof obligations arisingin the proof search. We prove that our proof system satisfies the soundness and relative completeness with respect to ordinary Horn constraint
solving schemes. The two main advantages of the proposed method arethat (1) it can deal with constraints over any background theories supported by the underlying SMT solver, including nonlinear arithmetic
and algebraic data structures, and (2) the method can verify relational
specifications across programs in various paradigms where multiple function calls need to be analyzed simultaneously. The class of specifications
includes practically important ones such as functional equivalence, associativity, commutativity, distributivity, monotonicity, idempotency, andnon-interference. Our novel combination of Horn clause constraints withinductive theorem proving enables us to naturally and automaticallyaxiomatize recursive functions that are possibly non-terminating, nondeterministic, higher-order, exception-raising, and over non-inductively
defined data types. We have implemented a relational verification tool
for the OCaml functional language based on the proposed method andobtained promising results in preliminary experiments.

Introduction

Verification problems of programs written in various paradigms, including imperative [30], logic, concurrent [28], functional [47, 54, 55, 59], and object-oriented [36]ones, can be reduced to problems of solving Horn clause constraints on predicate variables that represent unknown inductive invariants. A given program isguaranteed to satisfy its specification if the Horn constraints generated from theprogram have a solution (see [27] for an overview of the approach).
This paper presents a novel Horn constraint solving method based on inductive theorem proving: the method reduces Horn constraint solving to validity

alu

CAV *

l
We

st

* Complete

*

t
en

C*
AE l Doc Ev

A

rtif

checking of first-order formulas with inductively defined predicates, which arethen checked by induction on the derivation of the predicates. The main technicalchallenge here is how to automate inductive proofs. To this end, we propose an
inductive proof system tailored for Horn constraint solving and a technique basedon SMT and PDR [10] to automate proof search in the system. Furthermore,
we prove that the proof system satisfies the soundness and relative completenesswith respect to ordinary Horn constraint solving schemes.
Compared to previous Horn constraint solving methods [27, 29, 32, 33, 41, 48,
52, 55, 57] based on Craig interpolation [21, 42], abstract interpretation [20], and
PDR, the proposed method has two major advantages:
1. It can solve Horn clause constraints over any background theories supportedby the underlying SMT solver. Our method solved constraints over the theories of nonlinear arithmetic and algebraic data structures, which are notsupported by most existing Horn constraint solvers.
2. It can verify relational specifications where multiple function calls need to
be analyzed simultaneously. The class of specifications includes practicallyimportant ones such as functional equivalence, associativity, commutativity,
distributivity, monotonicity, idempotency, and non-interference.
To show the usefulness of our approach, we have implemented a relational verification tool for the OCaml functional language based on the proposed method
and obtained promising results in preliminary experiments.
For an example of the reduction from (relational) verification to Horn constraint solving, consider the following OCaml program Dmult .1
let rec mult x y = if y=0 then 0 else x + mult x (y-1)
let rec mult_acc x y a = if y=0 then a else mult_acc x (y-1) (a+x)
let main x y a = assert (mult x y + a = mult_acc x y a)Here, the function mult takes two integer arguments x, y and recursively computes x × y (note that mult never terminates if y < 0). mult acc is a tailrecursive version of mult with an accumulator a. The function main contains
an assertion with the condition mult x y + a = mult_acc x y a, which represents a relational specification, namely, the functional equivalence of multand mult acc. Our verification problem here is whether for any integers x, y,and a, the evaluation of main x y a, under the call-by-value evaluation strategy adopted by OCaml, never causes an assertion failure, that is ∀x, y, a ∈N. main x y a−→
6 ∗ assert false. By using a constraint generation method forfunctional programs [55], the relational verification problem is reduced to theconstraint solving problem of the following Horn clause constraint set Hmult :P (x, y, x + r) ⇐ P (x, y − 1, r) ∧ (y 6= 0),
 P (x, 0, 0),Q(x, 0, a, a), Q(x, y, a, r) ⇐ Q(x, y − 1, a + x, r) ∧ (y 6= 0),⊥ ⇐ P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ∧ (r1 + a 6= r2 )1

Our work also applies to programs that require a path-sensitive analysis of intricate
control flows caused by non-termination, non-determinism, higher-order functions,and exceptions but, for illustration purposes, we use this as a running example.

2Here, the predicate variable P (resp. Q) represents an inductive invariant among
the arguments and the return value of the function mult (resp. mult acc). The
first Horn clause P (x, 0, 0) is generated from the then-branch of the definition ofmult and expresses that mult returns 0 if 0 is given as the second argument. The
second clause in Hmult , P (x, y, x + r) ⇐ P (x, y − 1, r) ∧ (y 6= 0) is generated fromthe else-branch and represents that mult returns x+r if the second argument y is
non-zero and r is returned by the recursive call mult x (y-1). The other Hornclauses are similarly generated from the then- and else- branches of mult acc andthe assertion in main. Because Hmult has a satisfying substitution (i.e., solution)
θmult = {P 7→ λ(x, y, r).x × y = r, Q 7→ λ(x, y, a, r).x × y + a = r} for thepredicate variables P and Q, the correctness of the constraint generation [55]guarantees that the evaluation of main x y a never causes an assertion failure.
The previous Horn constraint solving methods, however, cannot solve thiskind of constraints that require a relational analysis of multiple predicates. To see
why, recall the constraint in Hmult , ⊥ ⇐ P (x, y, r1 )∧Q(x, y, a, r2 )∧(r1 +a 6= r2 )which asserts the equivalence of mult and mult acc, where a relational analysis of the two predicates P and Q is required. The previous methods, however,analyze each predicate P and Q separately, and therefore must infer nonlinear invariants r1 = x × y and r2 = x × y + a respectively for the predicate
applications P (x, y, r1 ) and Q(x, y, a, r2 ) to conclude r1 + a = r2 by cancelingx × y, because x and y are the only shared arguments between P (x, y, r1 ) andQ(x, y, a, r2 ). The previous methods can only find solutions that are expressible
by efficiently decidable theories such as the quantifier-free linear real (QF LRA)
and integer (QF LIA) arithmetic2 , which are not powerful enough to express theabove nonlinear invariants and the solution θmult of Hmult .
By contrast, our induction-based Horn constraint solving method can directly and automatically show that the predicate applications P (x, y, r1 ) andQ(x, y, a, r2 ) imply r1 + a = r2 (i.e., Hmult is solvable), by simultaneously analyzing the two. More precisely, our method interprets P, Q as the predicates
inductively defined by the definite clauses (i.e., the clauses whose head is a predicate application), and uses induction on the derivation of P (x, y, r1 ) to prove theconjecture ∀x, y, r1 , a, r2 .(P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ∧ (r1 + a 6= r2 ) ⇒ ⊥) denotedby the goal clause (i.e., the clause whose head is not a predicate application).
The use of Horn clause constraints, which can be considered as an Intermediate Verification Language (IVL) common to Horn constraint solvers and target languages, enables our method to verify relational specifications across programs written in various paradigms. Horn constraints can naturally axiomatize
various advanced language features including recursive functions that are partial (i.e., possibly non-terminating), non-deterministic, higher-order, exceptionraising, and over non-inductively defined data types (recall that Hmult axiomatizes the partial functions mult and mult acc, and see the full version [58] formore examples). Furthermore, we can automate the axiomatization process byusing program logics such as Hoare logics for imperative and refinement type systems [47, 54, 55, 60] for functional programs. In fact, researchers have developed2

See http://smt-lib.org/ for the definition of the theories.

3and made available tools such as SeaHorn [30] and JayHorn [36], respectively
for translating C and Java programs into Horn constraints. Despite their expressiveness, Horn constraints have a simpler logical semantics than other popular
IVLs like Boogie [3] and Why3 [8]. The simplicity enabled us to directly apply
inductive theorem proving and made the proofs and implementation easier.
In contrast to our method based on the logic of predicates defined by Hornclause constraints, most state-of-the-art automated inductive theorem provers
such as ACL2s [15], Leon [50], Dafny [40], Zeno [49], HipSpec [18], and CVC4 [46]are based on logics of pure total functions over inductively-defined data structures. Some of them support powerful induction schemes such as recursion induction [43] and well-founded induction (if the termination arguments for the recursive functions are given). However, the axiomatization process often requires
users’ manual intervention and possibly has a negative effect on the automationof induction later, because one needs to take into consideration the evaluation
strategies and complex control flows caused by higher-order functions and sideeffects such as non-termination, exceptions, and non-determinism. Furthermore,
the process needs to preserve branching and calling context information for pathand context-sensitive verification. Thus, our approach complements automatedinductive theorem proving with the expressive power of Horn clause constraints
and, from the opposite point of view, opens the way to leveraging the achievements of the automated induction community into Horn constraint solving.
The rest of the paper is organized as follows. In Section 2, we will give an
overview of our induction-based Horn constraint solving method. Section 3 defines Horn constraint solving problems and proves the correctness of the reduction from constraint solving to inductive theorem proving. Section 4 formalizes
our constraint solving method and proves its soundness and relative completeness. Section 5 reports on our prototype implementation based on the proposed
method and the results of preliminary experiments. We compare our methodwith related work in Section 6 and conclude the paper with some remarks on
future work in Section 7. The full version [58] contains omitted proofs, example
constraints generated from verification problems, and implementation details.

2

Overview of Induction-Based Horn Constraint Solving

In this section, we use the constraint set Hmult in Section 1 as a running example
to give an overview of our induction-based Horn constraint solving method (moreformal treatment is provided in Sections 3 and 4). Our method interprets thedefinite clauses of a given constraint set as derivation rules for atoms P (et),
namely, applications of a predicate variable P to a sequence et of terms t1 , . . . , tm .
For example, the definite clauses Dmult ⊆ Hmult are interpreted as the rules:|= y = 0 ∧ r = 0
P (x, y, r)

P (x, y − 1, r − x)
P (x, y, r)|= y 6= 0|= y = 0 ∧ r = a
Q(x, y, a, r)

Q(x, y − 1, a + x, r)Q(x, y, a, r)|= y 6= 0

4

Here, the heads of the clauses are changed into the uniform representations
P (x, y, r) and Q(x, y, a, r) of atoms over variables. These rules inductively define
the least interpretation ρmult for P and Q that satisfies the definite clauses Dmult .
We thus get ρmult = {P 7→ {(x, y, r) ∈ Z3 | x×y = r ∧y ≥ 0}, Q 7→ {(x, y, a, r) ∈Z4 | x × y + a = r ∧ y ≥ 0}}, and Hmult has a solution iff the goal clause∀x, y, r1 , a, r2 . (P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ∧ (r1 + a 6= r2 ) ⇒ ⊥)is valid under ρmult (see Section 3 for a correctness proof of the reduction). We
then check the validity of the goal by induction on the derivation of atoms.
Principle 1 (Induction on Derivations) Let P be a property on derivations
D of atoms. We then have ∀D.P(D) if and only if ∀D. ((∀D0 ≺ D.P(D0 )) ⇒ P(D)),
where D0 ≺ D represents that D0 is a strict sub-derivation of D.
Formally, we propose an inductive proof system for deriving judgments of theform D; Γ ; A; φ ` ⊥, where ⊥ represents the contradiction, φ represents a formula
without atoms, A represents a set of atoms, Γ represents a set of induction
hypotheses and user-specified lemmas, and D represents a set of definite clausesthat define the least interpretation of the predicate variables in Γ or A. Here,Γ , A, and φ are allowed to have common free term variables. The free term
variables of a clause in D have the scope within the clause, and are considered
to be universally
Intuitively, a judgment D; Γ ; A; φ ` ⊥ means that
V quantified.
Vthe formula Γ ∧ A ∧ φ ⇒ ⊥ is valid under the least interpretation induced
by D. For example, consider the following judgment Jmult :Jmult , Dmult ; ∅; {P (x, y, r1 ), Q(x, y, a, r2 )} ; (r1 + a 6= r2 ) ` ⊥If Jmult is derivable, P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ∧ (r1 + a 6= r2 ) ⇒ ⊥ is valid under
the least predicate interpretation by Dmult , and hence Hmult has a solution.
The inference rules for the judgment D; Γ ; A; φ ` ⊥ are shown in Section 4,
Figure 2. The rules there, however, are too general and formal for the purposeof providing an overview of the idea. Therefore, we defer a detailed explanationof the rules to Section 4, and here explain a simplified version shown below,
obtained from the complete version by eliding some conditions and subtleties
while retaining the essence. The rules are designed to exploit Γ andVD for iteratively updating the current knowledge represented by the formula A ∧ φ until
a contradiction is implied. The first rule Induct
P (et) ∈ A{ey } = fvs(A)xe : fresh
σ = {ey 7→ xe} V ∪ fvs(φ)ψ = ∀ex. P (σet) ≺ P (et) ∧ σA ⇒ ¬(σφ)
D; Γ ∪ {ψ} ; A; φ ` ⊥D; Γ ; A; φ ` ⊥selects an atom P (et) ∈ A and performs induction on the derivation of the atom
by adding a new V
induction hypothesis ψ to Γ , which is obtained from the current
proof obligation A ∧ φ ⇒ ⊥ by generalizing its free term variables (denoted byfvs(A) ∪ fvs(φ)) into fresh ones x
e using a map σ, and adding a guard P (σe
t) ≺
5

P (e
t), requiring the derivation of P (σet) to be a strict sub-derivation of that ofe
P (t), to avoid an unsound application of ψ. The second rule Unfold
P (et) ∈ A

D; Γ ; A ∪ [et/ex]A0 ; φ ∧ [et/ex]φ0 ` ⊥(for each (P (ex) ⇐ A0 ∧ φ0 ) ∈ D)
D; Γ ; A; φ ` ⊥selects an atom P (et) ∈ A, performs a case analysis on the last rule used to derive
the atom, which is represented by a definite clause in D. The third rule Apply⊥
∀e
x.



 V

P (te0 ) ≺ P (et ) ∧ A0 ⇒ φ 0 ∈ Γdom(σ) = {ex}P (σ te0 ) ≺ P (et)
VV|= A ∧ φ ⇒ σA0D; Γ ; A; φ ∧ σφ0 ` ⊥D; Γ ; A; φ ` ⊥selects an induction hypothesis in Γ , and tries to find an instantiation σ of thequantified variables xe such thatV
– the instantiatedpremise σA0 of the hypothesis is implied by the currentVknowledge A ∧ φ and– the derivation of the atom P (σ te0 ) ∈ σA0 to which the hypothesis is being
applied is a strict sub-derivation of that of the atom P (et) on which theinduction (that has introduced the hypothesis) has been performed.
If such a σ is found, σφ0 is added to the current knowledge. The fourth rule
Valid⊥ checks whether the current knowledge implies ⊥, and if so, closes theproof branch under consideration.
Figure 1 shows the structure (with side-conditions omitted) of a derivation of
the judgment Jmult , constructed by using the simplified version of the inference
rules. We below explain how the derivation is constructed. First, by performing
induction on the atom P (x, y, r1 ) in Jmult using the rule Induct, we obtain thesubgoal J0 , where the induction hypothesis ∀x0 , y 0 , r10 , a0 , r20 . φind is added. Wethen apply Unfold to perform a case analysis on the last rule used to derive
the atom P (x, y, r1 ), and obtain the two subgoals J1 and J2 . We here got two
subgoals because Dmult has two clauses with the head that matches with theatom P (x, y, r1 ). The two subgoals are then discharged as follows.
– Subgoal 1: By performing a case analysis on Q(x, y, a, r2 ) in J1 using therule Unfold, we further get two subgoals J3 and J4 . Both J3 and J4 arederived by the rule Valid⊥ because |= φ3 ⇒ ⊥ and |= φ4 ⇒ ⊥ hold.
– Subgoal 2: By performing a case analysis on Q(x, y, a, r2 ) in J2 using therule Unfold, we obtain two subgoals J5 and J6 . J5 is derived by the rule
Valid⊥ because |= φ5 ⇒ ⊥ holds. To derive J6 , we use the rule Apply⊥ toapply the induction hypothesis to the atom P (x, y − 1, r1 − x) ∈ A6 in J6 .
Note that this can be done by using the quantifier instantiation
σ = {x0 7→ x, y 0 7→ y − 1, r10 7→ r1 − x, a0 7→ a + x, r20 7→ r2 } ,6

J3(Valid⊥)J1(Valid⊥)J4(Unfold)

J5(Valid⊥)J7(Apply⊥)J6(Unfold)
J2(Unfold)(Valid⊥)J0(Induct)
Jmult

Here, Ji ’s are of the form Ji , Dmult ; {∀x0 , y 0 , r10 , a0 , r20 . φind } ; Ai ; φi ` ⊥ where:
φind = (P (x0 , y 0 , r10 ) ≺ P (x, y, r1 )) ∧ P (x0 , y 0 , r10 ) ∧ Q(x0 , y 0 , a0 , r20 ) ⇒ r10 + a0 = r20
φ0 = r1 + a 6= r2

φ6 = φ2 ∧ y 6= 0

φ1 = φ0 ∧ y = 0 ∧ r1 = 0

φ7 = φ6 ∧ σ(r10 + a0 = r20 )φ2 = φ0 ∧ y 6= 0

A0 = A1 = A3 = {P (x, y, r1 ), Q(x, y, a, r2 )}φ3 = φ1 ∧ y = 0 ∧ r2 = a

A2 = A5 = A0 ∪ {P (x, y − 1, r1 − x)}φ4 = φ1 ∧ y 6= 0

A4 = A1 ∪ {Q(x, y − 1, a + x, r2 )}φ5 = φ2 ∧ y = 0 ∧ r2 = a

A6 = A7 = A2 ∪ {Q(x, y − 1, a + x, r2 )}Fig. 1. The structure of an example derivation of Jmult .

because σ(P (x0 , y 0 , r10 )) = P (x, y − 1, r1 − x) ≺ P (x, y, r1 ) holds and thepremise σ(P (x0 , y 0 , r10 ) ∧ Q(x0 , y 0 , a0 , r20 )) = P (x, y − 1, r1 − x) ∧ Q(x, y − 1, a +x,
V r2 ) of the instantiated hypothesis is implied by the current knowledge
A6 ∧ r1 + a 6= r2 ∧ y 6= 0. We thus obtain the subgoal J7 , whose φ-partis equivalent to r1 + a 6= r2 ∧ y 6= 0 ∧ r1 + a = r2 . Because this implies acontradiction, J7 is finally derived by using the rule Valid⊥.
To automate proof search in the system, we use either an off-the-shelf SMT
solver or a PDR-based Horn constraint solver for checking whether the current
knowledge implies a contradiction (in the rule Valid⊥). An SMT solver is also
used to check whether each element of Γ can be used to update the current
knowledge, by finding a quantifier instantiation σ (in the rule Apply⊥). The
use of an SMT solver provides our method with efficient and powerful reasoning
about data structures, including integers, real numbers, arrays, algebraic datatypes, and uninterpreted functions. However, there still remain two challenges
to be addressed towards full automation:
1. Challenge: How to check (in the rule Apply⊥) the strict sub-derivation
relation P (et0 ) ≺ P (et) between the derivation of an atom P (et0 ) to which an
induction hypothesis in Γ is being applied, and the derivation of the atomP (et) on which the induction has been performed? Recall that in the above
derivation of Jmult , we needed to check P (x, y −1, r1 −x) ≺ P (x, y, r1 ) before
applying the rule Apply⊥ to J6 .
Our solution: The formalized rules presented in Section 4 keep sufficient
information for checking the strict sub-derivation relation: we associate eachinduction hypothesis in Γ with an induction identifier α, and each atom in
7A with a set M of identifiers indicating which hypotheses can be applied tothe atom. Further details are explained in Section 4.
2. Challenge: In which order should the rules be applied?
Our solution: We here adopt the following simple strategy, and evaluate it
by experiments in Section 5.
– Repeatedly apply the rule Apply⊥ if possible, until no new knowledge
is obtained. (Even if the rule does not apply, applications of Induct andUnfold explained in the following items may make Apply⊥ applicable.)– If the knowledge cannot be updated by Apply⊥, select some atom fromA in a breadth-first manner, and apply the rule Induct to the atom.
– Apply the rule Unfold whenever Induct is applied.
– Try to apply the rule Valid⊥ whenever the knowledge is updated.

3

Horn Constraint Solving Problems

This section formalizes Horn constraint solving problems and proves the correctness of our reduction from constraint solving to inductive theorem proving. We
here restrict ourselves to constraint Horn clauses over the theory TZ of quantifierfree linear integer arithmetic for simplicity, although our induction-based Hornconstraint solving method formalized in Section 4 supports constraints over any
background theories supported by the underlying SMT solver. A TZ -formula φ isa Boolean combination of atomic formulas t1 ≤ t2 , t1 < t2 , t1 = t2 , and t1 6= t2 .
We write > and ⊥ respectively for tautology and contradiction. A TZ -term t iseither a term variable x, an integer constant n, or t1 + t2 .
3.1

Notation for HCSs

A Horn Constraint Set (HCS) H is a finite set {hc 1 , . . . , hc m } of Horn clauses.
A Horn clause hc is defined to be h ⇐ b, consisting of a head h and a body b.
A head h is either of the form P (et) or ⊥, and a body b is of the form P1 (et1 ) ∧· · · ∧ Pm (etm ) ∧ φ. Here, P is a meta-variable ranging over predicate variables.
We write ar (P ) for the arity of P . We often abbreviate a Horn clause h ⇐> as h. We write pvs(hc)S for the set of the predicate variables that occur in
hc and define pvs(H) = hc∈H pvs(hc). Similarly, we
S write fvs(hc) for the setof the term variables in hc and define fvs(H) = hc∈H fvs(hc). We assume
that for any hc 1 , hc 2 ∈ H, hc 1 6= hc 2 implies fvs(hc 1 ) ∩ fvs(hc 2 ) = ∅. Weewrite HP for the
Wm set of Horn clauses in H of the form P (t) ⇐ b. We defineH(P ) = λex.∃ey . i=1 (bi ∧ xe=eti ) if HP = P (eti ) ⇐ bi i∈{1,...,m} where {ey} =fvs(HP ) andV{ex}∩{ey } = ∅. By using H(P ), an HCS H is logically interpreted as
the formula P ∈pvs(H) ∀e
xP . (H(P )(exP ) ⇒ P (exP )), where x
eP = x1 , . . . , xar (P ) .
A Horn clause with the head of the form P (et) (resp. ⊥) is called a definite
clause (resp. a goal clause). We write def (H) (resp. goal (H)) for the subset of
H consisting of only the definite (resp. goal) clauses. Note that H = def (H) ∪goal (H) and def (H) ∩ goal (H) = ∅.
8

3.2

Predicate Interpretation

A predicate interpretation ρ for an HCS H is a map from each predicate variableP ∈ pvs(H) to a subset of Zar (P ) . We write the domain of ρ as dom(ρ). We writeρ1 ⊆ ρ2 if ρ1 (P ) ⊆ ρ2 (P ) for all P ∈ pvs(H). We call an interpretation ρ a solution of H and write ρ |= H if ρ |= hc holds
For example, ρ0mult = for all hc ∈ H.
34
{P 7→ (x, y, r) ∈ Z | x × y = r , Q 7→ (x, y, a, r) ∈ Z | x × y + a = r } is asolution of the HCS Hmult in Section 1.
Definition 1 (Horn Constraint Solving Problems). A Horn constraint
solving problem is the problem of checking if a given HCS H has a solution.
We now establish the reduction from Horn constraint solving to inductive theorem proving, which is the foundation of our induction-based Horn constraint
solving method. The definite clauses def (H) are considered to inductively define the least predicate interpretation for H as the least fixed-point µFH of thefollowing function on predicate interpretations.
nnooFH (ρ) = P 7→ (ex) ∈ Zar (P ) ρ |= H(P )(ex)
P ∈ dom(ρ)
Because FH is continuous [35], the Sleast fixed-point µFH of FH exists. Furtheriimore, we can express it as µFH = i∈N FH({P 7→ ∅ | P ∈ pvs(H)}), where FH
means i-times application of FH . It immediately follows that the least predicate
interpretation µFH is a solution of def (H) because any fixed-point of FH is asolution of def (H). Furthermore, µFH is the least solution. Formally, we canprove the following proposition.
Proposition 1. µFH |= def (H) holds, and for all ρ such that ρ |= def (H),µFH ⊆ ρ holds.
On the other hand, the goal clauses goal (H) are considered as specifications of
the least predicate interpretation µFH . As a corollary of Proposition 1, it follows
that H has a solution if and only if µFH satisfies the specifications goal (H).
Corollary 1. ρ |= H for some ρ if and only if µFH |= goal (H)In Section 4, we present an induction-based method for proving µFH |= goal (H).

4

Induction-based Horn Constraint Solving Method

As explained in Section 2, our method is based on the reduction from Horn constraint solving into inductive theorem proving. The remaining task is to develop
an automated method for proving the inductive conjectures obtained from Hornconstraints. We thus formalize our inductive proof system tailored to Horn constraint solving and proves its soundness and relative completeness. To automate
proof search in the system, we adopt the rule application strategy in Section 2.
We formalize a general and more elaborate version of the inductive proof
system explained in Section 2. A judgment of the extended system is of the form
9ePerform induction on the derivation of the atom
 P (t):M e
0P◦ (t) ∈ AΓ = Γ ∪ (α . P (et), A, φ, h)D; Γ 0 ; (A \ P◦M (et)) ∪ PαM (et) ; φ ` h(α : fresh)
D; Γ ; A; φ ` hCase-analyze the last rule used (where m rules are possible):VW
ei . (φi ∧ Ai )PαM (et) ∈ A
D(P )(et) = mi=1 ∃xM ∪{α}
D; Γ ; A ∪ Ai ◦; φ ∧ φi ` h(for each i ∈ {1, . . . , m})
D; Γ ; A; φ ` hApply an induction hypothesis or a user-specified lemma in Γ :(g, A0 , φ0 , ⊥) ∈ Γdom(σ) = fvs(A0 )|= φ ⇒ Jσg∈AK|= φ ⇒ JσA0 ⊆AK0{ex} = fvs(φ ) \ dom(σ)
D; Γ ; A; φ ∧ ∀ex.¬(σφ0 ) ` h
D; Γ ; A; φ ` hApply an induction hypothesis or a user-specified lemma in Γ :(g, A0 , φ0 , P (et)) ∈ Γdom(σ) = fvs(A0 ) ∪ fvs(et)|= φ ⇒ Jσg∈AK|= φ ⇒ ∃ex.(σφ0 ) n |= φ ⇒oJσA0 ⊆AK{ex} = fvs(φ0 ) \ dom(σ)
D; Γ ; A ∪ P◦∅ (σet) ; φ ` hD; Γ ; A; φ ` hApply a definite clause in D: V
(P (et) ⇐ φ0 ∧ A0 ) ∈ D|= φ ⇒ ∃ex.(σφ0 ){ex} = fvs(φ0 ) \ dom(σ)

dom(σ) = fvs(A0 ) ∪ fvs(et)
0|= φ ⇒ JσAn ⊆AKoD; Γ ; A ∪ P◦∅ (σet) ; φ ` hD; Γ ; A; φ ` h(Induct)(Unfold)(Apply⊥)(ApplyP )(Fold)

Check if the current knowledge entails the asserted proposition:qyVVµFD |= A ∧ φ ⇒ ⊥µFD |= A ∧ φ ⇒ P (et)∈A
(Valid⊥)(ValidP )D; Γ ; A; φ ` ⊥D; Γ ; A; φ ` P (et)
Auxiliary functions:
_
q
y
P (e
t)∈A ,et=et0

JA1 ⊆A2 K ,P (te0 )∈A

J•∈AK , >

q

^

q

P (e
t)∈A2

y

P (te)∈A1nozy r
α . P (et)∈A , P (et)∈ P M (te0 ) ∈ A | α ∈ M

Fig. 2. The inference rules for the judgment D; Γ ; A; φ ` h.

D; Γ ; A; φ ` h, where D is a set of definite clauses and φ represents a formula
without atoms. We here assume that D(P ) is defined similarly as H(P ). The asserted proposition h on the right is now allowed to be an atom P (et) instead of ⊥.
For deriving such judgments, we will introduce new rules Fold and ValidP laterin this section. Γ represents a set {(g1 , A1 , φ1 , h1 ), . . . , (gm , Am , φm , hm )} con10

sisting of user-specified lemmas and induction hypotheses, where giVis either • or
α . P (et). (•, A, φ, h) ∈ Γ represents the user-specified lemma ∀ex. ( A ∧ φ ⇒ h)ewhere {ex} = fvs(A, φ, h), while
(α
.
P
(
t
),
A,
φ,
h)
∈
Γ
represents
the induction
 V
hypothesis ∀ex. P (et) ≺ P (et0 ) ∧ A ∧ φ ⇒ h with {ex} = fvs(P (et), A, φ, h) thathas been introduced by induction on the derivation of the atom P (et0 ). Here, α
represents the induction identifier assigned to the application of induction that
has introduced the hypothesis. Note that h on the right-hand side of ⇒ is now
allowed to be an atom of the form Q(et). We will introduce a new rule ApplyP
later in this section for using such lemmas
hypotheses to obtain new knowl andMm
1 eedge. A is also extended to be a set P1 M(ttm ) of annotated1 ), . . . , Pm αm (eα1M eatoms. Each element Pα (t) has two annotations:– an induction identifier α indicating that the induction with the identifier α
is performed on the atom by the rule Induct. If the rule Induct has neverbeen applied to the atom, α is set to be a special identifier denoted by ◦.
– a set of induction identifiers M indicating that if α0 ∈ M , the derivation
D of the atom PαM (et) satisfies D ≺ D0 for the derivation D0 of the atom0P (et ) on which the induction with the identifier α0 is performed. Thus, an
induction hypothesis (α0 . P (et0 ), A0 , φ0 , h0 ) ∈ Γ can be applied to the atom0M ePα (t) ∈ A only if α ∈ M holds.
t)Note that we use these annotations only for guiding inductive proofs and PαM (eis logically equivalent to P (et). We often omit these annotations when they areclear from the context.
Given a Horn constraint solving problem H, our method reduces the problem
into an inductive
theorem proving problem as follows. For each goal clause inVmgoal (H) = { Ai ∧ φi ⇒ ⊥}i=1 , we check the judgment def (H); ∅; Ai ∅◦ ; φi ` ⊥is derivable by the inductive proof system. Here, each atom in Ai is initiallyannotated with ∅ and ◦.
The inference rules for the judgment D; Γ ; A; φ ` h are defined in Figure 2.
t) ∈ A and performs induction on the
The rule Induct selects an atom P◦M (ederivation of the atom. This rule generates a fresh induction identifier α 6= ◦,adds a new induction hypothesis (α . P (et), A, φ, h) to Γ , and replaces the atomP◦M (et) with the annotated one PαM (et) for remembering that the induction witht) ∈ Athe identifier α is performed on it. The rule Unfold selects V
an atom PαM (eand performs a case analysis on the last rule P (et) ⇐ φi ∧ Ai used to derive
the atom. As the result, the goal is broken into m-subgoals if there are m rules∪{α}possibly used to derive the atom. The rule adds Ai M
and φi respectively◦M
to A and φ in the i-th subgoal, where Aα represents PαM (et) P (et) ∈ A . Notehere that each atom in Ai is annotated with M ∪ {α} because the derivationof the atom Ai is a strict sub-derivation of that of the atom PαM (et) on which
the induction with the identifier α has been performed. If α = ◦, it is the casethat the rule Induct has never been applied to the atom PαM (et) yet. The rules
Apply⊥ and ApplyP select (g, A0 , φ0 , h) ∈ Γ , which represents a user-specified
lemma if g = • and an induction hypothesis otherwise, and try to add new
knowledge respectively to the φ- and the A-part of the current knowledge: the11rules try to find an instantiation σ for the free term variables in (g, A0 , φ0 , h),which are considered to be universally quantified, and then use σ(g, A0 , φ0 , h)to obtain new knowledge. Contrary to Vthe rule Unfold, the rule Fold tries
to use a definite clause P (et) ⇐ φ0 ∧ A0 ∈ D
V from the body to the headdirection: Fold tries to find σ such that σ(φ0 ∧ A0 ) is implied by the current
knowledge, and updates it with P (σet). This rule is useful when we check thecorrectness Vof user specified lemmas. The rule Valid⊥ checks if the current
knowledge A ∧ φ implies a contradiction, while the rule ValidP checks if theasserted proposition P (et) on the right-hand side of the judgment is implied by
the current knowledge. Here, we can use either an SMT solver or a (PDR-based)
Horn constraint solver.
The former is much faster because
the validity checking
VV
problem µFD |= A ∧ φ ⇒ ψ is approximated to |= φ V⇒ ψ. By contrast, thelatter is much more precise because
V we reduce µFD |= A ∧ φ ⇒ ψ to Hornconstraint solving of D ∪ {⊥ ⇐ A ∧ φ ∧ ¬ψ}. The soundness of the inductive
proof system is shown as follows.
Lemma 1 (Soundness). If D; Γ ; A; φ ` h is derivable, then there is k such thatk V
kµFD |= JΓ, AK ∧ A ∧ φ ⇒ h holds. Here, JΓ, AK represents the conjunction ofuser-specified lemmas and induction hypotheses in Γ instantiated for the atoms
occurring in the k-times unfolding of A.
The correctness of our Horn constraint solving method follows immediatelyfrom Lemma 1 and Corollary 1 as follows.
Vm
Theorem 1. Suppose that H is an HCS with goal (H) = { Ai ∧ φi ⇒ ⊥}i=1
and def (H); ∅; Ai ; φi ` ⊥ for all i = 1, . . . , m. It then follows ρ |= H for some ρ.
VkProof. By Lemma
1 and the fact that µFdef (H) |=Ai ⇒ J∅, Ai K , we getVµFdef (H) |= Ai ∧ φi ⇒ ⊥. We therefore have µFdef (H) |= goal (H). It thenfollows that ρ |= H for some ρ by Corollary 1.
We can also prove the following relative completeness of our system withrespect to ordinary Horn constraint solving schemes that find solutions explicitly.
Lemma 2 (Relative Completeness).
Suppose that ρ is a solution of a givenV
HCS H with goal (H) = {⊥ ⇐ A ∧ φ}. Let Γ = {φP | P ∈ dom(ρ)} where
φP = (∀ex. P (ex) ⇒ ρ(P )(ex)). Then, def (H); Γ ; A; φ ` ⊥ and def (H); Γ \{φP } ; P (ex); ¬ρ(P )(ex) ` ⊥ hold for all P ∈ dom(ρ).
Note that our method can exploit over-approximations of the predicates computed by an existing Horn constraint solver as lemmas for checking the validityof the goal clauses, even if the existing solver failed to find a complete solution.

5

Implementation and Preliminary Experiments

We have implemented a Horn constraint solver based on the proposed method
and integrated it, as a backend solver, with a refinement type-based verification
tool RCaml [54, 55, 57] for the OCaml functional language. Our solver generates
12

a proof tree like the one shown in Figure 1 as a certificate if the given constraint
set is judged to have a solution, and a counterexample if the constraint set isjudged unsolvable. We adopted Z3 [22] and its PDR engine [32] respectively as
the underlying SMT and Horn constraint solvers of the inductive proof system.
In addition, our solver is extended to generate conjectures on the determinacyof the predicates, which are then checked and used as lemmas. This extension isparticularly useful for verification of deterministic functions. The details of theimplementation are explained in the full version [58]. The web interface to theverification tool as well as all the benchmark programs used in the experiments
reported below are available from http://www.cs.tsukuba.ac.jp/~uhiro/.
We have tested our tool on two benchmark sets. The first set is obtained fromthe test suite for automated induction provided by the authors of the IsaPlannersystem [23]. The benchmark set consists of 85 (mostly) relational verification
problems of pure mathematical functions on algebraic data types (ADTs) such as
natural numbers, lists, and binary trees. Most of the problems cannot be verified
by using the previous Horn constraint solvers [27, 29, 33, 41, 48, 52, 55, 57] because
they support neither relational verification nor ADTs. The benchmark set has
also been used to evaluate the automated inductive theorem provers [18, 40, 46,49]. The experiment results on this benchmark set are reported in Section 5.1.
To demonstrate advantages of our novel combination of Horn constraint solving with inductive theorem proving, we have prepared the second benchmark set
consisting of 30 assertion safety verification problems of (mostly relational) specifications of OCaml programs that use various advanced language features suchas partial (i.e., possibly non-terminating) functions, higher-order functions, exceptions, non-determinism, ADTs, and non-inductively defined data types (e.g.,real numbers). The benchmark set also includes integer functions with complex
recursion and a verification problem concerning the equivalence of programs
written in different language paradigms. All the verification problems except 4
are relational ones where safe inductive invariants are not expressible in QF LIA,
and therefore not solvable by the previous Horn constraint solvers. These verification problems are naturally and automatically axiomatized by our method
using predicates defined by Horn constraints as the least interpretation. By contrast, these problems cannot be straightforwardly axiomatized by the previous
automated inductive theorem provers based on logics of pure total functions on
ADTs. The experiment results on this benchmark set are reported in Section 5.2.
5.1

Experiments on IsaPlanner benchmark set

We manually translated the IsaPlanner benchmarks into assertion safety verification problems of OCaml programs, where we encoded natural numbers using
integer primitives, and defined lists and binary trees as ADTs in OCaml. RCaml
reduced the verification problems into Horn constraint solving problems using
the constraint generation method proposed in [55]. Our solver then automaticallysolved 68 out of 85 verification problems without using lemmas, and 73 problems
with the extension for conjecturing the determinacy of predicates enabled. We
have manually analyzed the experiment results and found that 9 out of 12 failed
13

problems require lemmas. The other 3 problems caused timeout of Z3. It was
because the rule application strategy implemented in our solver caused uselessdetours in proofs and put heavier burden on Z3 than necessary.
The experiment results on the IsaPlanner benchmark set show that our Hornclause-based axiomatization of total recursive functions does not have significant
negative impact on the automation of induction; According to the comparisonin [49] of state-of-the-art automated inductive theorem provers, which are basedon logics of pure total functions over ADTs, IsaPlanner [23] proved 47 out of
the 85 IsaPlanner benchmarks, Dafny [40] proved 45, ACL2s [15] proved 74, andZeno [49] proved 82. The HipSpec [18] inductive prover and the SMT solver
CVC4 extended with induction [46] are reported to have proved 80. In contrast
to our Horn-clause-based method, these inductive theorem provers can be, and infact are directly applied to prove the conjectures in the benchmark set, because
the benchmark set contains only pure total functions over ADTs.
It is also worth noting that, all the inductive provers that achieved better
results than ours support automatic lemma discovery (beyond the determinacy),in a stark contrast to our solver. For example, the above result (80 out of 85)
of CVC4 is obtained when they enable an automatic lemma discovery techniqueproposed in [46] and use a different encoding (called dti in [46]) of natural
numbers than ours. When they disable the technique and use a similar encoding
to ours (called dtt in [46]), CVC4 is reported to have proved 64. Thus, we
believe that extending our method with automatic lemma discovery, which has
been comprehensively studied by the automated induction community [15, 18,34, 37, 46, 49], further makes induction-based Horn constraint solving powerful.
5.2

Experiments on benchmark set that uses advanced features

Table 1 summarizes the experiment results on the benchmark set. The column“specification” shows the verified specification and the column “kind” shows its
kind, where “equiv”, “assoc”, “comm”, “dist”, “mono”, “idem”, “nonint”, and“nonrel” respectively represent the equivalence, associativity, commutativity,
distributivity, monotonicity, idempotency, non-interference, and non-relational.
The column “features” shows the language features used in the verification problem, where each character has the following meaning: H: higher-order functions,
E: exceptions, P: partial (i.e., possibly non-terminating) functions, D: demonic
non-determinism, R: real functions, I: integer functions with complex recursion, N: nonlinear functions, C: procedures written in different programming
paradigms. The column “result” represents whether our tool succeeded 3or failed
7. The column “time” represents the elapsed time for verification in seconds.
Our tool successfully solved 28 out of 30 problems. Overall, the results showthat our tool can solve relational verification problems that use various advanced
language features, in a practical time with surprisingly few user-specified lemmas. We also want to emphasize that the problem ID5, which required a lemma,
is a relational verification problem involving two function calls with significantly
different control flows: one recurses on x and the other on y. Thus, the result
demonstrates an advantage of our induction-based method that it can exploit
14

Table 1. Experiment results on programs that use various language features
ID specification
kind features result time (sec.)
1 mult x y + a = mult acc x y a
equiv
P
3
0.378
2 mult x y = mult acc x y 0
equiv
P
3†
0.803
3 mult (1 + x) y = y + mult x y
equiv
P
3
0.403
4 y ≥ 0 ⇒ mult x (1 + y) = x + mult x y
equiv
P
3
0.426
5 mult x y = mult y x
comm
P
3‡
0.389
6 mult (x + y) z = mult x z + mult y z
dist
P
3
1.964
7 mult x (y + z) = mult x y + mult x z
dist
P
3
4.360
8 mult (mult x y) z = mult x (mult y z)
assoc
P
7
n/a
9 0 ≤ x1 ≤ x2 ∧ 0 ≤ y1 ≤ y2 ⇒ mult x1 y1 ≤ mult x2 y2
mono
P
3
0.416
10 sum x + a = sum acc x a
equiv
3
0.576
11 sum x = x + sum (x − 1)
equiv
3
0.452
12 x ≤ y ⇒ sum x ≤ sum y
mono
3
0.593
13 x ≥ 0 ⇒ sum x = sum down 0 x
equiv
P
3
0.444
14 x < 0 ⇒ sum x = sum up x 0
equiv
P
3
0.530
15 sum down x y = sum up x y
equiv
P
7
n/a
16 sum x = apply sum x
equiv
H
3
0.430
17 mult x y = apply2 mult x y
equiv
H, P
3
0.416
18 repeat x (add x) a y = a + mult x y
equiv
H, P
3
0.455
19 x ≤ 101 ⇒ mc91 x = 91
nonrelI
30.233
20 x ≥ 0 ∧ y ≥ 0 ⇒ ack x y > ynonrelI
3
0.316
21 x ≥ 0 ⇒ 2 × sum x = x × (x + 1)
nonrelN
30.275
22 dyn sys 0. −→/ ∗ assert false
nonrel R,N3
0.189
23 flip mod y x = flip mod y (flip mod y x)
idem
P3
13.29024 noninter h1 l1 l2 l3 = noninter h2 l1 l2 l3
nonintP
3
1.203
25 try find opt p l = Some (find p l) with
Not Found → find opt p l = None
equiv
H, E
3
1.065
26 try mem (find ((=) x) l) l with Not Found → ¬(mem x l) equiv
H, E
3
1.056
27 sum list l = fold left (+) 0 l
equiv
H
3
6.148
28 sum list l = fold right (+) l 0
equiv
H
3
0.508
29 sum fun randpos n > 0
equiv
H,D
3
0.319
30 mult x y = mult Ccode(x, y)
equiv
P, C
3
0.303
†
‡

A lemma Pmult acc (x, y, a, r) ⇒ Pmult acc (x, y, a − x, r − x) is used
A lemma Pmult (x, y, r) ⇒ Pmult (x − 1, y, r − y) is used
Used a machine with Intel(R) Xeon(R) CPU (2.50 GHz, 16 GB of memory).

lemmas to fill the gap between function calls with different control flows. Another interesting result we obtain is that the distributivity ID7 of mult is solved
thanks to our combination of inductive theorem proving and PDR-based Hornconstraint solving, and just using either of them failed.
Our tool, however, failed to verify the associativity ID8 of mult and the equivalence ID15 of sum down and sum up. ID8 requires two lemmas Pmult (x, y, r) ⇒Pmult (y, x, r), which represents the commutativity of mult, and Pmult (x+y, z, r) ⇒∃s1 , s2 .(Pmult (x, z, s1 )∧Pmult (y, z, s2 )∧r = s1 +s2 ). The latter lemma, however, is
not of the form currently supported by our proof system. In ID15, the functions
sum down and sum up use different recursion parameters (resp. y and x), andrequires Psum down (x, y, s) ∧ a < x ⇒ ∃s1 , s2 .(Psum down (a, y, s1 ) ∧ Psum down (a, x −15

1, s2 ) ∧ s = s1 − s2 ) and Psum up (x, y, s) ∧ a < x ⇒ ∃s1 , s2 .(Psum down (a, y, s1 ) ∧Psum down (a, x − 1, s2 ) ∧ s = s1 − s2 ). These lemmas are provable by induction on
the derivation of Psum down (x, y, s) and Psum up (x, y, s), respectively. However, as
in the case of ID8, our system does not support the form of the lemmas. Future
work thus includes an extension to more general form of lemmas and judgments.

6

Related Work

Automated inductive theorem proving techniques and tools have long been studied, for example and to name a few: the Boyer-Moore theorem provers [37]ACL2s [15], rewriting induction provers [45] SPIKE [9], proof planners CLAM [14,34] and IsaPlanner [23], and SMT-based induction provers Leon [50], Dafny [40],Zeno [49], HipSpec [18], and CVC4 extended with induction [46]. These automated provers are mostly based on logics of pure total functions over inductive
data types. Consequently, users of these provers are required to axiomatize advanced language features and specifications using pure total functions as necessary. The axiomatization process, however, is non-trivial, error-prone, and possibly causes a negative effect on the automation of induction. For example, if apartial function (e.g., f (x) = f (x) + 1) is input, Zeno goes into an infinite loop
and CVC4 is unsound (unless control literals proposed in [50] are used in the axiomatization). We have also confirmed that CVC4 failed to verify complex integerfunctions like the McCarthy 91 and the Ackermann functions (resp. ID19 andID20 in Table 1). By contrast, our method supports advanced language featuresand specifications via Horn-clause encoding of their semantics based on programlogics. Compared to cyclic proofs [11] and widely-supported structural induction
on derivation trees, our proof system uses induction explicitly by maintaining a
set of induction hypotheses and annotating atoms with induction identifiers sothat we can apply the hypotheses soundly. This enables our system to introduce
multiple induction hypotheses within a single proof path from dynamically generated formulas. Another advantage is the support of user-supplied lemmas, which
are useful in relational verification involving function calls with different control
flows (e.g., ID5). To address entailment checking problems in separation logic,
researchers have recently proposed induction-based methods [12, 13, 16, 39, 51] togo beyond the popular unfold-and-match paradigm (see e.g. [44]). It seems fruitful to incorporate their techniques into our approach to Horn constraint solving
to enable verification of heap-manipulating higher-order functional programs.
To aid verification of relational specifications of functional programs, Giesl [25]proposed context-moving transformations and Asada et al. [2] proposed a kindof tupling transformation. SymDiff [38] is a transformation-based tool built
on top of Boogie [3] for equivalence verification of imperative programs. Selfcomposition [5] is a program transformation technique to reduce k-safety [19,53] verification into ordinary safety verification, and has been applied to noninterference [4, 5, 53, 56] and regression verification [24] of imperative programs.
These transformations are useful for some patterns of relational verification problems, which are, however, less flexible in some cases than our approach based on16

a more general principle of induction. For example, Asada et al.’s transformation
enables verification of the functional equivalence of recursive functions with thesame recursion pattern (e.g., ID1), but does not help verification of the commutativity of mult (ID5). Because most of the transformations are designed for aparticular target language, they cannot be applied to aid relational verification
across programs written in different paradigms (e.g., ID30). Concurrently to ourwork, De Angelis et al. [1] recently proposed a predicate pairing transformation in the setting of Horn constraints for relational verification of imperative
programs. We tested our tool with some of their benchmark constraint solving
problems. There were some problems our tool successfully solved but their tool
VeriMAP failed, and vice versa: only our tool solved “barthe2” in MON category (if its goal clause is generalized) and “product” in INJ category. We also
confirmed that VeriMAP failed to solve our benchmark ID5 involving function
calls with different control flows. On the contrary, VeriMAP solved ID15.
There have also been proposed program logics that allow precise relationalverification [6, 7, 17, 26]. In particular, the relational refinement type system proposed in [6] can be applied to differential privacy and other relational security
verification problems of higher-order functional programs. This approach, however, is not automated.

7

Conclusion and Future Work

We have proposed a novel Horn constraint solving method based on an inductive
proof system and a PDR and SMT-based technique to automate proof searchin the system. We have shown that our method can solve Horn clause constraints obtained from relational verification problems that were not possible
with the previous methods based on Craig interpolation, abstract interpretation, and PDR. Furthermore, our novel combination of Horn clause constraints
with inductive theorem proving enabled our method to automatically axiomatize and verify relational specifications of programs that use various advanced
language features.
As a future work, we are planning to extend our inductive proof system tosupport more general form of lemmas and judgments. We are also planning toextend our proof search method to support automatic lemma discovery as in
the state-of-the-art inductive theorem provers [15, 18, 46, 49]. To aid users tobetter understand verification results of our method, it is important to generate
a symbolic representation of a solution of the original Horn constraint set fromthe found inductive proof. It is however often the case that a solution of Hornconstraint sets that require relational analysis (e.g., Hmult ) is not expressible
by a formula of the underlying logic. It therefore seems fruitful to generate asymbolic representation of mutual summaries in the sense of [31] across multiple
predicates (e.g., P, Q of Hmult ).
17

Acknowledgments We would like to thank Tachio Terauchi for useful discussions, and anonymous referees for their constructive comments. This work waspartially supported by Kakenhi 16H05856 and 15H05706.

References
1. E. D. Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Relational verification
through horn clause transformation. In SAS ’16, pages 147–169. Springer, 2016.
2. K. Asada, R. Sato, and N. Kobayashi. Verifying relational properties of functional
programs by first-order refinement. In PEPM ’15, pages 61–72. ACM, 2015.
3. M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie:
A modular reusable verifier for object-oriented programs. In FMCO ’05, pages
364–387. Springer, 2006.
4. G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using productprograms. In FM ’11, pages 200–214. Springer, 2011.
5. G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by selfcomposition. In CSFW ’04, pages 100–114. IEEE, 2004.
6. G. Barthe, M. Gaboardi, E. Gallego Arias, J. Hsu, A. Roth, and P.-Y. Strub.
Higher-order approximate relational refinement types for mechanism design anddifferential privacy. In POPL ’15, pages 55–68. ACM, 2015.
7. G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin. Probabilistic relational
reasoning for differential privacy. In POPL ’12, pages 97–110. ACM, 2012.
8. F. Bobot, J.-C. Filliâtre, C. Marché, and A. Paskevich. Why3: Shepherd your herdof provers. In Boogie ’11, pages 53–64, 2011.
9. A. Bouhoula, E. Kounalis, and M. Rusinowitch. SPIKE, an automatic theorem
prover. In LPAR ’92, volume 624 of LNCS, pages 460–462. Springer, 1992.
10. A. R. Bradley. SAT-based model checking without unrolling. In VMCAI ’11,
volume 6538 of LNCS, pages 70–87. Springer, 2011.
11. J. Brotherston. Cyclic proofs for first-order logic with inductive definitions. In
TABLEAUX ’05, volume 3702 of LNCS, pages 78–92. Springer, 2005.
12. J. Brotherston, D. Distefano, and R. L. Petersen. Automated cyclic entailment
proofs in separation logic. In CADE-23, pages 131–146. Springer, 2011.
13. J. Brotherston, C. Fuhs, J. A. P. Navarro, and N. Gorogiannis. A decision procedure
for satisfiability in separation logic with inductive predicates. In CSL-LICS ’14,
pages 25:1–25:10. ACM, 2014.
14. A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In
CADE-10, pages 647–648. Springer, 1990.
15. H. R. Chamarthi, P. Dillinger, P. Manolios, and D. Vroon. The ACL2 sedan
theorem proving system. In TACAS ’11, volume 6605 of LNCS, pages 291–295.
Springer, 2011.
16. D.-H. Chu, J. Jaffar, and M.-T. Trinh. Automatic induction proofs of datastructures in imperative programs. In PLDI ’15, pages 457–466. ACM, 2015.
17. Ş. Ciobâcă, D. Lucanu, V. Rusu, and G. Roşu. A language-independent proof
system for mutual program equivalence. In ICFEM ’14, pages 75–90. Springer,
2014.
18. K. Claessen, M. Johansson, D. Rosén, and N. Smallbone. Automating inductive
proofs using theory exploration. In CADE-24, volume 7898 of LNCS, pages 392–
406. Springer, 2013.

18

19. M. R. Clarkson and F. B. Schneider. Hyperproperties. In CSF ’08, pages 51–65.
IEEE, 2008.
20. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static
analysis of programs by construction or approximation of fixpoints. In POPL ’77,
pages 238–252. ACM, 1977.
21. W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory
and proof theory. Journal of Symbolic Logic, 22:269–285, 1957.
22. L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS ’08, volume4963 of LNCS, pages 337–340. Springer, 2008.
23. L. Dixon and J. D. Fleuriot. IsaPlanner: A prototype proof planner in Isabelle. In
CADE-19, volume 2741 of LNCS, pages 279–283. Springer, 2003.
24. D. Felsing, S. Grebing, V. Klebanov, P. Rümmer, and M. Ulbrich. Automating
regression verification. In ASE ’14, pages 349–360. ACM, 2014.
25. J. Giesl. Context-moving transformations for function verification. In LOPSTR’00, volume 1817 of LNCS, pages 293–312. Springer, 2000.
26. B. Godlin and O. Strichman. Regression verification: proving the equivalence ofsimilar programs. Software Testing, Verification and Reliability, 23(3):241–258,
2013.
27. S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing
software verifiers from proof rules. In PLDI ’12, pages 405–416. ACM, 2012.
28. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement
for verifying multi-threaded programs. In POPL ’11, pages 331–344. ACM, 2011.
29. A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses over
LI+UIF. In APLAS ’11, volume 7078 of LNCS, pages 188–203. Springer, 2011.
30. A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas. The SeaHorn verification
framework. In CAV ’15, pages 343–361. Springer, 2015.
31. C. Hawblitzel, M. Kawaguchi, S. K. Lahiri, and H. Rebêlo. Towards modularlycomparing programs using automated theorem provers. In CADE-24, pages 282–
299. Springer, 2013.
32. K. Hoder and N. Bjørner. Generalized property directed reachability. In SAT ’12,
pages 157–171. Springer, 2012.
33. K. Hoder, N. Bjørner, and L. de Moura. µZ: An efficient engine for fixed points
with constraints. In CAV ’11, volume 6806 of LNCS, pages 457–462. Springer,
2011.
34. A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal ofAutomated Reasoning, 16(1-2):79–111, 1996.
35. J. Jaffar and M. J. Maher. Constraint logic programming: a survey. The Journalof Logic Programming, 19:503 – 581, 1994.
36. T. Kahsai, P. Rümmer, H. Sanchez, and M. Schäf. JayHorn: A framework forverifying Java programs. In CAV ’16, volume 9779, pages 352–358. Springer, 2016.
37. M. Kaufmann, J. S. Moore, and P. Manolios. Computer-Aided Reasoning: An
Approach. Kluwer Academic Publishers, 2000.
38. S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebêlo. SYMDIFF: A languageagnostic semantic diff tool for imperative programs. In CAV ’12, pages 712–717.
Springer, 2012.
39. Q. L. Le, J. Sun, and W.-N. Chin. Satisfiability modulo heap-based programs. In
CAV ’16, volume 9779, pages 382–404. Springer, 2016.
40. K. R. M. Leino. Automating induction with an SMT solver. In VMCAI ’12, volume7148 of LNCS, pages 315–331. Springer, 2012.
41. K. McMillan and A. Rybalchenko. Computing relational fixed points using interpolation. Technical Report MSR-TR-2013-6, Microsoft Research, 2013.

19

42. K. L. McMillan. An interpolating theorem prover. Theoretical Computer Science,
345(1):101–121, 2005.
43. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: a proof assistant forhigher-order logic. Springer, 2002.
44. E. Pek, X. Qiu, and P. Madhusudan. Natural proofs for data structure manipulation in C using separation logic. In PLDI ’14, pages 440–451. ACM, 2014.
45. U. S. Reddy. Term rewriting induction. In CADE-10, volume 449 of LNCS, pages
162–177. Springer, 1990.
46. A. Reynolds and V. Kuncak. Induction for SMT solvers. In VMCAI ’15, volume
8931 of LNCS, pages 80–98. Springer, 2015.
47. P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI ’08, pages 159–169.
ACM, 2008.
48. P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for horn-clauseverification. In CAV ’13, volume 8044 of LNCS, pages 347–363. Springer, 2013.
49. W. Sonnex, S. Drossopoulou, and S. Eisenbach. Zeno: An automated prover for
properties of recursive data structures. In TACAS ’12, volume 7214 of LNCS,
pages 407–421. Springer, 2012.
50. P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive programs.
In SAS ’11, volume 6887 of LNCS, pages 298–315. Springer, 2011.
51. Q.-T. Ta, T. C. Le, S.-C. Khoo, and W.-N. Chin. Automated mutual explicit
induction proof in separation logic. In FM ’16, pages 659–676. Springer, 2016.
52. T. Terauchi. Dependent types from counterexamples. In POPL ’10, pages 119–130.
ACM, 2010.
53. T. Terauchi and A. Aiken. Secure information flow as a safety problem. In SAS’05, volume 3672 of LNCS, pages 352–367. Springer, 2005.
54. H. Unno and N. Kobayashi. On-demand refinement of dependent types. In FLOPS’08, volume 4989 of LNCS, pages 81–96. Springer, 2008.
55. H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP
’09, pages 277–288. ACM, 2009.
56. H. Unno, N. Kobayashi, and A. Yonezawa. Combining type-based analysis andmodel checking for finding counterexamples against non-interference. In PLAS
’06, pages 17–26. ACM, 2006.
57. H. Unno and T. Terauchi. Inferring simple solutions to recursion-free horn clauses
via sampling. In TACAS ’15, volume 9035 of LNCS, pages 149–163. Springer,
2015.
58. H. Unno, S. Torii, and H. Sakamoto. Automating induction for solving horn clauses.
Full version, available from http://www.cs.tsukuba.ac.jp/~uhiro/, 2017.
59. N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. Peyton Jones. Refinement
types for Haskell. In ICFP ’14, pages 269–282. ACM, 2014.
60. H. Xi and F. Pfenning. Dependent types in practical programming. In POPL ’99,
pages 214–227. ACM, 1999.

20