Automating Induction
for Solving Horn Clauses
Hiroshi Unno, Sho Torii, and Hiroki Sakamoto
University of Tsukuba, Japan

2017/7/28

Computer Aided Verification 20171

Program Verification via
Horn Constraint Solving
Verification Problems of Programs in
Various Paradigms (e.g., functional [U.+ ’08, ’09, Rondon+ ’08, …],procedural [Grebenshchikov+ ’12, Gurfinkel+ ’15], object-oriented[Kahsai+ ’16], multi-threaded [Gupta+ ’11], constraint logic) with
Advanced Language Features (e.g., algebraic data structures,
linked data structures, exceptions, higher-order functions) withSide-Effects (e.g., non-termination, non-determinism, concurrency,assertions, destructive updates)

ReduceHorn Constraint Solving Problems
2017/7/28

Computer Aided Verification 20172

Overall Flow of Horn Constraint
based Program Verification
Program & Specification
Constraint Generation(* OCaml *)/* C */
let rec mult x y =int mult(int x, int y) {if y = 0 then 0
int s Set= 0;
Horn Constraint
else x + mult x (y - 1)
while(y != 0){s += x;{- Haskell -}Constraint Solving
𝑃𝑃y--;𝑥𝑥, 𝑦𝑦, 𝑟𝑟 ≡ 𝑟𝑟 = 𝑥𝑥 × 𝑦𝑦
mult :: Int -> Int -> Int}
mult x 0 = 0
return s;
Solutionor Counterexample
mult x y = x + multx (y - 1)}
2017/7/28
Computer Aided Verification 20173

This Work

Horn Constratint Solving

Horn Constraint Set
Constraint Solving

ReduceSolvable or Not

InductiveTheorem Proving
SMT Solving• Enable verification of relational specifications acrossprograms in various paradigms• Support constraints over any background theories(if the backend SMT solver does)
2017/7/28

Computer Aided Verification 20174

Relational Specifications• Specifications that involve multiple function calls• Equivalence• Invertibility• Non-interference• Associativity• Commutativity• Distributivity• Monotonicity• Idempotency•…

2017/7/28

Computer Aided Verification 20175

Overall Flow of Horn Constraint
based Program Verification(Functional) Program &Relational Specification
Constraint Generation
Horn Constraint Set
Constraint Solving
Solvable or Not
2017/7/28

Computer Aided Verification 20176

Example: (Functional) Programand Relational Specification(* recursive function to compute “x × y” *)let rec mult x y =if y = 0 then 0 else x + mult x (y - 1)(* tail recursive function to compute “x × y + a” *)let rec mult_acc x y a =if y = 0 then a else mult_acc x (y - 1) (a + x)(* functional equivalence of mult and mult_acc *)let main x y a = assert (mult x y + a = mult_acc x y a)
2017/7/28

Computer Aided Verification 20177

Overall Flow of Horn Constraint
based Program Verification(Functional) Program &Relational Specification
Constraint Generation
Horn Constraint Set
Constraint Solving
Solvable or Not
2017/7/28

Computer Aided Verification 20178

Horn Constraint Generation [U.+ ’09]
let rec mult x y =if y = 0 then 0else x + mult x (y - 1)
let rec mult_acc x y a =if y = 0 then aelse mult_acc x (y - 1) (a + x)

2017/7/28

let main x y a =assert (mult x y + a= mult_acc x y a)Computer Aided Verification 20179

Overall Flow of Horn Constraint
based Program Verification(Functional) Program &Relational Specification
Constraint Generation
Horn Constraint Set
Constraint Solving
Solvable or Not
2017/7/28

Computer Aided Verification 201710

Horn Constraint Solving• Check the existence of a solution for predicate
variables satisfying all the Horn constraints• If a solution exists, the original program isguaranteed to satisfy the specification

Example (Non-relational) specification:
let main x y = if x >= 0 && y >= 0 then assert (mult x y >= 0)

Solution 1: 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑟𝑟 ≡ 𝑥𝑥 ≥ 0 ∧ 𝑦𝑦 ≥ 0 ⇒ 𝑟𝑟 ≥ 0
Solution 2: 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑟𝑟 ≡ 𝑟𝑟 = 𝑥𝑥 × 𝑦𝑦
Nonlinear
QF-NIA
2017/7/28

Computer Aided Verification 2017

QF-LIA11

Previous Methods for Solving Horn
Clause Constraints [U.+ ’08,’09, Rondon+ ’08,

Gupta+ ’11, Hoder+ ’11,’12, McMillan+ ’13, Rümmer+ ’13, …]Find a solution expressible in QF-LIA (or QF-LRA)

Solution 1: 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑟𝑟 ≡ 𝑥𝑥 ≥ 0 ∧ 𝑦𝑦 ≥ 0 ⇒ 𝑟𝑟 ≥ 0
Solution 2: 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑟𝑟 ≡ 𝑟𝑟 = 𝑥𝑥 × 𝑦𝑦
2017/7/28

