Automating Induction for Solving Horn Clauses
Hiroshi Unno

Sho Torii

arXiv:1610.06768v1 [cs.PL] 21 Oct 2016

University of Tsukuba
{uhiro,sho}@logic.cs.tsukuba.ac.jp

Abstract

important ones such as functional equivalence, associativity,
commutativity, distributivity, monotonicity, idempotency, and
non-interference.

Verification problems of programs written in various paradigms
(such as imperative, logic, concurrent, functional, and objectoriented ones) can be 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 an SMT solver to discharge proof
obligations arising in the proof search. The main advantage of
the proposed method is that it 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, and non-interference. Furthermore, our novel combination
of Horn clause constraints with inductive theorem proving enables
us to naturally and automatically axiomatize recursive functions
that are possibly non-terminating, non-deterministic, 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 and obtained
promising results in preliminary experiments.

2. It can solve Horn clause constraints over whatever background
theories supported by the underlying SMT solver. Example constraints in Section 3.3 are over the theories of nonlinear arithmetics and algebraic data structures, which have not been supported by available Horn constraint solvers to our knowledge.
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 functional program
Dmult (in OCaml syntax).1
let rec mult x y =
if y=0 then 0 else
let rec mult_acc x y
if y=0 then a else
let main x y a =
assert (mult x y +

x + mult x (y-1)
a =
mult_acc x (y-1) (a+x)
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 tail-recursive 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 mult
and 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-byvalue evaluation strategy adopted by OCaml, never causes an asser∗
tion failure, that is ∀x, y, a ∈ N. main x y a −→
6
assert false.
By using existing Horn constraint generation methods for call-byvalue functional programs [37, 53], the relational verification problem is reduced to the constraint solving problem of the following
Horn clause constraint set Hmult :



 P (x, 0, 0),





 P (x, y, x + r) ⇐ P (x, y − 1, r) ∧ (y 6= 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. Introduction
Verification problems of programs written in various paradigms, including imperative [28], logic, concurrent [27], functional [45, 52,
53, 56], and object-oriented [35] ones, can be reduced to problems
of solving Horn clause constraints on predicate variables that represent unknown inductive invariants. A given program is guaranteed
to satisfy its specification if the Horn constraints generated from the
program have a solution (see [25] 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 checking of first-order formulas with
inductively defined predicates, which are then checked by induction
on the derivation of the predicates. The main technical challenge
here is how to automate inductive proofs. To this end, we propose
an inductive proof system tailored for Horn constraint solving and
an SMT-based technique to automate proof search in the system.
Compared to previous Horn constraint solving methods [25,
26, 31, 41, 46, 50, 53, 54] based on Craig interpolation [18, 42],
abstract interpretation [17], and PDR [10], the proposed method
has two major advantages:

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 of mult and expresses
that mult returns 0 if 0 is given as the second argument. The sec1 Our work

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

1. It can verify relational specifications where multiple function
calls need to be analyzed simultaneously. As shown in Sections 3.3 and 5, the class of specifications includes practically

1

2016/10/24

ond clause in Hmult , P (x, y, x + r) ⇐ P (x, y − 1, r) ∧ (y 6= 0)
is generated from the 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 Horn clauses are similarly generated from the then- and else- branches of mult acc and
the 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 the predicate variables P and
Q, the correctness of the constraint generation method [53] guarantees that the call-by-value evaluation of main x y a never causes
an assertion failure.
The previous Horn constraint solving methods, however, cannot solve this kind 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 )
that 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 canceling x × y, because x and y are the only shared arguments between
P (x, y, r1 ) and Q(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 the above
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 ) and Q(x, y, a, r2 ) imply r1 + a = r2 (i.e.,
Hmult is solvable), by simultaneously analyzing P (x, y, r1 ) and
Q(x, y, a, r2 ). 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) of Hmult , and uses
induction on the derivation of P (x, y, r1 ) to prove the conjecture
∀x, y, r1 , a, r2 . (P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ∧ (r1 + a 6= r2 ) ⇒ ⊥)
represented by the goal clause (i.e., the clause whose head is not a
predicate application) of Hmult . Section 2 gives an overview of our
method using this running example.
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 clause constraints can naturally axiomatize
various advanced language features including recursive functions
that are partial (i.e., possibly non-terminating), non-deterministic,
higher-order, exception-raising, and over non-inductively defined
data types (recall that Hmult axiomatizes the partial functions mult
and mult acc, and see Section 3.3 for more examples). Furthermore, we can automate the axiomatization process by using program logics such as Hoare logics for imperative and refinement
type systems [45, 52, 53, 57] for functional programs. In fact, researchers have developed and made available tools such as SeaHorn [28] and JayHorn [35], respectively for translating C and Java
programs into Horn clause constraints. In spite of the expressiveness, Horn clause constraints have a simpler logical semantics compared to other popular IVLs like Boogie [2] and Why3 [8]. This
simplicity enabled us to directly apply inductive theorem proving
and made the correctness proof and implementation easier.
In contrast to our induction method based on the logic of predicates defined by Horn clause constraints, most state-of-the-art automated inductive theorem provers such as ACL2s [13], Leon [49],
Dafny [40], Zeno [48], HipSpec [15], and CVC4 [44] are based on
2 See

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

2

logics of pure total functions over inductively-defined data structures. Consequently, the axiomatization of advanced language features and specifications becomes a non-straightforward process,
which often requires users’ manual intervention and possibly has
a negative effect on the automation of induction later. Thus, our approach complements automated inductive 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 formalizes Horn constraint solving problems
and shows examples of the reduction from various program verification problems to Horn constraint solving problems. Section 4
formalizes our constraint solving method and proves its correctness. Section 5 reports on our prototype implementation based on
the proposed method and the results of preliminary experiments.
We compare our method with related work in Section 6 and conclude the paper with some remarks on future work in Section 7.

2. Overview of Induction-Based Horn Constraint
Solving Method
In this section, we use the Horn constraint set Hmult in Section 1
as a running example to give an overview of our induction-based
Horn constraint solving method. Our method interprets the definite
clauses (i.e., the clauses whose head is a predicate application)
of a given Horn constraint set as derivation rules for predicate
applications P (e
t), which we call atoms henceforth. For example,
the definite clauses Dmult ⊆ Hmult are interpreted as the following
derivation rules:
P (x, y − 1, r − x)
|= y 6= 0
|= y = 0 ∧ r = 0
P (x, y, r)
P (x, y, r)
|= y = 0 ∧ a = r
Q(x, y, a, r)

Q(x, y − 1, a + x, r)
Q(x, y, a, r)

|= y 6= 0

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. The above rules
 inductively define the least predicate interpretation {P 7→ (x, y, r) ∈ Z3 | x × y = r ∧ y ≥ 0 , Q 7→
{(x, y, a, r) ∈ Z4 | x × y + a = r ∧ y ≥ 0}} that satisfies the
definite clauses Dmult . It then follows that a given Horn constraint
set has a solution if and only if all the goal clauses (i.e., the clauses
whose head is not an atom) are valid under the interpretation (see
Corollary 1 for the proof). Therefore, constraint solving of Hmult
boils down to the validity checking of the goal clause
∀x, y, r1 , a, r2 . (P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ∧ (r1 + a 6= r2 ) ⇒ ⊥)
under the least predicate interpretation for P and Q.
To check the validity of such a conjecture, our method uses
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. ((∀D′ ≺ D.P(D′ )) ⇒ P(D)), where D′ ≺ D represents
that D′ is a strict sub-derivation of D.
Formally, we propose an inductive proof system for deriving
judgments of the form D; Γ; A; φ ⊢ ⊥, where ⊥ represents the
contradiction, φ represents a formula without atoms, A represents
a set of atoms, Γ represents a set of induction hypotheses and userspecified lemmas, and D represents a set of definite clauses that
define the least predicate 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

2016/10/24

P (e
t) ∈ A
{e
y} = fvs(A) ∪ fvs(φ)
x
e : fresh  σ V
= {e
y 7→ x
e}


D; Γ ∪ ∀e
x. P (σe
t) ≺ P (e
t) ∧ σA ⇒ ¬(σφ) ; A; φ ⊢ ⊥
D; Γ; A; φ ⊢ ⊥
(I NDUCT)

′
P (e
t) ∈ A
σ= x
e 7→ e
t
D; Γ; A ∪ σA ; φ ∧ σφ′ ⊢ ⊥
(for each (P (e
x) ⇐ A′ ∧ φ′ ) ∈ D)
D; Γ; A; φ ⊢ h
(U NFOLD)

 V

∀e
x. P (te′ ) ≺ P (e
t) ∧ A ′ ⇒ φ′ ∈ Γ
dom(σ) = {e
x}
V
V
P (σ te′ ) ≺ P (e
t)
|= A ∧ φ ⇒ σA′
D; Γ; A; φ ∧ σφ′ ⊢ ⊥
D; Γ; A; φ ⊢ ⊥
(A PPLY⊥)
|= φ ⇒ ⊥
D; Γ; A; φ ⊢ ⊥

J3

(VALID⊥)
J1

J4

(VALID⊥)
(U NFOLD)
J0
Jmult

J5

(VALID⊥)
J7
(A PPLY⊥)
J6
(U NFOLD)
(U NFOLD)

(VALID⊥)
J2

(I NDUCT)

J0 , Dmult ; Γmult ; A∅ ; r1 + a 6= r2 ⊢ ⊥
J1 , Dmult ; Γmult ; A∅ ; r1 + a 6= r2 ∧ y = 0 ∧ r1 = 0 ⊢ ⊥
J2 , Dmult ; Γmult ; AP ; r1 + a 6= r2 ∧ y 6= 0 ⊢ ⊥
J3 , Dmult ; Γmult ; A∅ ; r1 + a 6= r2 ∧ y = 0 ∧ r1 = 0 ∧ a = r2 ⊢ ⊥
J4 , Dmult ; Γmult ; AQ ; r1 + a 6= r2 ∧ y = 0 ∧ r1 = 0 ∧ y 6= 0 ⊢ ⊥
J5 , Dmult ; Γmult ; AP ; r1 + a 6= r2 ∧ y 6= 0 ∧ y = 0 ∧ a = r2 ⊢ ⊥
J6 , Dmult ; Γmult ; AP Q ; r1 + a 6= r2 ∧ y 6= 0 ⊢ ⊥
J7 , Dmult ; Γmult ; AP Q ; r1 + a 6= r2 ∧ y 6= 0 ∧ r1 + a = r2 ⊢ ⊥

(VALID⊥)

Γmult , {∀x′ , y ′ , r1′ , a′ , r2′ .((P (x′ , y ′ , r1′ ) ≺ P (x, y, r1 ))∧
P (x′ , y ′ , r1′ ) ∧ Q(x′ , y ′ , a′ , r2′ ) ⇒ r1′ + a′ = r2′ )}

Figure 1. A simplified version of the inference rules in Figure 3
for the judgment D; Γ; A; φ ⊢ ⊥.

A∅ , {P (x, y, r1 ), Q(x, y, a, r2 )}
AP , A∅ ∪ {P (x, y − 1, r1 − x)}
AQ , A∅ ∪ {Q(x, y − 1, a + x, r2 )}

scope within the clause, and are considered to be universally quantified (see Section 3 for a formal account). Intuitively, a judgment
D; Γ; A; φ ⊢ ⊥ means that under
V theVleast predicate interpretation
induced by D, the formula Γ ∧ A ∧ φ ⇒ ⊥ is valid. For
example, consider the following judgment Jmult :

AP Q , AP ∪ {Q(x, y − 1, a + x, r2 )}
Figure 2. The structure of an example derivation of Jmult .

Jmult , Dmult ; ∅; {P (x, y, r1 ), Q(x, y, a, r2 )} ; (r1 +a 6= r2 ) ⊢ ⊥
P (e
t) on which the induction (that has introduced the hypothesis) has been performed.

If Jmult is derivable, P (x, y, r1 )∧Q(x, y, a, r2 )∧(r1 +a 6= r2 ) ⇒
⊥ is valid under the least predicate interpretation induced by Dmult ,
and hence Hmult has a solution.
The inference rules for the judgment D; Γ; A; φ ⊢ ⊥ are shown
in Figure 3. The rules there, however, are too general and formal
for the purpose of providing an overview of the idea. Therefore,
we defer a detailed explanation of the rules to Section 4, and here
explain a simplified version shown in Figure 1, obtained from the
complete version by eliding some conditions and subtleties while
retaining the essence. The rules are designed to exploit Γ and D
for iteratively
V updating the current knowledge represented by the
formula A ∧ φ until a contradiction is implied. The first rule
I NDUCT selects an atom P (e
t) ∈ A and performs induction on
the derivation of the atom
by
 induction hypothesis
V adding a new
∀e
x. P (σe
t) ≺ P (e
t) ∧ σA ⇒ ¬(σφ) to Γ. Here, a map σ is
used to generalize the free term variables ye that occur in A or φ
(denoted by fvs(A) ∪ fvs(φ)) into fresh variables x
e, and P (σe
t) ≺
P (e
t) requires that the derivation of P (σe
t) is a strict sub-derivation
of that of P (e
t). The second rule U NFOLD selects an atom P (e
t) ∈
A, performs a case analysis on the last rule used to derive the atom,
which is represented by a definite clause in DVof the form PV
(e
x) ⇐
A′ ∧ φ′ , and updates the
current
knowledge
A
∧
φ
with
(A ∪

σA′ )∧φ∧σφ′ for σ = x
e 7→ e
t 
. The third rule APPLY⊥ selects an

V
induction hypothesis in Γ, ∀e
x. P (te′ ) ≺ P (e
t) ∧ A ′ ⇒ φ′ ,
and tries to find an instantiation σ of the quantified variables x
e such
that
V
• the instantiated premise σA′ of the hypothesis is implied by
V
the current knowledge A ∧ φ and
• the derivation of the atom P (σ te′ ) ∈ σA′ to which the hypothesis is being applied is a strict sub-derivation of that of the atom

If
the rule updates the current knowledge with
V such a σ is found,
A ∧ φ ∧ σφ′ . The fourth rule VALID⊥ checks whether φ ⇒
⊥ is valid, and if it is the case, closes the proof branch under
consideration.
Figure 2 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 I NDUCT, we obtain the
subgoal J0 with an induction hypothesis Γmult added. We then
apply U NFOLD 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 as the result, because Dmult has two clauses with the head
that matches with the atom 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 the rule U NFOLD, we further get two subgoals J3 and
J4 . Both J3 and J4 are proved 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 the rule U NFOLD, we obtain two subgoals J5 and J6 .
J5 is proved by the rule VALID⊥ because |= φ5 ⇒ ⊥ holds.
We then apply the induction hypothesis in Γmult ,
∀x′ , y ′ , r1′ , a′ , r2′ .((P (x′ , y ′ , r1′ ) ≺ P (x, y, r1 ))∧
P (x′ , y ′ , r1′ ) ∧ Q(x′ , y ′ , a′ , r2′ ) ⇒ r1′ + a′ = r2′ )
to the atom P (x, y − 1, r1 − x) ∈ AP Q in J6 using the rule
A PPLY⊥. Note that this can be done by using the quantifier

3

2016/10/24

instantiation σ defined by
 ′
x 7→ x, y ′ 7→ y − 1, r1′ 7→ r1 − x, a′ 7→ a + x, r2′ 7→ r2 ,

vanced language features, including higher-order functions and
exceptions.
The syntax of Horn Clause Constraint Sets (HCCSs) over the
theory TZ of quantifier-free linear integer arithmetic is defined by

because σ(P (x′ , y ′ , r1′ )) = P (x, y − 1, r1 − x) ≺ P (x, y, r1 )
holds and the premise σ(P (x′ , y ′ , r1′ ) ∧ Q(x′ , y ′ , a′ , r2′ )) =
P (x, y − 1, r1 − x) ∧ Q(x, y − 1, a + x, r2 ) of V
the instantiated
hypothesis is implied by the current knowledge AP Q ∧ r1 +
a 6= r2 ∧ y 6= 0. We thus obtain the subgoal J7 , where the
φ-part of the knowledge is updated to

(HCCSs) H : := {hc 1 , . . . , hc m }
(Horn clauses) hc : := h ⇐ b
(heads) h : := P (e
t) | ⊥

(bodies) b : := P1 (e
t1 ) ∧ · · · ∧ Pm (e
tm ) ∧ φ
(TZ -formulas) φ : := t1 ≤ t2 | ⊤ | ⊥ | ¬φ | φ1 ∧ φ2 | φ1 ∨ φ2
(TZ -terms) t : := x | n | t1 + t2

r1 + a 6= r2 ∧ y 6= 0 ∧ σ(r1′ + a′ = r2′ )
≡ r1 + a 6= r2 ∧ y 6= 0 ∧ (r1 − x) + (a + x) = r2
≡ r1 + a 6= r2 ∧ y 6= 0 ∧ r1 + a = r2 .

Here, the meta-variables P and x respectively represent predicate
variables and term variables, and e
t represents a sequence of terms
t1 , . . . , tm . We write the arity of P as ar (P ). Note that, in the
syntax of TZ -formulas, linear inequalities t1 ≤ t2 can be used to
encode t1 < t2 , t1 = t2 , and t1 6= t2 . For example, t1 < t2
is encoded as t1 + 1 ≤ t2 . The formula ⊤ (resp. ⊥) represents
the tautology (resp. the contradiction). We here restrict ourselves
to TZ for simplicity, although our induction-based Horn constraint
solving method formalized in Section 4 supports constraints over
whatever background theories supported by the underlying SMT
solver, including the theories of nonlinear arithmetics, algebraic
data structures, and uninterpreted function symbols as shown in
Section 3.3.

Because this implies a contradiction, J7 is finally proved by
using the rule VALID⊥.
To automate proof search in the system, this paper proposes
an SMT-based technique: we use an off-the-shelf SMT solver for
checking whether the current knowledge implies a contradiction
(in the rule VALID⊥) and whether there is an element of Γ that can
be used to update the current knowledge, by finding a quantifier
instantiation σ (in the rule A PPLY⊥). The use of an SMT solver
provides our method with efficient and powerful reasoning about
data structures supported by SMT, including integers, real numbers,
arrays, algebraic data types (ADTs), and uninterpreted functions.
There, however, still remain two challenges to be addressed towards
full automation:

3.1 Notation for HCCSs

1. Challenge: How to check (in the rule A PPLY⊥) the strict subderivation relation P (e
t′ ) ≺ P (e
t) between the derivation of an
′
atom P (e
t ) to which an induction hypothesis in Γ is being applied, and the derivation of the atom P (e
t) 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 A PPLY⊥ to J6 .
Our solution: The formalized rules presented in Section 4 keep
sufficient information for checking the strict sub-derivation relation: we associate each induction hypothesis in Γ with an induction identifier α, and each atom in A with a set M of identifiers indicating which hypotheses can be applied to the atom.
Further details are explained in Section 4.

A Horn clause constraint set H is a finite set {hc 1 , . . . , hc m }
of Horn clauses. A Horn clause h ⇐ b consists of a head h
and a body b. We often abbreviate a Horn clause h ⇐ ⊤ as
h. We write pvs(hc) for the set of
S the predicate variables that
occur in hc and define pvs(H) = hc∈H pvs(hc). Similarly, we
write fvs(hc)
S for the set of 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 ) = ∅. We write H↾P for the
e
set of Horn
W clauses in H of the form P (t) ⇐ b. We define H(P ) =
λe
x.∃e
y. m
e = e
ti ) if H↾P = P (e
ti ) ⇐ bi i∈{1,...,m}
i=1 (bi ∧ x
where {e
y } = fvs(H↾P ) and {e
x} ∩ {e
y} = ∅. By using H(P ), an
HCCS H is logically interpreted as the formula
^
∀e
xP . (H(P )(e
xP ) ⇒ P (e
xP )) ,

2. Challenge: In which order should the rules be applied?
Our solution: This paper adopts the following simple strategy,
and evaluates it by experiments.

P ∈pvs(H)

where x
eP = x1 , . . . , xar(P ) . A Horn clause with the head of
the form P (e
t) (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) = ∅.

• Repeatedly apply the rule A PPLY⊥ if possible, until no new

knowledge is obtained. (Even if the rule does not apply, applications of I NDUCT and U NFOLD explained in the following items may make A PPLY⊥ applicable.)
• If the current knowledge cannot be updated by using the

rule A PPLY⊥, select some atom from A in a breadth-first
manner, and apply the rule I NDUCT to the atom.

3.2 Predicate Interpretation
A predicate interpretation ρ for an HCCS H is a map from each
predicate variable P ∈ 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 all hc ∈ H. For
example, ρmult = {P 7→ (x, y, r) ∈ Z3 | x × y = r , Q 7→

(x, y, a, r) ∈ Z4 | x × y + a = r } is a solution of the HCCS
Hmult in Section 1.

• Apply the rule U NFOLD whenever I NDUCT is applied.
• Try to apply the rule VALID⊥ whenever the φ-part of the

knowledge is updated.

3. Horn Constraint Solving Problems
This section formalizes Horn constraint solving problems and
proves the correctness of our reduction from Horn constraint solving to inductive theorem proving in Corollary 1. Section 3.3 also
shows example Horn constraint solving problems reduced from
(relational) verification problems of programs that use various ad-

Definition 1 (Horn Constraint Solving Problems). A Horn constraint solving problem is the problem of checking whether a given
HCCS H has a solution.

4

2016/10/24

plates for the functions in Dmult .

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 the following function on predicate interpretations.
n
n
o
o
FH (ρ) = P 7→ (e
x) ∈ Zar (P ) ρ |= H(P )(e
P ∈ dom(ρ)
x)

mult :
mult acc :

(x : int) → (y : int) → {r : int | P (x, y, r)}
(x : int) → (y : int) → (a : int) →
{r : int | Q(x, y, a, r)}

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 constraint generation method then
type-checks the program against the type templates, and obtains
the Horn constraint set Hmult in Section 1, which has a solution if
and only if the program is typable under a refinement type system.
The refinement type system guarantees that if a given program is
typable, the evaluation of main n never causes an assertion failure
for any integer n.

Because FH is continuous [33], the least fixed-point µFH of FH
exists. Furthermore, we can express it as
[ i
FH ({P 7→ ∅ | P ∈ pvs(H)}),
µFH =
i∈N

i
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 a solution of def (H).
Furthermore, µFH is the least solution. Formally, we can prove the
following proposition.

Example 2. Consider the following program.
let rec sum n =
if n < 0 then n + sum (n + 1)
else if n = 0 then 0 else n + sum (n - 1)
let rec sum_acc n a =
if n < 0 then sum_acc (n + 1) (a + n)
else if n = 0 then a else sum_acc (n - 1) (a + n)
let main n a = assert(sum n + a = sum_acc n a)

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).

In a similar manner to Example 1, we obtain the following Horn
constraint set:


P (0, 0),








P (x, r + x) ⇐ P (x + 1, r) ∧ x < 0,






 P (x, r + x) ⇐ P (x − 1, r) ∧ x > 0,

Q(0, a, a),



Q(x, a, r) ⇐ Q(x + 1, a + x, r) ∧ x < 0, 







Q(x, a, r) ⇐ Q(x − 1, a + x, r) ∧ x > 0, 




⊥ ⇐ P (x, r1 ) ∧ Q(x, a, r2 ) ∧ r1 + a 6= r2

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).
3.3 Examples Reduced from Program Verification Problems

