A Horn Constraint Solver
based on Inductive Theorem Proving

Hiroki Sakamoto

Sho Torii

Shu Nakao

Background(University of Tsukuba)

Our Horn Constraint Solver (Demo Available!)

Verification problems of programs in various paradigms
imperative, logic, concurrent, functional, ...
can be reduced to Horn constraint solving problems

Approach : Inductive theorem proving
1. Reduce Horn constaint solving problems into validity checkingof first-order formulas with inductively defined predicates, thenVerification Problem

let rec mult x y =if y=0 then 0 else x + mult x (y - 1)

2. Check by induction on the derivation of the predicates

Automation of inductive proofs(1) A new proof system tailored to Horn constraint solving

let rec mult_acc x y a =if y=0 then aelse mult_acc x (y - 1) (a + x)

(2) Discharge proof obligations arising in the proof search using
・PDR-based Horn constraint solver, and・SMT solver∀x,y,a.(mult x y)+a = (mult_acc x y a)(3) Exploit lemmas, which arereduce

Horn Constraint Solving Problemℋ𝑚𝑢𝑙𝑡P(x,0,0).
P(x,y,x+r) :- P(x,y-1,r) ∧ y≠0.
Q(x,0,a,a).
Q(x,y,a,r) :- Q(x,y-1,a+x,r) ∧ y≠0.
Unknown
invariant of mult

Hiroshi Unno

・User-supplied,・Heuristically obtained from the given constraints, or・Automatically generated by an abstract interpreter

Advantages
Our method can(1) deal with constraints over any background theories
supported by the underlying SMT solver

Unknown
invariant of mult_acc(2) enable verification of relational specifications acrossprograms in various paradigms functional equivalence, associativity,P(x,y,r1) ∧ Q(x,y,a,r2) |= r1+a=r2
Is there a substitution for P and Q
that satisfies all the constraints?

commutativity, monotonicity, …

(3) enable verification of recursive functions that are possibly
non-deterministic, higher-order, exception-raising, and over
non-inductively defined data types

Applications

1. Verif. of higher-order programs

P(Nil,0). P(Cons(x,l'),x+r) :- P(…).
R(…). R(…) :- …
P(l,r1) ∧ R(0,l,r2) |= r1=r2⊨ 𝑦 ≠ 0 ∧ 𝑟1 − 𝑥 + 𝑎 + 𝑥 = 𝑟2 ⇒ 𝑟1 + 𝑎 = 𝑟2

𝜙; 𝐶 ∧ 𝑦 ≠ 0 ∧ (𝑟1 − 𝑥) + 𝑎 + 𝑥 = 𝑟2 ⊢ 𝑟1 + 𝑎 = 𝑟2…

reduceExample : Inductive Proof for ℋ𝑚𝑢𝑙𝑡…

type list = Nil | Cons of int * list
let rec sum_list l = match l with
| Nil -> 0 | Cons(x,xs) -> x + sum_list xs
let rec foldl f s l = match l with
| Nil -> s | Cons(x,xs) -> foldl f (f s x) xs
let plus x y = x + y∀l.sum_list l = foldl plus 0 lnonlinear arithmetics, algebraic
data structures, and heaps

𝜙; 𝐶 ∧ 𝑦 ≠ 0 ⊢ 𝑟1 + 𝑎 = 𝑟2

𝜙; 𝐴 ⊢ 𝑟1 + 𝑎 = 𝑟2
Induct𝐴 ⊢ 𝑟1 + 𝑎 = 𝑟2

prove

ApplyUnfold

𝜙; 𝐵 ∧ 𝑦 ≠ 0 ⊢ 𝑟1 + 𝑎 = 𝑟2
𝜙 = ∀𝑥 , 𝑦 , 𝑟1′ , 𝑟2′ . 𝑃 𝑥 ′ , 𝑦 ′ , 𝑟1′ ≺ 𝑃 𝑥, 𝑦, 𝑟1 ∧′′ ′ ′′ ′ ′ ′𝑃 𝑥 , 𝑦 , 𝑟1 ∧ 𝑄 𝑥 , 𝑦 , 𝑎 , 𝑟2 ⇒ 𝑟1 + 𝑎′ = 𝑟2 ′′Valid′

Unfold𝐴 = 𝑃 𝑥, 𝑦, 𝑟1 ∧ 𝑄 𝑥, 𝑦, 𝑎, 𝑟2
𝐵 = 𝐴 ∧ 𝑃 𝑥, 𝑦 − 1, 𝑟1 − 𝑥
𝐶 = 𝐵 ∧ 𝑄 𝑥, 𝑦 − 1, 𝑎 + 𝑥, 𝑟2

Spec. Satisfied!
3. Verif. of programs that may raise exceptions 4. Verif. of heap-manipulating programs
2. Verif. of user-defined ADTs
type list =Nil | Cons of int * list
let rec append l ys = …
let rec drop n l = …
let rec take n l = …
∀n,l.
append (take n l) (drop n l) = l
reduceP(Nil,l2,l2). P(…) :- ….
Q(…). Q(…) :- ….
R(…). R(…) :- ….
∀n,l. P(…) ∧ Q(…) ∧ R(…) |= r=l
prove

Spec. Satisfied!
5. Verif. of nonlinear spec.

let rec find p l = match l with| []->raise Not_found| x::xs->if p x then x else find p xs
let rec find_opt p l = match l with| [] -> None
| x::xs -> if p x then Some x else
find_opt p xs
∀p,l.
try find_opt p l = Some (find p l)with Not_found -> find_opt p l = None
reduce…
Pex(…,Not_found) ∧ Q(…,r2) |= None=r2
prove

Extensions

Spec. Satisfied!

(with Nam Mai and Tachio Terauchi)
let rec zero_list x = match !x with
| Nil->true| Cons(d,l)->if d=0 then zero_list l else false
let rec init_list x = match !x with
| Nil->() | Cons(d,l)->init_list l;x:=Cons(0,l)∀x. (init_list x) => (zero_list x)
reduceZero_list(h,x) :- h=(x |-> Nil) * h2.
Zero_list(h,x) :Zero_list(h',l), h=(x|->Cons(0,l))*h'.
Init_list(h,x,h) :- h=(x|->Nil)*h2.
Init_list(h,x,h') :- Init_list(h2,l,h3),
h=(x|->Cons(d,l))*h2, h'=(x|->Cons(0,l))*h3.
∀h,x,h'. Init_list(h,x,h') |= Zero_list(h',x)
prove

Spec. Satisfied!
let rec sum n =if n<0 then n + sum (n+1)
1.
Coinduction
oncopredicates(withSeiichShinomiya)
2. Relational program synthesis
else if n=0 then 0
merge(Cons(a,as),bs,Cons(a,cs)) :- merge(bs,as,cs). let rec mult x y = …
else n + sum (n-1)
let rec mult_acc x y a = ?
∀n. n>=0 => 2*sum n = n*(n+1) even(Cons(x1,Cons(x2,xs)),Cons(x1,ys))
reduceP(0,0). P(…) :- P(…) ∧ x<0.
p(x,r+x) :- P(x-1,r) ∧ x>0.
∀n.P(x,r)∧x>=0 |= 2*r=x*(x+1)
proveSpec. Satisfied!

:- even(xs,ys).
equal(Cons(l,ls),Cons(r,rs)) :- l=r,equal(ls,rs).
∀u,v,r1,r2.merge(u,v,r1),even(r1,r2) |= equal(r2,u)prove

Solvable!

∀x,y,a.(mult x y) + a= (mut_acc x y a)reduceHorn Constraint Abduction Problem
solve

Definition of mult_acc