Computer Aided Verification 2017

QF-LIA

QF-NIA
12

Example Constraints that Can Not
be Solved by Previous Methods
Constraint
Solving Fails!

QF-NIA

Analyzed
Analyzed
separately from 𝑄𝑄 separately from 𝑃𝑃

𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ≡ 𝑠𝑠1 = 𝑥𝑥 × 𝑦𝑦

2017/7/28

𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2 ≡ 𝑠𝑠2 = 𝑥𝑥 × 𝑦𝑦 + 𝑎𝑎

Computer Aided Verification 201713

Our Constraint Solving Method
Horn Constraint Set
Constraint Solving

ReduceInductiveTheorem Proving

Solvable or Not
Simultaneously analyze
multiple predicates byexpressing and exploiting
mutual invariants
2017/7/28

Computer Aided Verification 201714

Reduction from Constraint Solving
to Inductive Theorem Proving
𝑃𝑃 𝑥𝑥, 0,0 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑥𝑥 + 𝑟𝑟 ⇐ 𝑃𝑃 𝑥𝑥, 𝑦𝑦 − 1, 𝑟𝑟 ∧ 𝑦𝑦 ≠ 0
𝑄𝑄 𝑥𝑥, 0, 𝑎𝑎, 𝑎𝑎 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑟𝑟 ⇐ 𝑄𝑄 𝑥𝑥, 𝑦𝑦 − 1, 𝑎𝑎 + 𝑥𝑥, 𝑟𝑟 ∧ 𝑦𝑦 ≠ 0𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2 ⇐ 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧ 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2

Prove this byinduction onderivation of𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ,Q x, y, s2∀𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 , 𝑎𝑎, 𝑠𝑠2 . 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧ 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2 ⇒ 𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2
2017/7/28

Computer Aided Verification 201715

Principle of Induction on Derivation∀𝐷𝐷. 𝜓𝜓 𝐷𝐷 if and only if∀𝐷𝐷. ∀𝐷𝐷′ . 𝐷𝐷 ′ ≺ 𝐷𝐷 ⇒ 𝜓𝜓 𝐷𝐷′ ⇒ 𝜓𝜓 𝐷𝐷
where 𝐷𝐷′ ≺ 𝐷𝐷 represents that
𝐷𝐷′ is a strict sub-derivation of 𝐷𝐷

𝐷𝐷 =2017/7/28

𝐷𝐷1𝐽𝐽3

𝐽𝐽2𝐷𝐷2𝐽𝐽1

𝐷𝐷3𝐷𝐷4𝐽𝐽4Computer Aided Verification 2017

Assume𝜓𝜓 𝐷𝐷1 , 𝜓𝜓 𝐷𝐷2 ,𝜓𝜓 𝐷𝐷3 , 𝜓𝜓 𝐷𝐷4and prove 𝜓𝜓 𝐷𝐷16

Horn Constraint Solving:

InductionTheorem
hypotheses
and lemmas
InductiveProving:

Judgment∅; 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 , 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2 ⊢ 𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2
Premises

2017/7/28

Computer Aided Verification 201717

Add an induction hypothesis:Guard to avoid unsound application∀𝑥𝑥 ′ , 𝑦𝑦 ′ , 𝑠𝑠1′ , 𝑎𝑎′ , 𝑠𝑠2′ . 𝐷𝐷 𝑃𝑃 𝑥𝑥 ′ , 𝑦𝑦 ′ , 𝑠𝑠1′ ≺ 𝐷𝐷 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧𝛾𝛾 =𝑃𝑃 𝑥𝑥′, 𝑦𝑦′, 𝑠𝑠1 ′ ∧ 𝑄𝑄 𝑥𝑥 ′ , 𝑦𝑦 ′ , 𝑎𝑎′ , 𝑠𝑠2′ ⇒ 𝑠𝑠1 ′ + 𝑎𝑎′ = 𝑠𝑠2 ′Induct2017/7/28

Unfold Case analysis on the last rule used

Computer Aided Verification 201718

2017/7/28

Computer Aided Verification 201719

Case analysis on the last rule used
Unfold2017/7/28

Computer Aided Verification 201720

2017/7/28

Computer Aided Verification 2017

21

Validity checking
Valid2017/7/28

Computer Aided Verification 201722

2017/7/28

Computer Aided Verification 201723

Valid2017/7/28

Computer Aided Verification 201724

2017/7/28

Computer Aided Verification 201725

Unfold

2017/7/28

Case analysis on the last rule usedComputer Aided Verification 201726

2017/7/28

Computer Aided Verification 201727

Valid2017/7/28

Computer Aided Verification 201728

2017/7/28