Here, the predicate variable P (resp. Q) represents an inductive
invariant among the arguments and the return value of the function sum (resp. sum acc). Here, suppose that the main function is
replaced by

This section shows example Horn constraint solving problems
reduced from (relational) verification problems of programs that
use advanced language features such as algebraic data structures,
higher-order functions, and exceptions. The reduction used in this
section is mostly based on an existing Horn constraint generation
method [53] for an ML-like (i.e., call-by-value, statically-typed,
and higher-order) functional language. The method can be used to
reduce a given assertion safety verification problem defined below
into a Horn constraint solving problem.

let main n =
if n >= 0 then assert (2 * sum n = n * (n + 1))
We then obtain the following goal clause over the nonlinear integer
arithmetic instead:
⊥ ⇐ P (x, r) ∧ x ≥ 0 ∧ 2 × r 6= x × (x + 1)

Definition 2 (Assertion Safety Verification Problems). An assertion safety verification problem of a given functional program, with
a special function main of the ordinary ML type int → · · · →
int → unit, is the problem of deciding whether

The method can automatically axiomatize complex recursive
functions on integers.
Example 3. Consider the following program with complex recursion.

∀n1 , . . . , nm ∈ Z. main n1 . . . nm −→
/ ∗ assert false,
where −→ is the one-step evaluation relation. We call the program
safe if this property holds, and unsafe otherwise.
The constraint generation method is based on refinement types [57],
which are used internally to express value dependent inductive invariants and specifications of the program. The following theorem
states the soundness of the reduction.

