### 2 - Microsoft Research

```Model Checking Software,
Solving Horn Clauses
Part I
Nikolaj Bjørner
Microsoft Research
VTSA,
Luxembourg, October 30-31, 2014
Takeaways
Symbolic Software Model Checking =
SMT for Horn Clauses
Simplification and pre-processing
A Solver using clues from IC3
An Algorithmic Overview (separate slides)
Horn Clauses
mc(x) = x-10
mc(x) = mc(mc(x+11))
if x > 100
if x  100
assert (x ≤  →mc(x) = 91)
∀.  >   mc(,  − )
∀, , .  ≤   mc( + , )  mc(, )  mc(, )
∀, . mc(, ) ∧  ≤  →  =
Solver finds solution for mc
[Hoder, B. SAT 2012]
Transition System
•
•
•
•
V
init(V)
step(V, V’)
safe(V)
- program variables
- initial states
- transition relation
- safe states
Safe Transition System
∃.
• ∀V . init(V) → (V)
• ∀V, V’ .  V ∧ step(V, V’) → (V′)
• ∀V . (V) →safe(V)
– [Rybalchenko et.al. PLDI 2012, POPL 2014]
Termination and reactivity are also handled in
framework of solving systems of logical formulas.
Recursive Procedures
Formulate as Horn clauses:
∀.  >   mc(,  − )
∀, , .  ≤   mc( + , )  mc(, )  mc(, )
∀, . mc(, ) ∧  ≥    =
Solve for mc
Recursive Procedures
Formulate as Predicate Transformer:
F
(mc)(,) =
> 100 ∧  =  − 10
∨  ≤ 100 ∧ ∃. mc  + 11,  ∧ mc(, )
Check: μF mc , ∧  ≥ 101 →  = 91
Recursive Procedures
Instead of computing μF mc , ,
then checking μF mc , ∧  ≤ 101 →  = 91
Suffices to find post-fixed point mc satisfying:
∀, .
F
mc ,  → mc ,
∀, . mc ,  ∧  ≤ 101 →  = 91
Program Verification as SMT
- aka
Program Verification (Safety)
as
Solving fixed-points
as
Satisfiability of Horn clauses
[Bjørner, McMillan, Rybalchenko, SMT workshop 2012]
Hilbert Sausage Factory: [Grebenshchikov, Lopes, Popeea, Rybalchenko, PLDI 2012]
Procedures  Horn Formulas
Summary as
commands
Verifying
procedure calls
Modular Concurrency  Horn Clauses
−
−
, , ′ ,  ′ −
,  −
,  ′ −     ′
⇒   ,
,  ∧   , , ′ ,  ′ ⇒  ′ ,  ′
,  ∧
,  ′
⇒
, ′
,  ∧   , , ′ ,  ′ ⇒  ,  ′
1 1 ∧ ⋯ ∧   ⇒
≠
[Predicate Abstraction and
Refinement for Verifying
Gupta, Popeea, Rybalchenko,
POPL 2011]
 Horn Clauses
Γ ⊢ :  ()} → :  (, ) } ≺ :  ′()} → :  ′(, ) }
Extract sufficient Horn Conditions
Γ ∧ ′  ⇒
Γ ∧ ′  ∧  ,  ⇒ ′ ,
Generalized Horn Formulas
Handling background axioms:
∀,  .  ,  ⇒ ∃
∀   ∧   ∧  , ,  ⇒
Remark:
Abductive Logic Programming amounts to symbolic simulation:
-  +  ⊨ ∃ . ()
-  +   is consistent
eg. solve for negation of above formula:
∃.   ∧ (∀ .  ,  → ∃ . (, , ))
Simplifying Horn Clauses
A model checking Example
Abstraction as Boolean Program
b := count == old_count
[SLAM, BLAST, Graf & Saidi, Uribe, ..]
(Predicate) Abstraction/Refinement
• SMT solver used to synthesize (strongest)
abstract transition relation F:
, ′ ⇒ (1  … ,   , 1 ′ … ,  ′ )
Control as Horn Clauses
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
Loop
; Loop without if test
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state) (WhileTest count count true))))
; Loop with if-test
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state) (WhileTest (+ 1 count ) count false))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (not (= old_count count )) (WhileTest count old_count lock_state))
(Loop count old_count lock_state))))
While
Test
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (= old_count count ) (WhileTest count old_count lock_state))
(= lock_state true))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(check-sat)
(get-model)
Solving Horn Clauses
Pre-processing
→ ′
Search
– Find model M such that  ⊨
Or
– Find refutation proof :  ⊢ ⊥
Pre-processing
•
•
•
•
•
•
Cone of Influence
Simplification
Subsumption
Inlining
Slicing
Unfolding
Cone of Influence – top down
∧   →
P  →
T  →
∧>→
∧<→
=  →
Q  ∧≤→
S is not used
S  ≔
Cone of Influence – bottom up
∧  , 0 →
∧>→
∧<→
=  →
There is no “rule
to produce Q(x,1)”
,  ≔  = 1
Q ,  ∧  ≤  →  ,
Inlining
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state) (WhileTest count count true))))
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= count count)))
(Loop count count true)))
; Loop without if test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
; Loop with if-test
(=> (and (Loop count old_count lock_state) (= count count))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(= true true)))
(=> (Loop count old_count lock_state) (WhileTest (+ 1 count ) count false))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (not (= old_count count )) (WhileTest count old_count lock_state))
(Loop count old_count lock_state))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (= old_count count ) (WhileTest count old_count lock_state))
(= lock_state true))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(check-sat)
(get-model)
; Loop with if-test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count ))
(Loop (+ 1 count) count false)))
; Loop with if-test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= (+ 1 count ) count )
(= false true)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(check-sat)
(get-model)
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
Simplification
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= count count)))
(Loop count count true)))
; Loop without if test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= count count))
(= truetrue)))
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
; Loop without if test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= true true)))
; Loop with if-test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count ))
; Loop with if-test + repeat loop
(Loop (+ 1 count) count false)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
; Loop with if-test + loop exit
(Loop (+ 1 count) count false)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= (+ 1 count ) count )
(= false true)))
; Loop with if-test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(check-sat)
(get-model)
(check-sat)
(get-model)
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
Simplification
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= count count)))
(Loop count count true)))
; Loop without if test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= count count))
(= truetrue)))
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
; Loop without if test + loop exit
; Loop with if-test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count ))
; Loop with if-test + repeat loop
(Loop (+ 1 count) count false)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
; Loop with if-test + loop exit
(Loop (+ 1 count) count false)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= (+ 1 count ) count )
(= false true)))
; Loop with if-test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count true)
false)))
(check-sat)
(get-model)
(check-sat)
(get-model)
Cone of Influence
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= count count)))
(Loop count count true)))
; Loop without if test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= count count))
(= truetrue)))
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
; Loop without if test + loop exit
; Loop with if-test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count ))
; Loop with if-test + repeat loop
(Loop (+ 1 count) count false)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
; Loop with if-test + loop exit
(Loop (+ 1 count) count false)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= (+ 1 count ) count )
(= false true)))
; Loop with if-test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count true)
false)))
(check-sat)
(get-model)
(check-sat)
(get-model)
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
Result
; Loop is entered in arbitrary values of count, old_count
(assert (forall ((count Int) (old_count Int))
(Loop count old_count false)))
; Loop without if test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= count count)))
(Loop count count true)))
; Loop without if test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= count count))
(= truetrue)))
(set-logic HORN)
(declare-fun Loop (Int Int Bool) Bool)
(declare-fun WhileTest (Int Int Bool) Bool)
; Loop is entered in arbitrary values of count, old_count
; Loop without if test + repeat loop
; Loop without if test + loop exit
; Loop with if-test + repeat loop
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count ))
; Loop with if-test + repeat loop
(Loop (+ 1 count) count false)))
; Loop with if-test + loop exit
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (and (Loop count old_count lock_state) (= (+ 1 count ) count )
(= false true)))
(assert (forall ((count Int) (old_count Int) (lock_state Bool))
(=> (Loop count old_count lock_state)
(= lock_state false))))
(check-sat)
(get-model)
; Loop with if-test + loop exit
(check-sat)
(get-model)
Slicing
• Remove variables that have no effect
Unfolding
• = more aggressive in-lining
• Also applied to predicates that are not
eliminated
A Horn Clause Solver
Algorithm
Objective is to solve for R such that
F
→  ,
→   , ∀
Key elements of PDR algorithm:
Over-approximate reachable states
≔ F  ,  →  → ⋯ →  ≔
Propagate back from ¬
Resolve conflicts
Strengthen/propagate using induction
Algorithm
Objective is to solve for R such that
F
→  ,
Initialize:
→   , ∀

↖
↗
≔
≔ F
F

Main invariant:
↖
↖
↗

+
↖
F
Algorithm
Main invariant:
F
→ +
→
→ +
Search: Mile-high perspective
Modern SMT solver
Decisions:
Conflict
Conflict Clauses
Assignments Resolution
Fixedpoint solver
→ WP  → Conflict ← SP  ←
Resolution
Conflict resolution with arithmetic
R(0,0,0,0).
Initial states
T(L,M,Y1,Y2,L’,M’,Y1’,Y2’)R(L,M,Y1,Y2)  R(L’,M’,Y1’,Y2’)
Reachable states
R(2,2,Y1,Y2)  false
Is unsafe state reachable?
Step(L,L’,Y1,Y2,Y1’)  T(L,M,Y1,Y2,L’,M,Y1’,Y2)
Step(M,M’,Y2,Y1,Y2’)  T(L,M,Y1,Y2,L,M’,Y1,Y2’)
Step(0,1,Y1,Y2,Y2+1).
(Y1 ≤ Y2 ∨ Y2 = 0)  Step(1,2,Y1,Y2,Y1).
Step(2,3,Y1,Y2,Y1).
Step(3,0,Y1,Y2,0).
P1 takes a step
P2 takes a step
ℓ :  ≔  + ;  ℓ
ℓ :   =  ∨  ≤  ;  ℓ
ℓ :  ;  ℓ
ℓ :  ≔ ;  ℓ
Search: Mile-high perspective

F
()
F 2 ()
B2 ¬
B ¬
¬
Conflict Propagation
Conflict Propagation
Conflict Resolution
Interpolating Conflicts
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
Conflict Resolution
≥  +  ∧  ≥
Conflict
∧
≤ 0
≥
∧
≤ 0∧
Resolution
Get Generalization from Farkas Lemma
Eg., resolve away blue internal variables
Interpolating Conflicts
=
=
=
==
=
→
≥

=

→  ≥
=
=
Conflict Resolution
Conflict Propagation
Conflict Propagation
=
=
=
=
=
==
→=≥
=
=
Generalization from T-lemmas
Can we satisfy?
(, , , ).
Initial states
, , , , ’, ’, ’, ’ ,  , , ,   ’, ’, ’, ’
Reachable states
, , ,   ¬  =  ∧  =  .
Unsafe state is unreachable
=  ∧  =  ∧  =  ∧ F
M

E.g., there is unsat core of:

is unsatisfiable
≤  ≤  ∧ F

M
Unsat proof uses T-lemmas
>  ∨  <  ∨  −  >  ∨  −  >
¬
¬M
Generalization from T-lemmas
Can we satisfy?
(, , , ).
Initial states
, , , , ’, ’, ’, ’ ,  , , ,   ’, ’, ’, ’
Reachable states
, , ,   ¬  =  ∧  =  .
Unsafe state is unreachable
Unsat proof uses T-lemmas
>  ∨  <  ∨  −  >  ∨  −  >
¬
¬M
⋅ − ≤ −
≤
⋅ ( −  ≤ )
−  ≤
− ≤ −
≤
−  ≤
−  ≤
−−−−− −
≤ −
−   ≤

```