Computer Aided Verification 201729

′ ′ ′′ , 𝑦𝑦 ′ , 𝑠𝑠 ′∀𝑥𝑥,𝑎𝑎,𝑠𝑠.
𝐷𝐷𝑃𝑃𝑥𝑥∧ ∧𝐷𝐷 𝑃𝑃′ , 𝑦𝑦
𝑥𝑥,′𝑦𝑦, 𝑠𝑠−1,𝑠𝑠−𝑥𝑥≺
𝐷𝐷
𝑃𝑃 𝑥𝑥, 𝑦𝑦,1 𝑠𝑠1 ≺∧𝐷𝐷𝑃𝑃 𝑃𝑃𝑥𝑥, 𝑦𝑦𝑥𝑥,−𝑦𝑦,1,𝑠𝑠𝑠𝑠11 − 𝑥𝑥
11 2𝜎𝜎 𝛾𝛾𝛾𝛾 ==𝑄𝑄 𝑦𝑦′,𝑥𝑥, 𝑦𝑦𝑠𝑠1−′ 1,∧𝑎𝑎𝑄𝑄+ 𝑥𝑥,+ 𝑎𝑎′𝑥𝑥) == 𝑠𝑠𝑠𝑠22 ′𝑃𝑃 𝑥𝑥′,𝑥𝑥 ′𝑠𝑠,2𝑦𝑦 ′⇒, 𝑎𝑎′ 𝑠𝑠, 1𝑠𝑠2′− 𝑥𝑥⇒+𝑠𝑠1(𝑎𝑎′ +IndHyp Apply induction hypothesis

2017/7/28

Computer Aided Verification 201730

Valid2017/7/28

Computer Aided Verification 2017

QED31

Properties of Inductive Proof System
for Horn Constraint Solving• Soundness: If the goal is proved, the original Hornconstraints have a solution (which may not be
expressible in the underlying logic)• Relative Completeness: If the original constraints
have a solution expressible in the underlying logic,
the goal is provable

2017/7/28

Computer Aided Verification 201732

Automating Induction• Use the following rule application strategy:• Repeatedly apply INDHYP until no new premises are added• Apply VALID whenever a new premise is added• Select some 𝑃𝑃 𝑡𝑡̃ and apply INDUCT and UNFOLD• Close a proof branch by using:• SMT solvers: provide efficient and powerful reasoning aboutdata structures (e.g., integers, reals, algebraic data structures)
but predicates are abstracted as uninterpreted functions• Horn constraint solvers: provide bit costly but powerfulreasoning about inductive predicates2017/7/28

Computer Aided Verification 201733

Prototype Constraint Solver• Use Z3 and 𝝁𝝁Z PDR engine respectively
as the backend SMT and Horn constraint solvers• Integrated with a refinement type based verification
tool RCaml for the OCaml functional language• Can exploit lemmas which are:• User-supplied,• Heuristically obtained from the given constraints, or• Automatically generated by an abstract interpreter• Can generate a counterexample (if any)
2017/7/28

Computer Aided Verification 201734

Experiments on IsaPlanner
Benchmark Set• 85 (mostly) relational verification problems of
total functions on inductively defined data structures
Inductive Theorem Prover#Successfully ProvedRCaml68
Zeno
82 [Sonnex+ ’12]
Support automatic
HipSpec
80 [Claessen+ ’13]
lemma discovery &CVC4
goal generalization 80 [Reynolds+ ’15]
ACL2s
74 (according to [Sonnex+ ’12])
IsaPlanner
47 (according to [Sonnex+ ’12])
2017/7/28
Computer Aided Verification 45
2017 (according to [Sonnex+ ’12])
35
Dafny

Experiments on Benchmark Programs with
Advanced Language Features & Side-Effects• 30 (mostly) relational verification problems for:• Complex integer functions: Ackermann, McCarthy91• Nonlinear real functions: dyn_sys• Higher-order functions: fold_left, fold_right, repeat, find, ...
• Exceptions: find
• Non-terminating functions: mult, sum, …
• Non-deterministic functions: randpos• Imperative procedures: mult_Ccode

2017/7/28

Computer Aided Verification 201736

• 28 (2 required lemmas) successfully proved by RCaml• 3 proved by Horn constraint solver 𝝁𝝁Z PDR• 2 proved by inductive theorem prover CVC4 (if inductivepredicates are encoded using uninterpreted functions)

2017/7/28

Computer Aided Verification 201737

Conclusion• Proposed an automated verification method combining
Horn constraint solving and inductive theorem proving• Enable relational verification across programs in various
paradigms with advanced language features and side-effects• Support constraints over any background theories(if the backend SMT solver does)• Future and ongoing work:• Automatic lemma discovery and goal generalization• Relational program synthesis• Coinduction
2017/7/28

Computer Aided Verification 201738