let rec mc91 x =
if x > 100 then x - 10 else mc91 (mc91 (x + 11))
let main x = if x <= 101 then assert(mc91 x = 91)
By using the refinement type template
mc91 :

(x : int) → {r : int | P (x, r)}

the constraint generation method returns the following Horn constraint set:



 P (x, x − 10) ⇐ x > 100,
P (x, s) ⇐ P (x + 11, r) ∧ P (r, s) ∧ x ≤ 100,

 ⊥ ⇐ P (x, r) ∧ x ≤ 101 ∧ r 6= 91

Theorem 1 (Soundness [53]). Let H be the HCCS generated from
a program D. If there exists a solution ρ of H, then D is safe.
We now show example Horn constraints generated by the
method. The partial recursive functions shown in Section 1 are
automatically axiomatized using refinement types as follows.

Here, the predicate variable P represents an inductive invariant
among the arguments and the return value of the function mc91.

Example 1. Recall the program Dmult in Section 1. The constraint
generation method first prepares the following refinement type tem-

5

2016/10/24

Our method can also handle recursive functions on non-inductively
defined data types such as real numbers.

The method can also axiomatize higher-order functions into
Horn clause constraints automatically.

Example 4. Consider the following program that models a dynamical system from [38].

Example 6. Consider the following higher-order program.

type list = Nil | Cons of int * list
let rec dyn_sys vc =
let fa = 0.5418 *. vc *. vc in (* the force control *)let rec sum_list l = match l with
| Nil -> 0
let fr = 1000. -. fa in
| Cons(x, xs) -> x + sum_list xs
let ac = 0.0005 *. fr in
let rec fold_left f s l = match l with
let vc’ = vc +. ac in
| Nil -> s
assert (vc’ < 49.61); (* the safety velocity *)
| Cons(x, xs) -> fold_left f (f s x) xs
dyn_sys vc’
let plus x y = x + y
let main () = dyn_sys 0. (* the initial velocity *)
let main l = assert(sum_list l = fold_left plus 0 l)
By using the refinement type template
By using the refinement type templates
dyn sys : {x : real | P (x)} → unit
sum list : (x : list) → {r : int | P (x, r)}
the constraint generation method returns the following Horn confold left : (f : (a : int) → (b : int) → {c : int | Q(a, b, c)})
straint set:
→ (x : int) → (y : list) → {z : int | R(x, y, z)}


plus : (x : int) → (y : list) → {r : list | S(x, y, r)}
P (vc ′ ) ⇐ P (vc) ∧ fa = 0.5418 × vc × vc ∧ fr = 1000 − fa∧ 






 the constraint generation method returns the following Horn conac = 0.0005 × fr ∧ vc ′ = vc + ac ∧ vc ′ < 49.61,
P (0),
straint set over the theories of linear integer arithmetic and alge



 ⊥ ⇐ P (vc) ∧ fa = 0.5418 × vc × vc ∧ fr = 1000 − fa∧
 braic data structures:


′
′


ac = 0.0005 × fr ∧ vc = vc + ac ∧ vc ≥ 49.61
P (Nil, 0),




′
′


Here, the predicate variable P represents an inductive invariant on

 P (Cons(x, l ), x + r) ⇐ P (l , r),






the argument of the function dyn sys.

 R(s, Nil, s),
′
′
′
′
R(s,
Cons(x,
l
),
r
)
⇐
Q(s,
x,
r)
∧
R(r,
l
,
r
),
The constraint generation method can handle functional pro




 S(x, y, x + y),
grams that manipulate user-defined algebraic data structures.






Q(x, y, z) ⇐ S(x, y, z),




Example 5. Consider the following program that manipulates
⊥ ⇐ P (l, r1 ) ∧ R(0, l, r2 ) ∧ r1 6= r2
lists.
type list = Nil | Cons of int * list

The method can also axiomatize recursive functions that may
raise exceptions into Horn clause constraints.

let
|
|
let
|
|

rec append l ys = match l with
Nil -> ys
Cons(x, xs) -> Cons(x, append xs ys)
rec drop n l = match l with
Nil -> Nil
Cons(x, xs) ->
if n = 0 then Cons(x, xs) else drop (n - 1) xs
let rec take n l = match l with
| Nil -> Nil
| Cons(x, xs) ->
if n = 0 then Nil else Cons(x, take (n - 1) xs)
let main n xs =
assert(append (take n xs) (drop n xs) = xs)

Example 7. Consider the following higher-order program that
manipulates lists and possibly raises and catches exceptions.
exception Not_found
type int_option = None | Some of int
let
|
|
let
|
|
let

By using the refinement type templates
append :
drop :
take :

(x : list) → (y : list) → {r : list | P (x, y, r)}
(x : int) → (y : list) → {r : list | Q(x, y, r)}
(x : int) → (y : list) → {r : list | R(x, y, r)}

rec find p l = match l with
[] -> raise Not_found
x::xs -> if p x then x else find p xs
rec find_opt p l = match l with
[] -> None
x::xs -> if p x then Some x else find_opt p xs
main p l = try find_opt p l = Some (find p l)
with Not_found -> find_opt p l = None

Here, find and find_opt respectively use the exception Not_found
and the option type int_option, defined respectively in the first
and the second lines, for finding the first element of the list l satisfying the predicate p : int → bool. The constraint generation
method cannot directly handle this program because the underlying
refinement type system does not support exceptions. Note, however,
that we can mechanically transform the program into the following
one by eliminating exceptions using a selective CPS transformation [47].

the constraint generation method returns the following Horn constraint set over the theory of algebraic data structures:


P (Nil, l2 , l2 ),




 P (Cons(x, l), l2 , Cons(x, r)) ⇐ P (l, l2 , r),









Q(n, Nil, Nil),




′
′


 Q(n, Cons(x, l ), Cons(x, l )) ⇐ n = 0,

′
′
Q(n, Cons(x, l ), r) ⇐ Q(n − 1, l , r) ∧ n 6= 0,




R(n, Nil, Nil),




′




R(n, Cons(x, l ), Nil) ⇐ n = 0,




′
′


R(n,
Cons(x,
l
),
Cons(x,
r))
⇐
Q(n
−
1,
l
,
r)
∧
n
=
6
0,




⊥ ⇐ P (n, l, r1 ) ∧ Q(n, l, r2 ) ∧ R(r1 , r2 , r) ∧ r 6= l

type exc = Not_found
type int_option = None | Some of int
let
|
|
let

6

rec find p l ok ex = match l with
[] -> ex Not_found
x::xs -> if p x then ok x else find p xs ok ex
rec find_opt p l = match l with

2016/10/24

| [] -> None
| x::xs -> if p x then Some x else find_opt p xs
let main p l =
find p l (fun x -> assert (find_opt p l = Some x))
(fun Not_found -> assert (find_opt p l = None))

we obtain the following Horn constraint set:

P (x, y) ⇐ y > 0,



P (x, y) ⇐ P (x, y) ∧ y ≤ 0,




 Q(a, b) ⇐ Q(x, r) ∧ Q(a, b) ∧ x 6= 0,

Q(a, b) ⇐ P (a, b),
R(f, 0, y) ⇐ Q(0, y),




R(f, x, r1 + r2 ) ⇐




Q(0, y) ∧ Q(x, r1 ) ∧ R(f, x − 1, r2 ) ∧ x 6= 0,

