日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

Automating Well-Founded Inductionfor Horn Clause Solving
Sho Torii

Hiroshi Unno

Verification problems of programs in various paradigms (e.g., imperative, functional, and concurrent) canbe reduced to constraint solving problems of Horn clauses over predicate variables that represent unknown
inductive invariants to be inferred. This paper presents a novel constraint solving method based on inductive
theorem proving. The main advantage of the proposed method over existing methods is that it can verify relational specifications (e.g., the equivalence, associativity, commutativity, distributivity, monotonicity,idempotency, and non-interference) where multiple function calls need to be analyzed simultaneously. Our
novel combination with Horn-clause-based verification extends the reach of induction-based verification frompure total functions to impure partial programs in various paradigms with diﬀerent evaluation strategies.
The proposed method automates well-founded induction for integers by finding well-founded orders with aranking function synthesizer and discharging proof obligations with an SMT solver.

of specifications includes practically important ones

Summarysuch as the equivalence, associativity, commutativ-Verification problems of programs in various

ity, distributivity, monotonicity, idempotency, andparadigms including imperative, functional, andconcurrent can be reduced to constraint solving

non-interference.
For example, consider the following functional

problems of Horn clauses over predicate variables

program Dmult (in OCaml syntax).

that represent unknown inductive invariants to be

let rec mult x y =inferred [1, 2, 9, 13, 14]. An input program is guaranteed to satisfy a given specification if the constraints generated from the program have a solution.

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 =This paper presents a novel Horn constraint solv-assert (mult x y + a = mult_acc x y a)

ing method based on inductive theorem proving.

Here, the function mult takes two arguments x,

The main advantage of the proposed method overy and recursively computes x × y. mult acc is aprevious constraint solving methods based on inter-

tail-recursive version of mult with an accumulator

polation [1, 3, 4, 6, 10–12, 14, 15] is that it can ver-a. The function main contains an assertion with

ify relational specifications where multiple function

the condition mult x y + a = mult_acc x y a,calls need to be analyzed simultaneously. The classwhich represents a relational specification, namely,
the equivalence of mult and mult acc. By using ex-

ホーン節制約解消のための整礎帰納法自動化
This is an unrefereed paper. Copyrights belong tothe Author(s).

isting Horn constraint generation methods for call-鳥居 翔

tional verification problem is reduced to the con-

海野 広志, 筑波大学, University of Tsukuba.

by-value functional programs [9, 13, 14], the rela-straint solving problem of the following Horn clause
constraint
set Hmult .
 P (x, y, 0) ⇐ y ≤ 0,











P(x,y,x+r)⇐P(x,y−1,r)∧y>0,Q(x, y, a, a) ⇐ y ≤ 0,




Q(x,y,a,r)⇐Q(x,y−1,a+x,r)∧y>0,
 r + a = r ⇐ P (x, y, r ) ∧ Q(x, y, a, r )12
12Here, 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, y, 0) ⇐ y ≤0 ∈ Hmult is generated from the then-branch of thedefinition of mult and expresses that mult returns
0 if 0 is given as the second argument. The second clause P (x, y, x + r) ⇐ P (x, y − 1, r) ∧ y >0 ∈ Hmult is generated from the else-branch andrepresents 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 elsebranches 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, it is guaranteed that the evaluationof main x y never causes an assertion failure for any
input x and y.
The previous Horn constraint solving methods [1,3, 4, 6, 10–12, 14, 15], however, cannot solve thiskind of constraints that require a relational analysis of multiple predicates. To see why, recall theconstraint r1 +a = r2 ⇐ P (x, y, r1 )∧Q(x, y, a, r2 ) ∈Hmult that asserts the equivalence of mult andmult acc, where a relational analysis of the two
predicates P and Q is required.