⊥ ⇐ Q(randpos, x, y) ∧ y ≤ 0

Note here that two function arguments ok and ex of the ordinary
ML type int → unit, which respectively represent continuations
for normal and exceptional cases, are added to the function find.
The constraint generation method then prepares the following refinement type templates:
find :
find opt :















Pok (p, x :: xs, r) ⇐ p x = ⊤,
Pok (p, x :: xs, r) ⇐ Pok (p, xs, r) ∧ p x = ⊥,
Pex (p, [ ], Not Found),
Pex (p, x :: xs, r) ⇐ Pex (p, xs, r) ∧ p x = ⊥,
Q(p, [ ], None),
Q(p, x :: xs, Some x) ⇐ p x = ⊤,
Q(p, x :: xs, r) ⇐ Q(p, xs, r) ∧ p x = ⊥,
⊥ ⇐ Pok (p, l, r1 ) ∧ Q(p, l, r2 ) ∧ Some r1 6= r2
⊥ ⇐ Pex (p, l, r1 ) ∧ r1 6= Not Found
⊥ ⇐ Pex (p, l, Not Found) ∧ Q(p, l, r2 ) ∧ None 6= r2

Example 9. Consider the following C program.
int mult(int x, int y) {
int r=0; while(y != 0) r = r + x; y = y - 1;
return r;
}
Using the Hoare logic, we obtain the following Horn constraint set:



 I(x, y, r) ⇐ r = 0,
I(x, y − 1, r + x) ⇐ I(x, y, r) ∧ y 6= 0,

 R(x, y, r) ⇐ I(x, y, r) ∧ y = 0
















Here, the predicate variable I represents the loop invariant of the
while loop, and R represents invariants among the arguments x, y
and the return value r of the procedure mult. The goal clause
⊥ ⇐ P (x, y, r1 ) ∧ R(x, y, r2 ) ∧ r1 6= r2 , with the predicate
P defined by Hmult in Section 1, represents the equivalence of C
and OCaml implementations of mult.















It is also worth mentioning here that there have also been
proposed techniques for reducing verification problems of multithreaded programs [25, 27] and functional programs with the
call-by-need evaluation strategy [56] into Horn constraint solving
problems. Angelic non-determinism [29] and temporal specifications [7] can also be automatically axiomatized into Horn clause
constraints extended with existentially quantified heads.

Here, p is an uninterpreted function symbol, which is essential for
the success of Horn constraint solving here because we need to
express the fact that the multiple occurrences of p x in the body
of different clauses return the same value if the same function is
passed as p.

4. Induction-based Horn Constraint Solving
Method

Our method also supports demonic non-determinism.

As explained in Section 2, our method is based on the reduction
from Horn constraint solving into inductive theorem proving. The
correctness of the reduction is established by Corollary 1 in Section 3. The remaining task is to develop an automated method for
proving the inductive conjectures obtained from Horn clause constraints. To this end, Section 4.1 formalizes our inductive proof system tailored to Horn constraint solving and proves its correctness.
Section 4.2 discusses how to automate proof search in the system
using an SMT solver.

Example 8. Consider the following higher-order program that
calls rand_int to generate random integers.
let rec randpos dummy =
let n = rand_int () in
if n > 0 then n else randpos dummy
let rec sum_fun f n =
if n = 0 then f 0
else f n + sum_fun f (n - 1)
let main n = assert (sum_fun randpos n > 0)

4.1 Inductive Proof System
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 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 (e
t) instead of ⊥. For deriving such judgments, we will introduce
new rules F OLD and VALIDP later in this section. Γ represents a

Note that the specification is satisfied because the function randpos
never returns a non-positive integer. By using the refinement type
templates
randpos :
sum fun :











Our method based on Horn clause constraints is not limited to
relational verification of functional programs. By combining the
constraint generation tools for C [28] and Java [35], we can axiomatize relational verification problems across functional, imperative, object-oriented, and, of course, (constraint) logic programs
into Horn clause constraints.

(x : int → bool) → (y : list) →
({z : int | Pok (x, y, z)} → unit) →
({w : exc | Pex (x, y, w)} → unit) → unit
(x : int → bool) → (y : list) →
{z : int option | Q(x, y, z)}

Here, the predicate variable Pok represents invariants among the
first and the second arguments of find and the argument of the
third argument ok of find. The predicate variable Pex represents
invariants among the first and the second arguments of find and
the argument of the fourth argument ex of find. The predicate
variable Q represents invariants among the arguments and the
return value of find_opt. The constraint generation method then
obtains the following Horn constraint set over the theories of linear
integer arithmetic, algebraic data structures, and uninterpreted
function symbols:


























(x : int) → {y : list | P (x, y)}
(f : (a : int) → {b : int | Q(a, b)}) →
(x : int) → {y : int | R(f, x, y)}
7

2016/10/24

while (α ⊲ P (e
t), A, φ, h) ∈ Γ represents the induction hypothesis


 ^
∀e
x. P (e
t) ≺ P (e
t′ ) ∧
A∧φ⇒ h

Perform induction on the derivation of the atom P (e
t):
P◦M (e
t) ∈ A
Γ′= Γ ∪ (α ⊲ P (e
t), A, φ, h)
D; Γ′ ; (A \ P◦M (e
t)) ∪ PαM (e
t) ; φ ⊢ h
(α : fresh)
D; Γ; A; φ ⊢ h
(I NDUCT)

where {e
x} = fvs(P (e
t), A, φ, h)

that has been introduced by induction on the derivation of the atom
P (e
t′ ). 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(e
t). We will introduce a new rule A PPLYP later in this
section for using such lemmas and hypotheses
to obtain new knowl
Mm e
1 e
edge. A is also extended to be a set P1 M
α1 (t1 ), . . . , Pm αm (tm )
M e
of annotated atoms. Each element Pα (t) has two annotations:

Case-analyze the last rule used (where
W m rules are possible):
V
PαM (e
t) ∈ A
D(P )(e
t) = m
ei . (φi ∧ Ai )
i=1 ∃x
M ∪{α}
D; Γ; A ∪ Ai ◦
; φ ∧ φi ⊢ h
(for each i ∈ {1, . . . , m})
D; Γ; A; φ ⊢ h
(U NFOLD)
Apply an induction hypothesis or a user-specified lemma in Γ:
(g, A′ , φ′ , ⊥) ∈ Γ
dom(σ) = fvs(A′ )
|= φ ⇒ Jσg∈AK
|= φ ⇒ JσA′ ⊆AK
{e
x} = fvs(φ′ ) \ dom(σ)
D; Γ; A; φ ∧ ∀e
x.¬(σφ′ ) ⊢ h
D; Γ; A; φ ⊢ h
(A PPLY⊥)

• an induction identifier α indicating that the induction with the

identifier α is performed on the atom by the rule I NDUCT. If the
rule I NDUCT has never been applied to the atom, α is set to be
a special identifier denoted by ◦.

• a set of induction identifiers M indicating that if α′ ∈ M , the

derivation D of the atom PαM (e
t) satisfies D ≺ D′ for the
derivation D′ of the atom P (e
t′ ) on which the induction with
the identifier α′ is performed. Thus, an induction hypothesis
(α′ ⊲P (e
t′ ), A′ , φ′ , h′ ) ∈ Γ can be applied to the atom PαM (e
t) ∈
A only if α′ ∈ M holds.

Apply an induction hypothesis or a user-specified lemma in Γ:
(g, A′ , φ′ , P (e
t)) ∈ Γ
dom(σ) = fvs(A′ ) ∪ fvs(e
t)
|= φ ⇒ Jσg∈AK
|= φ ⇒ ∃e
x.(σφ′ ) n |= φ ⇒oJσA′ ⊆AK
{e
x} = fvs(φ′ ) \ dom(σ)
D; Γ; A ∪ P◦∅ (σe
t) ; φ ⊢ h
D; Γ; A; φ ⊢ h

(A PPLYP )

Apply a definite clause
V in D:
(P (e
t) ⇐ φ′ ∧ A′ ) ∈ D
|= φ ⇒ ∃e
x.(σφ′ )
{e
x} = fvs(φ′ ) \ dom(σ)

Note that we use these annotations only for guiding inductive
proofs and PαM (e
t) is logically equivalent to P (e
t). We often omit
these annotations when they are clear from the context.
The inference rules for the judgment D; Γ; A; φ ⊢ h are defined
in Figure 3. The rule I NDUCT selects an atom P◦M (e
t) ∈ A and performs induction on the derivation of the atom. This rule generates
a fresh induction identifier α 6= ◦, adds a new induction hypothesis (α ⊲ P (e
t), A, φ, h) to Γ, and replaces the atom P◦M (e
t) with
the annotated one PαM (e
t) for remembering that the induction with
the identifier α is performed on it. The rule U NFOLD selects an
atom PαM (e
t) V
∈ A and performs a case analysis on the last rule
P (e
t) ⇐ φ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 deM ∪{α}
rive the atom. The rule adds Ai ◦
and φi respectively to A and
M
φ in the i-th subgoal, where Aα represents PαM (e
t) P (e
t) ∈ A .
Note here that each atom in Ai is annotated with M ∪ {α} because the derivation of the atom Ai is a strict sub-derivation of that
of the atom PαM (e
t) on which the induction with the identifier α
has been performed. If α = ◦, it is the case that the rule I NDUCT
has never been applied to the atom PαM (e
t) yet. The rules A PPLY⊥
and A PPLYP select (g, A′ , φ′ , h) ∈ Γ, which represents a userspecified 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: the rules try to find an instantiation σ for
the free term variables in (g, A′ , φ′ , h), which are considered to be
universally quantified, and then use σ(g, A′ , φ′ , h) to obtain new
knowledge. Contrary to the rule U NFOLD
V , the rule F OLD tries to
use a definite clause P (e
t) ⇐ φ′ ∧ A′ ∈ D from theV
body to
the head direction: F OLD tries to find σ such that σ(φ′ ∧ A′ ) is
implied by the current knowledge, and update it with P (σe
t). This
rule is useful when we check the correctness of user specified lemmas. The rule VALID⊥ checks if φ is unsatisfiable, while the rule
VALIDP checks if the asserted proposition P (e
t) on the right-hand
V
side of the judgment is implied by the current knowledge A ∧ φ.
Given a Horn constraint solving problem H, our method reduces the problem into an inductive theoremVproving problem as
follows. For each goal clause in goal (H) = { Ai ∧ φi ⇒ ⊥}m
i=1 ,
we check the judgment def (H); ∅; Ai ∅◦ ; φi ⊢ ⊥ is derivable by the

dom(σ) = fvs(A′ ) ∪ fvs(e
t)
′
|= φ ⇒ JσA
n ⊆AKo
D; Γ; A ∪ P◦∅ (σe
t) ; φ ⊢ h

D; Γ; A; φ ⊢ h

(F OLD)

Check if the current knowledge entails the asserted proposition:
q
y
|= φ ⇒ P (e
t)∈A
|= φ ⇒ ⊥
(VALID⊥)
(VALIDP )
D; Γ; A; φ ⊢ ⊥
D; Γ; A; φ ⊢ P (e
t)

Auxiliary functions:
q
y
P (e
t)∈A ,
q

_

P (te′ )∈A

e
t=e
t′

J•∈AK , ⊤
n
oz
y r
α ⊲ P (e
t)∈A , P (e
t)∈ P M (te′ ) ∈ A | α ∈ M
^ q
y
P (e
t)∈A2
JA1 ⊆A2 K ,
P (te)∈A1

Figure 3. The inference rules for the judgment D; Γ; A; φ ⊢ h.

set {(g1 , A1 , φ1 , h1 ), . . . , (gm , Am , φm , hm )} consisting of userspecified lemmas and induction hypotheses, where gi is either • or
α ⊲ P (e
t). (•, A, φ, h) ∈ Γ represents the user-specified lemma
∀e
x.

^


A ∧ φ ⇒ h where {e
x} = fvs(A, φ, h),

8

2016/10/24

5. Implementation and Preliminary Experiments

inductive proof system. Here, each atom in Ai is initially annotated
with ∅ and ◦.
We now prove the correctness of our method, which follows
from the soundness of the inductive proof system. To state the
soundness, we first define JΓ, AKk , which represents the conjunction of user-specified lemmas and induction hypotheses in Γ instantiated for the atoms occurring in the k-times unfolding of A.
JΓ, AK0 = JΓK (A),

JΓ, AKk+1 = JΓK (A) ∧
where D(P )(e
t) =
′

Wm

^

m
_

M (t
e)∈A i=1
Pα