The previousmethods, however, analyze each predicate P andQ separately, and therefore must infer nonlinear
invariants r1 = x × y and r2 = x × y + a respectively for the predicate applications P (x, y, r1 ) andQ(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 ) and Q(x, y, a, r2 ). Furthermore, the previous methods can only find solutions that are expressible by some eﬃciently decidable theories such as the quantifier-free linear real(QF LRA) and integer (QF LIA) arithmetic (seehttp://smt-lib.org/ for the definition of the theories), which are not powerful enough to express theabove nonlinear invariants and the solution θmult ofHmult .
By contrast, our new Horn constraint solving
method based on inductive theorem proving can directly infer the mutual invariant r1 +a = r2 to showthat Hmult is solvable by simultaneously unfolding
and analyzing the predicate applications P (x, y, r1 )and Q(x, y, a, r2 ).

More precisely, our method

applies well-founded induction to prove the goal
clause ∀x, y, r1 , a, r2 . P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ⇒r1 + a = r2 in Hmult where P, Q are interpreted as the predicates inductively defined as
the least models of the definite clauses in Hmult .
If we are given a well-founded relation ≺mult ={((x′ , y ′ , r1′ , a′ , r2′ ), (x, y, r1 , a, r2 )) | 0 ≤ y ′ < y}for the universally-quantified integer variables, theproof proceeds as follows.
P (x, y, r1 ) ∧ Q(x, y, a, r2 ) ⇒ r1 + a = r2
Case1. P (x, y, 0) ⇐ y ≤ 0⇐⇒ r1 = 0 ∧ y ≤ 0 ∧ Q(x, y, a, r2 ) ⇒ r1 + a = r2
Case1-1. Q(x, y, a, a) ⇐ y ≤ 0⇐⇒ r1 = 0 ∧ y ≤ 0 ∧ r2 = a ⇒ r1 + a = r2⇐⇒ ⊤Case1-2. Q(x, y, a, r) ⇐ Q(x, y − 1, a + x, r) ∧ y > 0⇐⇒ r1 = 0 ∧ y ≤ 0 ∧ Q(x, y − 1, a + x, r2 ) ∧ y > 0⇒ r1 + a = r2⇐⇒ ⊤Case2. P (x, y, x + r) ⇐ P (x, y − 1, r) ∧ y > 0⇐⇒ P (x, y − 1, r1 − x) ∧ y > 0 ∧ Q(x, y, a, r2 )⇒ r1 + a = r2
Case2-1. Q(x, y, a, a) ⇐ y ≤ 0⇐⇒ P (x, y − 1, r1 − x) ∧ y > 0 ∧ r2 = a ∧ y ≤ 0⇒ r1 + a = r2

(i.e., (n + 11, s) and (s, r)) of R that recursively
occurs in the body. Formally, TR is defined by thefollowing
constraint set.
T((n,r), (n + 11, s)) R

Case2-2. Q(x, y, a, r) ⇐ Q(x, y − 1, a + x, r) ∧ y > 0⇐ R(n + 11, s) ∧ R(s, r) ∧ n ≤ 100, ⇐⇒ P (x, y − 1, r1 − x) ∧ y > 0 ∧ Q(x, y − 1, a + x, r2 )





 TR ((n, r), (s, r))⇒ r1 + a = r2
⇐ R(n + 11, s) ∧ R(s, r) ∧ n ≤ 100 (induction hypothesis)
 We then apply existing ranking function synthe∀(x′ , y ′ , r1′ , a′ , r2′ ) ≺mult (x, y, r1 , a, r2 ).
 sizers [5, 7, 8] to find a ranking function f thatP (x′ , y ′ , r1′ ) ∧ Q(x′ , y ′ , a′ , r2′ ) ⇒ r1′ + a′ = r2′
witnesses the well-foundedness of TR . Formally,⇐⇒ y > 0 ∧ r1 − x + a + x = r2 ⇒ r1 + a = r2
we find f such that TR ⊆ {((n′ , r′ ), (n, r)) |⇐⇒ ⊤⇐⇒ ⊤0 ≤ f (n′ , r′ ) < f (n, r)} and obtain, for example,

The reasoning above is automated by the state-of-fmc91 (n, r) = 111 − n. By using the synthesized

the-art SMT provers.

well-founded relation ≺mc91 = {(n′ , r′ ), (n, r) | 0 ≤The remaining question is how to get an appro-

111 − n′ < 111 − n}, the proof of the goal clausepriate well-founded relation for induction. To this∀n, r. R(n, r) ∧ n ≤ 101 ⇒ r = 91 in Hmc91 pro-end, we propose a technique to synthesize a well-ceeds as follows.

founded relation for induction from the definition ofpredicates using existing ranking function synthe-R(n, r) ∧ n ≤ 101 ⇒ r = 91

sizers [5, 7, 8], which are originally developed for

Case1. R(n, n − 10) ⇐ n > 100

termination verification of programs. For exam-⇐⇒ r = n − 10 ∧ n ≤ 101 ∧ n > 100 ⇒ r = 91

ple, consider the following McCarthy 91 function⇐⇒ ⊤Dmc91 .

Case2. R(n, r) ⇐ R(n + 11, s) ∧ R(s, r) ∧ n ≤ 100

let rec mc91 n =⇐⇒ R(n + 11, s) ∧ R(s, r) ∧ n ≤ 100 ∧ n ≤ 101

if n > 100 then n - 10else mc91 (mc91 (n + 11))
let main n =if n <= 101 then assert (mc91 n = 91)⇒ r = 91(induction hypothesis)[]∀(n′ , r′ ) ≺mc91 (n, r). R(n′ , r′ ) ∧ n′ ≤ 101 ⇒ r′ = 91⇐⇒ ((s, r) ≺mc91 (n, r) ⇒ s ≤ 101 ⇒ r = 91)

The assertion expresses the well-known property of∧ R(n + 11, s) ∧ n ≤ 100

the function mc91: for any input n ≤ 101, mc91 n⇒ r = 91

always returns 91. From the program, we obtainthe following Horn clause constraint set Hmc91 . 
 R(n, n − 10) ⇐ n > 100,
R(n, r) ⇐ R(n + 11, s) ∧ R(s, r) ∧ n ≤ 100,r = 91 ⇐ R(n, r) ∧ n ≤ 101
Our method then synthesizes a well-founded relation for induction from the definition of the predicate R as follows. First, we introduce the transition relation TR that relates the argument (n, r)
of R in the head of the definite clause R(n, r) ⇐R(n + 11, s) ∧ R(s, r) ∧ n ≤ 100 ∈ Hmc91 with those⇐⇒ (s > n ⇒ s ≤ 101 ⇒ r = 91)∧ ((n + 11, s) ≺mc91 (n, r) ⇒ n ≤ 90 ⇒ s = 91)∧ R(n + 11, s) ∧ n ≤ 100⇒ r = 91
Case2-1. R(n, n − 10) ⇐ n > 100⇐⇒ (s > n ⇒ s ≤ 101 ⇒ r = 91)∧ (n ≤ 90 ⇒ s = 91)∧ s = n + 1 ∧ n > 89 ∧ n ≤ 100⇒ r = 91⇐⇒ ⊤Case2-2. R(n, r) ⇐ R(n + 11, s) ∧ R(s, r) ∧ n ≤ 100⇐⇒ (s > n ⇒ s ≤ 101 ⇒ r = 91)∧ (n ≤ 90 ⇒ s = 91)∧ R(n + 22, s′ ) ∧ R(s′ , s) ∧ n ≤ 89 ∧ n ≤ 100⇒ r = 91⇐⇒ ⊤References[ 1 ] Grebenshchikov, S., Lopes, N. P., Popeea, C.,
and Rybalchenko, A.: Synthesizing Software Verifiers from Proof Rules, PLDI ’12, ACM, 2012,
pp. 405–416.
[ 2 ] Gupta, A., Popeea, C., and Rybalchenko, A.:
Predicate Abstraction and Refinement for Verifying
Multi-threaded Programs, POPL ’11, ACM, 2011,
pp. 331–344.
[ 3 ] Gupta, A., Popeea, C., and Rybalchenko, A.:
Solving recursion-free horn clauses over LI+UIF,APLAS ’11, LNCS, Vol. 7078, Springer, 2011,
pp. 188–203.
[ 4 ] Hoder, K., Bjørner, N., and Moura, L. D.: µZ:
An Eﬃcient Engine for Fixed Points with Constraints, CAV ’11, LNCS, Vol. 6806, Springer, 2011,
pp. 457–462.
[ 5 ] Kuwahara, T., Terauchi, T., Unno, H., andKobayashi, N.: Automatic Termination Verificationfor Higher-Order Functional Programs, ESOP ’14,
LNCS, Vol. 8410, Springer, 2014, pp. 392–411.

[ 6 ] McMillan, K. and Rybalchenko, A.: Computing
Relational Fixed Points using Interpolation, Technical Report MSR-TR-2013-6, 2013.
[ 7 ] Podelski, A. and Rybalchenko, A.: A Complete
Method for the Synthesis of Linear Ranking Functions, VMCAI ’04, LNCS, Vol. 2937, Springer, 2004,
pp. 239–251.
[ 8 ] Popeea, C. and Rybalchenko, A.: Compositional Termination Proofs for Multi-threaded Programs, TACAS ’12, LNCS, Vol. 7214, Springer,
2012, pp. 237–251.
[ 9 ] Rondon, P., Kawaguchi, M., and Jhala, R.: Liquid Types, PLDI ’08, ACM, 2008, pp. 159–169.
[10] Rümmer, P., Hojjat, H., and Kuncak, V.:
Disjunctive Interpolants for Horn-Clause Verification, CAV ’13, LNCS, Vol. 8044, Springer, 2013,
pp. 347–363.
[11] Terauchi, T.: Dependent types from counterexamples, POPL ’10, ACM, 2010, pp. 119–130.
[12] Terauchi, T. and Unno, H.: Relaxed Stratification: A New Approach to Practical Complete
Predicate Refinement, ESOP ’15, LNCS, Vol. 9032,Springer, 2015, pp. 610–633.
[13] Unno, H. and Kobayashi, N.: On-Demand Refinement of Dependent Types, FLOPS ’08, LNCS,Vol. 4989, Springer, 2008, pp. 81–96.
[14] Unno, H. and Kobayashi, N.: Dependent Type
Inference with Interpolants, PPDP ’09, ACM, 2009,
pp. 277–288.
[15] Unno, H. and Terauchi, T.: Inferring Simple
Solutions to Recursion-free Horn Clauses via Sampling, TACAS ’15, LNCS, Vol. 9035, Springer, 2015,
pp. 149–163.