∃xei . (φi ∧
^
[

i=1

JΓK (A ) =


r
zk 
∪{α}
,
∃xei . φi ∧ Γ, Ai M
◦

V

(g,A,φ,h)∈Γ

Ai ) and JΓK is defined by:

J(g, A, φ, h)K (A′ ),

n
o
^
J(•, A, φ, h)K (A ) = ∀e
x.
A ∧ φ ⇒ h {e
x} = fvs(A, φ, h) ,
′

q
y
(α ⊲ P (e
t), A, φ, h) (A′ ) =

^
∀e
x.
A∧φ∧e
t=e
t′ ⇒ h

P M (e
t′ ) ∈ A′ , α ∈ M,
{e
x} = fvs(e
t, A, φ, h)



.

Intuitively, JΓK (A) represents the conjunction of user-specified
lemmas and induction hypotheses in Γ instantiated for the atoms
in A. The soundness of the inductive proof system is now stated by
the following lemma (see Appendix A for a proof).
Lemma 1 (Soundness). If D; Γ; A;
V φ ⊢ h is derivable, then there
is k such that µFD |= JΓ, AKk ∧ A ∧ φ ⇒ h holds.
The correctness of our Horn constraint solving method follows
immediately from Lemma 1 and Corollary 1 as follows.

We have implemented a Horn constraint solver based on the proposed method and integrated it, as a backend solver, with an existing verification tool called Refinement Caml [52–54], a refinement type checking and inference tool for the OCaml functional
language based on Horn constraint solving. Our solver can generate
a proof tree like the one in Figure 2 as a certificate, if the given Horn
constraint set is judged to have a solution. Furthermore, our solver
can generate a counterexample, if the constraint set is judged to
be unsolvable. We adopted Z3 [19] as the underlying SMT solver.
The details of the implementation are explained in Section 5.1. The
web interface of the verification tool as well as all the benchmark
programs used in the experiments reported here are available from
http://www.cs.tsukuba.ac.jp/~ uhiro/.
We have tested our constraint solver on two benchmark sets.
The first set is 85 benchmarks from the test suite for automated
induction provided by the authors of the IsaPlanner system [21].
The benchmark set consists of verification problems of relational
specifications of pure mathematical functions on inductive data
structures, most of which cannot be verified by the previous Horn
constraint solvers [25, 26, 31, 41, 46, 50, 53, 54]. The benchmark
set has also been used to evaluate previous automated inductive
theorem provers [15, 40, 44, 48]. The experiment results on this
benchmark set are reported in Section 5.2.
To demonstrate advantages of our novel combination of Horn
constraint solving with inductive theorem proving, we have prepared the second benchmark set consisting of verification problems
of (mostly relational) specifications of programs that use various
advanced language features, which are naturally and automatically
axiomatized by our method using predicates defined by Horn clause
constraints as the least satisfying interpretation. The experiment results on this benchmark set are reported in Section 5.3.
5.1 Implementation Details

Theorem
2. Suppose that H is an HCCS with goal (H) =
V
{ Ai ∧ φi ⇒ ⊥}m
i=1 . It then follows that ρ |= H for some ρ
if def (H); ∅; Ai ; φi ⊢ ⊥ is derivable for all i = 1, . . . , m.

This section describes details of the implementation. We explain
how to check the correctness of user specified lemmas and how
to generate a counterexample if the given Horn constraint set has
no solution, respectively in Sections 5.1.1 and 5.1.2. Section 5.1.3
describes implementation details of the rules A PPLY⊥, A PPLYP ,
and F OLD in Figure 3. In particular, we discuss how to find an
assignment σ for free term variables that occur in the element of Γ
selected by the rules.

Proof. Suppose that def (H); ∅; Ai ; φi ⊢ ⊥V
for all i = 1, . . . , m.
By Lemma 1 andVthe fact that µFdef (H) |= Ai ⇒ J∅, Ai Kk , we
get µFdef (H) |= Ai ∧ φi ⇒ ⊥. We therefore have µFdef (H) |=
goal (H). It then follows that ρ |= H for some ρ by Corollary 1.

5.1.1 Checking the correctness of user-specified lemmas
Our system allows users to specify lemmas as the initial Γ. Our
tool checks that D; ∅; A; φ ⊢ h is derivable for each user-specified
lemma (•, A, φ, h) by using the exact same rules in Figure 3. We
use the rule F OLD, in addition to the rules A PPLY⊥ and A PPLYP ,
to update the current knowledge. To avoid redundant applications
of F OLD, we select only definite clauses in D with the head of the
form P (e
t′ ) if h = P (e
t) and we do not use F OLD at all if h = ⊥.

4.2 Rule Application Strategy
We now elaborate on our rule application strategy shown in Section 2. Because all the inference rules except VALID⊥ and VALIDP
add new knowledge to A and/or φ, we repeatedly apply them until
VALID⊥ and VALIDP close all the proof branches under consideration. More specifically, we adopt the following strategy:

5.1.2 Counterexample generation

• Repeatedly apply the rules A PPLY⊥, A PPLYP , and F OLD if

Our tool can conclude that the goal clause (or the user-specified
lemma) currently solving has no solution if a subgoal of the form
D; Γ; A; φ ⊢ ⊥ satisfying the following conditions is obtained:

possible until no new knowledge is obtained. (Even if the
rules do not apply, applications of I NDUCT and U NFOLD explained in the following items may make A PPLY⊥, A PPLYP ,
and F OLD applicable.)

• all the atoms in A are already unfolded by the rule U NFOLD but

• If the current knowledge cannot be updated by using the above

• φ is satisfiable.

rules, select some atom from A in a breadth-first manner, and
apply the rule I NDUCT to the atom.

Note that the first condition ensures that the φ-part of the current
knowledge under-approximates the body of the goal clause.
Our tool then returns a satisfying model of φ found by the underlying SMT solver as a counterexample witnessing the unsolvability
of the given Horn constraint set. Some readers may notice that the

• Apply the rule U NFOLD whenever I NDUCT is applied.
• Try to apply the rules VALID⊥ and VALIDP whenever the

current knowledge is updated.

9

2016/10/24

counterexample generation is essentially the same as the execution
of constraint logic programs [33].

extended with induction [44] are reported to have proved 80. In
contrast to our Horn-clause-based method, these inductive theorem
provers can be, and in fact are directly applied to prove the conjectures in the benchmark set, because the benchmark set contains
only pure total functions over inductively-defined data structures.
It is also worth noting that, all the inductive provers that won
best results (greater than 70) on the benchmark set support automatic lemma discovery, in a stark contrast to our tool. For example,
the above result (80 out of 85) of CVC4 is obtained when they enable an automatic lemma discovery technique proposed in [44] and
use a different encoding (called dti in [44]) of natural numbers than
ours. When they disable the lemma discovery technique and use a
similar encoding to ours (called dtt in [44]), 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 [13, 15, 32, 36, 44, 48],
further makes induction-based Horn constraint solving powerful.

5.1.3 Finding an assignment σ for quantifier instantiation
We here explain how to find σ for instantiating quantified variables
of lemmas and induction hypotheses by using an SMT solver in the
implementation of the rule A PPLY⊥. The same technique is also
used for finding σ in the rules F OLD and A PPLYP .
Recall that, in order to apply the rule A PPLY⊥ to a judgment
D; Γ; A; φ ⊢ h, we need to find an assignment σ for free term
variables in (g, A′ , φ′ , h′ ) ∈ Γ. Note here that the atom that occurs
in g also occurs in A′ . We below assume that all the arguments
of the atoms in A′ are distinct term variables. This does not lose
generality because we can always replace P (e
t) ∈ A′ by P (e
x)
with fresh x
e by adding the constraint x
e
=e
t to φ′ . First of all, we
m
construct, for each P (e
x) ∈ A′ , the set x
e 7→ e
ti i=1 of assignments, where
P (e
t1 ), . . . , P (e
tm ) ∈ A. Here, if g = α ⊲ P (e
x),

m
e
the set
x
e 7→ ti i=1 of assignments is constructed only from
P M1 (e
t1 ), . . . , P Mm (e
tm ) ∈ A such that α ∈ Mi . For example,
let us consider
x1 ), A′ = {P
x1 ), P1 (e
x2 ), P2 (e
x3 )}
o1 (e
n g = α ⊲ P1 (e
∅ e
{α} e
t3 ) . For the atoms P1 (e
x1 ),
(t1 ), P1 (t2 ), P2 ∅ (e
and A = P1

P1 (e
x2 ), and P2 (e
x3 ), we respectively obtain the sets x
e1 7→ e
t1 ,

of assignments. We
{{e
x2 7→ e
t1 }, {e
x2 7→ e
t2 }}, and x
e3 7→ e
t3
then compute all the combination of assignments, and filter out
those that contradict with φ. For the above example, we obtain the
following two as candidates of σ:

σ1 = x
e1 7→ e
t1 , x
e2 7→ e
t1 , x
e3 7→ e
t3

e
e
e
σ2 = x
e1 7→ t1 , x
e2 7→ t2 , x
e3 7→ t3

5.3 Experiments on benchmark set consisting of programs
with various advanced language features
We prepared and tested our tool with the second benchmark set
consisting of (mostly relational) assertion safety verification problems of programs that use various advanced language features such
as partial (i.e., possibly non-terminating) functions, higher-order
functions, exceptions, non-determinism, algebraic data types, 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 four (ID19–22 in Table 1) are relational ones where
safe inductive invariants are not expressible in QF LIA, and therefore not solvable by the previous Horn constraint solvers. As shown
in Section 3.3, these verification problems are naturally and automatically axiomatized by our method using predicates defined
by Horn clause constraints as the least satisfying interpretation.
By contrast, these assertion safety verification problems cannot
be straightforwardly axiomatized and proved by the previous automated inductive theorem provers based on logics of pure total
functions on inductively-defined data structures: the axiomatization
process of these verification problems using pure total functions often requires users’ manual intervention and possibly causes a negative effect on the automation of induction, because, in the process,
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.
Additionally, the axiomatization process needs to preserve branching and calling context information in order to perform path- and
context-sensitive verification.
Table 1 summarizes the experiment results on the benchmark
set. The column “specification” represents the relational specification verified and the column “kind” shows the kind of the specification, 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 “language features” shows the language features used in the verification problem,
where each character has the following meaning.

For the rules F OLD and A PPLYP , we use the same technique
explained above for A PPLY⊥, but additionally check the condition
|= φ ⇒ ∃e
x. σφ′ , where {e
x} = fvs(φ′ ) \ dom(σ).

5.2 Experiments on IsaPlanner benchmark set
The IsaPlanner benchmark set consists of 85 conjectures for total
recursive functions on inductively defined data structures such as
natural numbers, lists, and binary trees. We have translated these
conjectures into assertion safety verification problems of OCaml
programs. In the translation, we encoded natural numbers using
integer primitives, and defined lists and binary trees as algebraic
data types in OCaml. More specifically, natural numbers Z and S t
are respectively encoded as 0 and t′ + 1 for t′ obtained by encoding
t. To preserve the semantics of natural numbers, we translated
conjectures of the form ∀x ∈ N. φ into ∀x ∈ Z. (x ≥ 0 ⇒ φ).
The translated verification problems are then verified by our verification tool. Our tool automatically reduced the verification problems into Horn constraint solving problems by using the constraint
generation method [53], and automatically (i.e., without using userspecified lemmas) solved 68 out of 85 verification problems. We
have manually analyzed the experiment results and found that 8
out of 17 failed verification problems require lemma discovery. The
other 9 problems caused timeout of Z3. It was because the rule application strategy implemented in our tool caused useless detours
in proofs and put heavier burden on Z3 than necessary.
The experiment results on the IsaPlanner benchmark set show
that our Horn-clause-based axiomatization of total recursive functions does not cause significant negative impacts on the automation
of induction; According to [48] that uses the IsaPlanner benchmark set to compare state-of-the-art automated inductive theorem
provers based on logics of pure total functions over inductivelydefined data structures, IsaPlanner [21] proved 47 out of 85,
Dafny [40] proved 45, ACL2s [13] proved 74, and Zeno [48] proved
82. The HipSpec [15] inductive prover and the SMT solver CVC4

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

10

2016/10/24

Table 1. Experiment results on programs that use various language features
specification
kind
language features result time (sec.)
mult x y + a = mult acc x y a
equiv
P
✓
0.257
mult x y = mult acc x y 0
equiv
P
✓†
0.435
mult (1 + x) y = y + mult x y
equiv
P
✓
0.233
y ≥ 0 ⇒ mult x (1 + y) = x + mult x y
equiv
P
✓
0.248
mult x y = mult y x
comm
P
✓‡
0.345
mult (x + y) z = mult x z + mult y z
dist
P
✓
1.276
mult x (y + z) = mult x y + mult x z
dist
P
✗
n/a
mult (mult x y) z = mult x (mult y z)
assoc
P
✗
n/a
0 ≤ x1 ≤ x2 ∧ 0 ≤ y1 ≤ y2 ⇒ mult x1 y1 ≤ mult x2 y2
mono
P
✓
0.265
sum x + a = sum acc x a
equiv
✓
0.384
sum x = x + sum (x − 1)
equiv
✓
0.272
x ≤ y ⇒ sum x ≤ sum y
mono
✓
0.350
x ≥ 0 ⇒ sum x = sum down 0 x
equiv
P
✓
0.312
x < 0 ⇒ sum x = sum up x 0
equiv
P
✓
0.368
sum down x y = sum up x y
equiv
P
✗
n/a
sum x = apply sum x
equiv
H
✓
0.286
mult x y = apply2 mult x y
equiv
H, P
✓
0.279
repeat x (add x) a y = a + mult x y
equiv
H, P
✓
0.317
x ≤ 101 ⇒ mc91 x = 91
nonrel
I
✓
0.165
x ≥ 0 ∧ y ≥ 0 ⇒ ack x y > y
nonrel
I
✓
0.212
x ≥ 0 ⇒ 2 × sum x = x × (x + 1)
nonrel
N
✓
0.196
dyn sys 0. −→
/ ∗ assert false
nonrel
R,N
✓
0.144
flip mod y x = flip mod y (flip mod y x)
idem
P
✓
7.712
noninter h1 l1 l2 l3 = noninter h2 l1 l2 l3
nonint
P
✓
0.662
try find opt p l = Some (find p l) with
Not Found → find opt p l = None
equiv
H, E
✓
0.758
26 try mem (find ((=) x) l) l with Not Found → ¬(mem x l) equiv
H, E
✓
0.764
27 sum list l = fold left (+) 0 l
equiv
H
✓
3.681
28 sum list l = fold right (+) l 0
equiv
H
✓
0.329
29 sum fun randpos n > 0
equiv
H,D
✓
0.240
30 mult x y = mult Ccode(x, y)
equiv
P, C
✓
0.217
†
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
Pf above represents the predicate that axiomatizes the function f .
The experiments were conducted on a machine with Intel(R) Xeon(R) CPU E5-2680 v3 (2.50 GHz, 16 GB of memory).
ID
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

obtained from the specification mult x (y + z) = mult x y +
mult x z into

N: nonlinear functions
C: procedures written in different programming paradigms

Pmult (y+z, x, s1 )∧Pmult (y, x, s2 )∧Pmult (z, x, s3 ) ⇒ s1 = s2 +s3

The column “result” represents whether our verification method
succeeded ✓or failed ✗. The column “time” represents the elapsed
time for verification in seconds.
Overall, the experiment results are promising, which show that
our tool can automatically 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 recureses on x and the other recurses
on y. Thus, the result demonstrates an advantage of our inductionbased method that it can exploit lemmas to fill the gap between
function calls with different control flows. Our tool, however, failed
to verify the distributivity ID7 of mult, the associativity ID8 of
mult, and the equivalence ID15 of sum down and sum up. ID7
could be reduced to ID6 and solved, if a lemma Pmult (x, y, r) ⇒
Pmult (y, x, r), which represents the commutativity of mult, was
used to rewrite the conjecture

by replacing atoms of the form Pmult (t1 , t2 , t3 ) with Pmult (t2 , t1 , t3 ).
The rule A PPLY P, however, replaces each atom Pmult (t1 , t2 , t3 )
with Pmult (t1 , t2 , t3 ) ∧ Pmult (t2 , t1 , t3 ) instead by keeping the
original atom so that we can monotonically increase the current
knowledge. Our tool supports an option for the rule A PPLY P of
eliminating the original atom, and if it is enabled, ID7 is verified.
The associativity verification problem ID8 is even more difficult.
In addition to the above lemma, a lemma Pmult (x + y, z, r) ⇒
∃s1 , s2 .(Pmult (x, z, s1 )∧Pmult (y, z, s2 )∧r = s1 +s2 ) is required.
This lemma, however, is currently not of the form supported by
our inductive proof system. In ID15, the functions sum down and
sum up use different recursion parameters (resp. y and x), and requires lemmas Psum down (x, y, s) ⇒ ∃s1 , s2 .(Psum down (0, y, s1 ) ∧
Psum down (0, x − 1, s2 ) ∧ s = s1 − s2 ) and Psum up (x, y, s) ⇒
∃s1 , s2 .(Psum down (0, y, s1 ) ∧ Psum down (0, 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 proof system does not support the form of the
lemmas. To put it differently, ID8 and ID15 demonstrate the in-

Pmult (x, y+z, s1 )∧Pmult (x, y, s2 )∧Pmult (x, z, s3 ) ⇒ s1 = s2 +s3

11

2016/10/24

the target language, which is complex compared to the logical semantics of Horn clause constraints.
There have been proposed program logics for relational verification [5, 6, 14, 24]. 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 is, however, not automated.

completeness of our inductive proof system. Our future work thus
includes an extension of the proof system to support more general
form of lemmas and judgments.

6. Related Work
As discussed in Section 1, Horn constraint solving methods have
been extensively studied [25, 26, 31, 41, 46, 50, 53, 54]. In contrast
to the proposed induction based method, these methods do not
support Horn clause constraints over the theories of algebraic data
structures and nonlinear arithmetics, and cannot verify most if not
all relational specifications shown in Section 5.
Because state-of-the-art SMT solvers such as Z3 [19] and CVC4
support quantifier instantiation heuristics, one may think that they
alone are sufficient for checking the validity of the logical interpretation of Horn clause constraints shown in Section 3.1. However,
they alone are not sufficient for proving most conjectures that require nontrivial use of induction such as the benchmark problems
in Section 5.3 In fact, [44] reports that Z3 (resp. CVC4 without induction) alone have proved only 35 (resp. 34) out of 85 problems
in the IsaPlanner benchmark set.
Automated inductive theorem proving techniques and tools
have long been studied, for example and to name a few: the BoyerMoore theorem provers [36] like ACL2s [13], rewriting induction
provers [43] like SPIKE [9], proof planners like CLAM [11, 12, 32,
34] and IsaPlanner [20, 21], and SMT-based induction provers like
Leon [49], Dafny [40], Zeno [48], HipSpec [15], and CVC4 [44].
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 (e.g., ones discussed in Section 3.3) 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 a partial 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 [49] are
used in the axiomatization). We have also confirmed that CVC4
failed to verify complex integer functions like the McCarthy 91
and the Ackermann functions (resp. ID19 and ID20 in Table 1).
By contrast, our method supports advanced language features and
specifications via Horn-clause encoding of their semantics based on
program logics such as Hoare logics and refinement type systems.
To aid verification of relational specifications of functional programs, Giesl [23] proposed context-moving transformations and
Asada et al. [1] proposed a kind of tupling transformation. SymDiff [30, 39] is a transformation-based tool built on top of Boogie [2] for equivalence verification of imperative programs. Selfcomposition [3] is a program transformation technique to reduce ksafety [16, 51] verification into ordinary safety verification, and has
been applied to non-interference [4, 51, 55] and regression verification [22] of imperative programs. These transformations are useful
for some patterns of relational verification problems, which are,
however, less flexible than our approach based on a more general
principle of induction. For example, Asada et al.’s transformation
enables verification of the functional equivalence of recursive functions with the same recursion pattern (e.g., ID1 in Table 1), but does
not help verification of the commutativity of mult (ID5 in Table 1).
Because each transformation is designed for a particular target language, the transformations cannot be applied to aid relational verification across programs written in different paradigms (e.g., ID30
in Table 1). Moreover, the correctness proof of the transformations
tends to be harder because it involves the operational semantics of
3 This

point is also mentioned in the
(http://rise4fun.com/Z3/tutorial/guide ).

tutorial

of

7. Conclusion and Future Work
We have proposed a novel Horn constraint solving method based
on an inductive proof system and an SMT-based technique to automate proof search in the system. We have shown that our method is
able to solve Horn clause constraints obtained from relational verification problems that were not possible with the previous methods
based on interpolating theorem proving. 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 to support more general form of lemmas and judgments.
We are also planning to extend our proof search method to support automatic lemma discovery as in the state-of-the-art inductive
theorem provers [13, 15, 44, 48]. To aid users to better understand
verification results of our method, it is important to generate a symbolic representation of a solution of the original Horn constraint set
from the found inductive proof. It is however often the case that a
solution of Horn constraint sets that require relational analysis (e.g.,
Hmult ) is not expressible by a formula of the underlying logic. It
therefore seems fruitful to generate a symbolic representation of
mutual summaries in the sense of [30] across multiple predicates
(e.g., P, Q of Hmult ).

References
[1] 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.
[2] 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.
[3] G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by
self-composition. In CSFW ’04, pages 100–114. IEEE, 2004.
[4] G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using
product programs. In FM ’11, pages 200–214. Springer, 2011.
[5] 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.
[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 and differential privacy. In POPL ’15, pages 55–
68. ACM, 2015.
[7] T. A. Beyene, C. Popeea, and A. Rybalchenko. Solving existentially
quantified horn clauses. In CAV ’13, volume 8044 of LNCS, pages
869–882. Springer, 2013.
[8] F. Bobot, J.-C. Filliâtre, C. Marché, and A. Paskevich. Why3: Shepherd your herd of 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] A. Bundy. The automation of proof by mathematical induction. In
Handbook of Automated Reasoning, volume I, pages 845–911. Elsevier, 2001.

Z3

12

2016/10/24

[12] A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The oyster-clam
system. In CADE-10, pages 647–648. Springer, 1990.

[36] M. Kaufmann, J. S. Moore, and P. Manolios. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.

[13] 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.

[37] K. Knowles and C. Flanagan. Type reconstruction for general refinement types. In ESOP ’07, volume 4421 of LNCS, pages 505–519.
Springer, 2007.

[14] Ş. Ciobâcă, D. Lucanu, V. Rusu, and G. Roşu. A languageindependent proof system for mutual program equivalence. In ICFEM
’14, pages 75–90. Springer, 2014.

[38] S. Kupferschmid and B. Becker. Craig interpolation in the presence
of non-linear constraints. In FORMATS ’11, pages 240–255. Springer,
2011.

[15] 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.

[39] S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebêlo. SYMDIFF: A language-agnostic semantic diff tool for imperative programs.
In CAV ’12, pages 712–717. Springer, 2012.

[16] M. R. Clarkson and F. B. Schneider. Hyperproperties. In CSF ’08,
pages 51–65. IEEE, 2008.

[40] K. R. M. Leino. Automating induction with an SMT solver. In VMCAI
’12, volume 7148 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, 2013.

[17] 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.

[42] K. L. McMillan. An interpolating theorem prover. Theoretical Computer Science, 345(1):101–121, 2005.

[18] W. Craig. Three uses of the Herbrand-Gentzen theorem in relating
model theory and proof theory. Journal of Symbolic Logic, 22:269–
285, 1957.
[19] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS
’08, volume 4963 of LNCS, pages 337–340. Springer, 2008.

[43] U. S. Reddy. Term rewriting induction. In CADE-10, volume 449 of
LNCS, pages 162–177. Springer, 1990.
[44] A. Reynolds and V. Kuncak. Induction for SMT solvers. In VMCAI
’15, volume 8931 of LNCS, pages 80–98. Springer, 2015.

[20] L. Dixon and J. Fleuriot. Higher order rippling in IsaPlanner. In
TPHOLs ’04, pages 83–98. Springer, 2004.

[45] P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI ’08,
pages 159–169. ACM, 2008.

[21] 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.

[46] P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for
horn-clause verification. In CAV ’13, volume 8044 of LNCS, pages
347–363. Springer, 2013.

[22] D. Felsing, S. Grebing, V. Klebanov, P. Rümmer, and M. Ulbrich.
Automating regression verification. In ASE ’14, pages 349–360. ACM,
2014.

[25] S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko.
Synthesizing software verifiers from proof rules. In PLDI ’12, pages
405–416. ACM, 2012.

[47] R. Sato, H. Unno, and N. Kobayashi. Towards a scalable software
model checker for higher-order programs. In PEPM ’13, pages 53–
62. ACM, 2013.
[48] 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, March 2012.
[49] 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.
[50] T. Terauchi. Dependent types from counterexamples. In POPL ’10,
pages 119–130. ACM, 2010.

[26] 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.

[51] T. Terauchi and A. Aiken. Secure information flow as a safety problem. In SAS ’05, volume 3672 of LNCS, pages 352–367. Springer,
2005.

[27] A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and
refinement for verifying multi-threaded programs. In POPL ’11, pages
331–344. ACM, 2011.

[52] H. Unno and N. Kobayashi. On-demand refinement of dependent
types. In FLOPS ’08, volume 4989 of LNCS, pages 81–96. Springer,
2008.

[28] A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas. The SeaHorn verification framework. In CAV ’15, pages 343–361. Springer,
2015.

[53] H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP ’09, pages 277–288. ACM, 2009.
[54] 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.
[55] H. Unno, N. Kobayashi, and A. Yonezawa. Combining type-based
analysis and model checking for finding counterexamples against noninterference. In PLAS ’06, pages 17–26. ACM, 2006.
[56] 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.
[57] H. Xi and F. Pfenning. Dependent types in practical programming. In
POPL ’99, pages 214–227. ACM, 1999.

[23] J. Giesl. Context-moving transformations for function verification. In
LOPSTR ’00, volume 1817 of LNCS, pages 293–312. Springer, 2000.
[24] B. Godlin and O. Strichman. Regression verification: proving the
equivalence of similar programs. Software Testing, Verification and
Reliability, 23(3):241–258, 2013.

[29] K. Hashimoto and H. Unno. Refinement type inference via horn
constraint optimization. In SAS ’15, volume 9291 of LNCS, pages
199–216. Springer, 2015.
[30] C. Hawblitzel, M. Kawaguchi, S. K. Lahiri, and H. Rebêlo. Towards
modularly comparing programs using automated theorem provers. In
CADE-24, pages 282–299. Springer, 2013.
[31] 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.
[32] A. Ireland and A. Bundy. Productive use of failure in inductive proof.
Journal of Automated Reasoning, 16(1-2):79–111, 1996.
[33] J. Jaffar and M. J. Maher. Constraint logic programming: a survey.
The Journal of Logic Programming, 19:503 – 581, 1994.
[34] M. Johansson, L. Dixon, and A. Bundy. Case-analysis for rippling and
inductive proof. In ITP ’10, volume 6172 of LNCS, pages 291–306.
Springer, 2010.
[35] T. Kahsai, P. Rümmer, H. Sanchez, and M. Schäf. JayHorn: A framework for verifying Java programs. In CAV ’16. Springer, 2016.

13

2016/10/24

Lemma 8. Suppose that P◦M (e
t) ∈ A and α does not occur in Γ
or A. We then obtain
n
ozk
r
⇒
t), A, φ, h) , PαM (e
t)
|= JΓ, AKk ∧ (α ⊲ P (e
r
n
ozk

Γ ∪ (α ⊲ P (e
t), A, φ, h) , (A \ P◦M (e
t)) ∪ PαM (e
t)

A. Proof of Lemma 1
We first show lemmas used to prove Lemma 1.
q
y
V
Lemma 2. |= φ ⇒ P (e
t)∈A implies |= A ∧ φ ⇒ P (e
t).
q
y
Proof. By the definition of P (e
t)∈A .

Lemma 3. |= φ ⇒ JA1 ⊆A2 K implies |=

V

A2 ∧ φ ⇒

Proof. By the definition of JA1 ⊆A2 K and Lemma 2.

V

Proof. By the definition of J•, •K• , we get
q
yk
|= JΓ, AKk ∧ (α ⊲ P (e
t), A, φ, h) , A ∧
n
ozk
r n
ozk r
⇒
t), A, φ, h) , PαM (e
t)
∧ (α ⊲ P (e
Γ, PαM (e
t)
r
n
ozk

Γ ∪ (α ⊲ P (e
t), A, φ, h) , (A \ P◦M (e
t)) ∪ PαM (e
t)

A1 .

Lemma 4. Suppose that (g, A′ , φ′ , h) ∈ Γ and |= φ ⇒ Jσg∈AK
for some σ with dom(σ)
= fvs(A′ ) ∪ fvs(h). It then follows
V
that |= JΓK (A) ∧ σA′ ∧ φ ⇒ (σh ∨ ∀e
x.¬(σφ′ )), where
′
{e
x} = fvs(φ ) \ dom(σ).

Because α does not occur in Γ or A and P◦M (e
t) ∈ A, we obtain
n
ozk
r
⇒
t), A, φ, h) , PαM (e
t)
|= JΓ, AKk ∧ (α ⊲ P (e
r
n
ozk

Γ ∪ (α ⊲ P (e
t), A, φ, h) , (A \ P◦M (e
t)) ∪ PαM (e
t)

Proof. We perform a case analysis on g.
• Suppose that g = •. By the definition of JΓK (A), we obtain

|= JΓK (A) ⇒ ∀e
x′ .

^


A ′ ∧ φ′ ⇒ h ,

where {e
x′ } = fvs(A′ ) ∪ fvs(φ′ ) ∪ fvs(h). Therefore, we get
^
|= JΓK (A) ⇒
σA′ ∧ ∃e
x.(σφ′ ) ⇒ σh,

Because µFD is the least interpretation, we obtain:
Lemma 9. For all P ∈ pvs(D) and ψ with fvs(ψ) ⊆ {e
x}, we get

where {e
x} = fvs(φ′ ) \ dom(σ). It immediately follows that
^
|= JΓK (A) ∧
σA′ ∧ φ ⇒ (σh ∨ ∀e
x.¬(σφ′ )).

µFD |= ∀e
x. ({P 7→ λe
x.ψ} D(P )(e
x) ⇒ ψ) ⇒ ∀e
x.(P (e
x) ⇒ ψ)
Lemma 10. For all P ∈ pvs(D) and ϕ with fvs(ϕ) ⊆ {e
x}, we
get

• Suppose that g = α ⊲ P (e
t). We assume that φ is not equivalent

µFD |= ∀e
x. ((∀p ≺ P. {P 7→ λe
x.ϕ} p(e
x)) ⇒ ϕ) ⇒ ∀e
x.(P (e
x) ⇒ ϕ),

to ⊥ (otherwise, the lemma is trivial). By |= φ ⇒ Jσg∈AK,
there is P M (e
t′ ) ∈ A such that α ∈ M and |= φ ⇒ σe
t=e
t′ .
By the definition of JΓK (A), we obtain

^
A ′ ∧ φ′ ∧ e
t=e
t′ ⇒ h ,
|= JΓK (A) ⇒ ∀e
x′ .

Proof. By Lemma 9 with ψ = ∀p  P. {P 7→ λe
x.ϕ} p(e
x).

where {e
x} = fvs(φ′ ) \ dom(σ). We thus obtain
^
|= JΓK (A) ∧
σA′ ∧ φ ⇒ (σh ∨ ∀e
x.¬(σφ′ )).

Proof. By Lemma 10.

where p ≺ P is a predicate obtained by unfolding P at least once.

Lemma 11. Suppose that P ∈ pvs(D), P◦M (e
t) ∈ A, α does not
occur in A, and the following holds
n
ozk ^
r
∧
A∧φ⇒ h
t), A, φ, h) , PαM (e
t)
µFD |= (α ⊲ P (e
V
It then follows that µFD |= A ∧ φ ⇒ h.

where {e
x′ } = fvs(e
t) ∪ fvs(A′ ) ∪ fvs(φ′ ) ∪ fvs(h). Therefore,
we get
^
|= JΓK (A) ⇒
σA′ ∧ ∃e
x.(σφ′ ) ∧ σe
t=e
t′ ⇒ σh,

We now prove Lemma 1.

Lemma 5. if k1 ≤ k2 , then |= JΓ, AKk2 ⇒ JΓ, AKk1 holds.

Proof of Lemma 1. By induction on the derivation of D; Γ; A; φ ⊢
h.

•

Proof. By the definition of J•, •K .
Lemma 6. We have
µFD

• Case I NDUCT: We have

P◦M (e
t) ∈ A,

Γ′ = Γ ∪ (α ⊲ P (e
t), A, φ, h) ,
D; Γ′ ; A′ ; φ ⊢ h,

A′ = (A \ P◦M (e
t)) ∪ PαM (e
t) , and
α is fresh.
By I.H., there is k′ such that
q
yk′ ^ ′
µFD |= Γ′ , A′
∧
A ∧φ⇒h

r

n
ozk
.
|= JΓ, AKk ∧ P (e
t) ⇒ Γ, A ∪ P◦∅ (e
t)

Proof. By the definition of J•, •K• .

Lemma 7. If PαM (e
t) ∈ A, then for each i ∈ {1, . . . , m},

m
r
zk 
_
∪{α}
∃xei . φi ∧ Γ, A ∪ Ai M
,
µFD |= JΓ, AKk+1 ⇒
◦

By Lemma 8, we get
r
n
ozk′
∧
µFD |= (α ⊲ P (e
t), A, φ, h) , PαM (e
t)
^ ′
′
A ∧ φ ∧ JΓ, AKk ⇒ h

i=1

where D(P )(e
t) =

Wm

i=1

∃xei . (φi ∧

Proof. By the definition of J•, •K• .

V

Ai ).

14

2016/10/24

By the fact |= A ⇔ A′ and the definition of J•, •K• , we get
rn
o n
ozk′
′
∧
µFD |= (α ⊲ P (e
t), A, φ ∧ JΓ, AKk , h) , PαM (e
t)
^
k′
A ∧ φ ∧ JΓ, AK ⇒ h

|= φ ⇒ JσA′ ⊆AK,
′
{e
x} = fvs(φ
n ) \ dom(σ),
o
D; Γ; A ∪ P◦∅ (σe
t) ; φ ⊢ h

By (g, A′ , φ′ , P (e
t)) ∈ Γ, |= φ ⇒ Jσg∈AK, and Lemmas 4
and 5, for some k1 , we get
^
|= JΓ, AKk1 ∧
σA′ ∧ φ ∧ ∃e
x.(σφ′ ) ⇒ P (σe
t)

Therefore, by Lemma 11, for k = k′ , we get
^
µFD |= JΓ, AKk ∧
A∧φ ⇒h

• Case U NFOLD: For each i ∈ {1, . . . , m}, we have

PαM (e
t) ∈ A,
W
V
D(P )(e
t) = m
ei . (φi ∧ Ai ), and
i=1 ∃x
M ∪{α}
D; Γ; A ∪ Ai ◦
; φ ∧ φi ⊢ h.
By I.H., for each i ∈ {1, . . . , m}, there is ki such that
r
z ki ^ 

∪{α}
∪{α}
µFD |= Γ, A ∪ Ai M
∧
A ∪ Ai M
∧φ∧φi ⇒ h
◦
◦
It then follows immediately that
^
µFD |= A ∧ φ∧

m 
r
zki ^
_
∪{α}
M ∪{α}
⇒h
φi ∧ Γ, A ∪ Ai M
∧
A
i
◦
◦

′

where k =
µFD

+1

⇒

m
_

i=1

max {ki }m
i=1 .

By Lemma 6, we obtain

r
n
ozk2
µFD |= JΓ, AKk2 ∧ P (σe
t) ⇒ Γ, A ∪ P◦∅ (σe
t)
µFD |= JΓ, AKk2 ∧

i=1

′

By I.H., there is k2 such that
r
n
ozk2 ^ 
n
o
∧
µFD |= Γ, A ∪ P◦∅ (σe
t)
A ∪ P◦∅ (σe
t) ∧φ ⇒ h

It then follows that

^

n
o
A ∪ P◦∅ (σe
t)
∧φ⇒h

Therefore, for k = max(k1 , k2 ), by Lemma 5, we get
^
µFD |= JΓ, AKk ∧
A∧φ⇒h

By Lemma 7, we get
µFD |= JΓ, AKk

Then, by |= φ ⇒ JσA′ ⊆AK, Lemma 3, and |= φ ⇒ ∃e
x.(σφ′ ),
we get
^
|= JΓ, AKk1 ∧
A ∧ φ ⇒ P (σe
t)


r
zk ′ 
∪{α}
,
∃xei . φi ∧ Γ, A ∪ Ai M
◦

• Case F OLD: We have

V 
P (e
t) ⇐ φ′ ∧ A′ ∈ D,
dom(σ) = fvs(A′ ) ∪ fvs(e
t),
|= φ ⇒ ∃e
x.(σφ′ ),
|= φ ⇒ JσA′ ⊆AK,
′
{e
x} = fvs(φ
n ) \ dom(σ),
o
D; Γ; A ∪ P◦∅ (σe
t) ; φ ⊢ h
V
By P (e
t) ⇐ φ′ ∧ A′ ∈ D, dom(σ) = fvs(A′ ) ∪ fvs(e
t), and
′
{e
x} = fvs(φ ) \ dom(σ), we obtain
^
µFD |=
σA′ ∧ ∃e
x.(σφ′ ) ⇒ P (σe
t)

Therefore, by Lemma 5, we obtain
!
m 
^
_
^ 
′
|= JΓ, AKk +1 ∧
A∧φ∧
⇒h
φi ∧
Ai
i=1

W
V
From the facts µFD |= P (e
t) ⇔ m
ei . (φi ∧ Ai ) and
i=1 ∃x
M e
′
Pα (t) ∈ A, for k = k + 1, we get
^
µFD |= JΓ, AKk ∧
A ∧ φ ⇒ h.

• Case A PPLY⊥: We have

(g, A′ , φ′ , ⊥) ∈ Γ,
dom(σ) = fvs(A′ ),
|= φ ⇒ Jσg∈AK,
|= φ ⇒ JσA′ ⊆AK,
{e
x} = fvs(φ′ ) \ dom(σ), and
D; Γ; A; φ ∧ ∀e
x.¬(σφ′ ) ⊢ h.
′
′
By (g, A , φ , ⊥) ∈ Γ, |= φ ⇒ Jσg∈AK, and Lemmas 4 and 5,
for some k1 , we get
^
|= JΓ, AKk1 ∧
σA′ ∧ φ ⇒ ∀e
x.¬(σφ′ )

By |= φ ⇒ JσA′ ⊆AK, Lemma 3, and |= φ ⇒ ∃e
x.(σφ′ ), we
get
^
µFD |=
A ∧ φ ⇒ P (σe
t)

By I.H., there is k′ such that
n
o
r
n
ozk′ ^ 
∧
A ∪ P◦∅ (σe
t) ∧φ ⇒ h
µFD |= Γ, A ∪ P◦∅ (σe
t)
By Lemma 6, we obtain

r
n
ozk′
′
µFD |= JΓ, AKk ∧ P (σe
t) ⇒ Γ, A ∪ P◦∅ (σe
t)

By |= φ ⇒ JσA′ ⊆AK and Lemma 3, we obtain
^
|= JΓ, AKk1 ∧
A ∧ φ ⇒ ∀e
x.¬(σφ′ )

It then follows that

′

µFD |= JΓ, AKk ∧

By I.H., there is k2 such that
^
µFD |= JΓ, AKk2 ∧
A ∧ φ ∧ ∀e
x.¬(σφ′ ) ⇒ h

^

n
o
A ∪ P◦∅ (σe
t)
∧φ⇒h

Therefore, for k = k′ , we obtain

µFD |= JΓ, AKk ∧

Therefore, for k = max(k1 , k2 ), by Lemma 5, we obtain
^
µFD |= JΓ, AKk ∧
A ∧ φ ⇒ h.

^

A∧φ⇒h

• Case VALID⊥: We have h = ⊥ and |= φ ⇒ ⊥. Therefore,

V
µFD |= JΓ, AKk ∧ A ∧ φ ⇒ h holds for any k.
q
y
• Case VALIDP : We have h = P (e
t) and |= φ ⇒ P (e
t)∈A .
V
By lemma 2, we getV|= A ∧ φ ⇒ P (e
t). It then follows that
µFD |= JΓ, AKk ∧ A ∧ φ ⇒ P (e
t) for any k.

• Case A PPLYP : We have

(g, A′ , φ′ , P (e
t)) ∈ Γ,
dom(σ) = fvs(A′ ) ∪ fvs(e
t),
|= φ ⇒ Jσg∈AK,
|= φ ⇒ ∃e
x.(σφ′ ),
15

2016/10/24

