Applications of Higher-Order Model
Checking to Program Verification
Hiroshi Unno
University of Tsukuba(Joint work with Naoki Kobayashi, Ryosuke
Sato, Tachio Terauchi, and Takuya Kuwahara)

2016/9/20

Workshop on HOMC + CDPS

1

Success Story:
Software Model Checkers for C
Prove Properties of Program Executions
Specification:
Program:𝑃𝑃 ⊨ Ψ
SLAM, BLAST,MAGIC, …

Concurrency
Recursive Procedures
Heap Data Structures
2016/9/20

TERMINATOR,…

Safety
TNT, T2,
Termination…
Non-termination
LTL, CTL, fair CTL, CTL*

T2, Workshop… on HOMC + CDPS

2

Challenge: How To Construct
Software Model Checker for OCaml?
Prove Properties of Program Executions
Program:Specification:• Higher-order Functions• Exception Handling• Algebraic Data Structures• Objects & Dyn. Dispatch• General References

SafetyTermination
Non-termination
LTL, CTL, fair CTL, CTL*

2016/9/20

𝑃𝑃 ⊨ Ψ
Workshop on HOMC + CDPS

3

This Tutorial: Software Model Checker
MoCHi for OCaml based on HOMC
Prove Properties of Program Executions
Program:Specification:

𝑃𝑃 ⊨ Ψ

• Higher-order Functions
Safety• Exception Handling
Termination• Algebraic Data
Non-termination
Structures𝜔𝜔-regular properties
2016/9/20

Workshop on HOMC + CDPS

4

This Tutorial: Software Model Checker
MoCHi for OCaml based on HOMC
Prove Properties of Program Executions
Program:Specification:

𝑃𝑃 ⊨ Ψ

• Higher-order Functions
Safety• Exception Handling
Termination• Algebraic Data
Non-termination
Structures𝜔𝜔-regular properties
2016/9/20

Workshop on HOMC + CDPS

5

Tool Demonstration of MoCHi• Web interface available from:http://www-kb.is.s.utokyo.ac.jp/~ryosuke/mochi/

2016/9/20

Workshop on HOMC + CDPS

6

Overall Flow of Safety Verification
OCaml Program
Function Encoding [Sato+ ’13]
Higher-order Integer Program
Predicate Abstraction+ CEGAR [Kobayashi+ ’11]

𝜆𝜆→ + recursion+ algebraic data types+ exceptions+ integers + booleans
𝜆𝜆→ + recursion+ integers + booleans

Higher-order Boolean Program

𝜆𝜆→ + recursion+ booleans

Higher-Order Model Checking(TRecS, HorSat, C-SHORe, Preface,…)Sound and complete!

2016/9/20

Workshop on HOMC + CDPS

7

Overall Flow of Safety Verification
OCaml Program
Function Encoding [Sato+ ’13]
Higher-order Integer Program
Predicate Abstraction+ CEGAR [Kobayashi+ ’11]

𝜆𝜆→ + recursion+ algebraic data types+ exceptions+ integers + booleans
𝜆𝜆→ + recursion+ integers + booleans

Higher-order Boolean Program

𝜆𝜆→ + recursion+ booleans

Higher-Order Model Checking(TRecS, HorSat, C-SHORe, Preface,…)Sound and complete!

2016/9/20

Workshop on HOMC + CDPS

8

Higher-Order Model Checking• A generalization of ordinary model checking：– Model the target system as a recursion scheme
and check if it satisfies the given specification
Model Checking
Finite state model checking
Pushdown model checking
Higher-order model checking

2016/9/20

Verification Target
Simple loops
First-order recursive functions
Higher-order recursive functions

Workshop on HOMC + CDPS

9

Higher-Order Recursion Scheme (HORS)• Grammar for generating a possibly infinite tree
S → aOrder-0 scheme
S → a c B
B → b S
S→ a
c

→ a
B

c

c B
B → b
S

b

c

b

S
2016/9/20→ ... →

→ a

a
c

b
a
c

b

a
c

a
B

Workshop on HOMC + CDPS

c

b

10

Higher-Order Recursion Scheme (HORS)• Grammar for generating a possibly infinite tree
A x → aOrder-1 schemex A(b x)a
S → A cA x → a x (A (b x))
c a
S →A c → a→ ac A(b c) c

→ ... →ab A(b(b c))c

2016/9/20

Workshop on HOMC + CDPS

b

a

a
b
c
b b ...
c b
b
c

11

Higher-Order Model Checking
Given
𝑮𝑮: a recursion scheme
𝑨𝑨: a tree automaton,
𝑻𝑻𝑻𝑻𝑻𝑻𝑻𝑻 𝑮𝑮 ∈ 𝑳𝑳(𝑨𝑨)?

a
c

e.g.
- Does every finite path end with “c”?
- Does “a” occur eventually whenever “b” occurs?

• Decidable but n-EXPTIME-complete(for order-n recursion scheme) [Ong ’06]
• Practical higher-order model checkers[Kobayashi
have been developed
2016/9/20
Workshopon HOMC + CDPS’09,…]

a
b

a

a
b
c
b b ...
c b
b
c

12

HORS as a Programming Language
Recursion schemes≈
Simply-typed λ-calculus+ recursion+ tree constructors (but no destructors)(+ finite data domains such as booleans)
2016/9/20

Workshop on HOMC + CDPS

13

From Program Verification toHigher-Order Model Checking [Kobayashi ’09]
Higher-orderbooleanprogram+
specification(on events or
output)2016/9/20

Program
Transformation

HORS(describing all
event sequences
or outputs)+
Tree automaton
recognizing valid
event sequences
or outputs

Workshop on HOMC + CDPS

Model
Checking

14

continuation parameter,
Example: Fromexpressing
Program
Verification
tohow“foo” is accessed
after theChecking
call returns
Higher-Order Model

let rec f(x) =F x k → + (c k) (r (F x k))+
if ∗ then close(x)S → F d else (read(x); f(x))
c r
CPS
in
+
Transformation!

let y = open “foo”
r
c
in
+

f (y)
r
c
...



Is the file “foo”
accessed according
to read* close?
2016/9/20

Is each path of the treelabeled by 𝑟𝑟 ∗ 𝑐𝑐?

Workshop on HOMC + CDPS

15

continuation parameter,
Example: Fromexpressing
Program
Verification
tohow“foo” is accessed
after theChecking
call returns
Higher-Order Model

let rec f(x) =F x k → + (c k) (r (F x k))+
if ∗ then close(x)S → F d else (read(x); f(x))
c r
CPS
in
+
Transformation!

let y = open “foo”
r
c
in
+

f (y)
r
c
...



Is the file “foo”
accessed according
to read* close?
2016/9/20

Is each path of the treelabeled by 𝑟𝑟 ∗ 𝑐𝑐?

Workshop on HOMC + CDPS

16

continuation parameter,
Example: Fromexpressing
Program
Verification
tohow“foo” is accessed
after theChecking
call returns
Higher-Order Model

let rec f(x) =F x k → + (c k) (r (F x k))+
if ∗ then close(x)S → F d else (read(x); f(x))
c r
CPS
in
+
Transformation!

let y = open “foo”
r
c
in
+

f (y)
r
c
...



Is the file “foo”
accessed according
to read* close?
2016/9/20

Is each path of the treelabeled by 𝑟𝑟 ∗ 𝑐𝑐?

Workshop on HOMC + CDPS

17

continuation parameter,
Example: Fromexpressing
Program
Verification
tohow“foo” is accessed
after theChecking
call returns
Higher-Order Model

let rec f(x) =F x k → + (c k) (r (F x k))+
if ∗ then close(x)S → F d else (read(x); f(x))
c r
CPS
in
+
Transformation!

let y = open “foo”
r
c
in
+

f (y)
r
c
...



Is the file “foo”
accessed according
to read* close?
2016/9/20

Is each path of the treelabeled by 𝑟𝑟 ∗ 𝑐𝑐?

Workshop on HOMC + CDPS

18

Program Verification based on
Higher-Order Model Checking [Kobayashi ’09]
Higher-orderbooleanprogram+Specification

Program
Transformation

HORS
+
Tree
automaton

Model
Checking

Sound, complete, and automatic for:- Simply-typed 𝜆𝜆-calculus + recursion+ tree constructors (but no destructors)+ finite data domains (e.g. booleans)(but not for infinite data domains!)- A large class of verification problems:resource usage verification,
reachability, flow analysis, ...19
2016/9/20
Workshop on HOMC + CDPS

Overall Flow of Safety Verification
OCaml Program
Function Encoding [Sato+ ’13]
Higher-order Integer Program
Predicate Abstraction+ CEGAR [Kobayashi+ ’11]

𝜆𝜆→ + recursion+ algebraic data types+ exceptions+ integers + booleans
𝜆𝜆→ + recursion+ integers + booleans

Higher-order Boolean Program

𝜆𝜆→ + recursion+ booleans

Higher-Order Model Checking(TRecS, HorSat, C-SHORe, Preface,…)Sound and complete!

2016/9/20

Workshop on HOMC + CDPS

20

Predicate Abstraction [Graf & Saidi ’97]
Program

Predicate
Abstraction
BooleanProgram

2016/9/20

let f x = x+1
𝑃𝑃 ≡ 𝜆𝜆𝜆𝜆. 𝑥𝑥 ≥ 0 𝑄𝑄 ≡ 𝜆𝜆𝜆𝜆. 𝑦𝑦 ≥ 0Predicates¬𝑃𝑃 𝑥𝑥 ⇏ 𝑄𝑄 𝑥𝑥 + 1¬𝑃𝑃 𝑥𝑥 ⇏ ¬𝑄𝑄 𝑥𝑥 + 1

b=true ⇔ 𝑃𝑃 𝑥𝑥

let f b = if b then true else rndbool
𝑃𝑃 𝑥𝑥 ⇒ 𝑄𝑄 𝑥𝑥 + 1

Workshop on HOMC + CDPS

21

CEGAR [Clarke et al. ’00]

Program
Predicate
Abstraction

New
Predicates

BooleanProgram

CEGAR
Loop

Model Checking

NG

Error TraceOK

infeasible

Feasibility
Checkfeasible

unsafesafe
2016/9/20

Predicate
DiscoveryWorkshop on HOMC + CDPS

22

CEGAR [Clarke et al. ’00]

Program
Predicate
Abstraction

New
Predicates

BooleanProgram

CEGAR
Loop

Model Checking

NG

Error TraceOK

infeasible

Feasibility
Checkfeasible

unsafesafe
2016/9/20

Predicate
DiscoveryWorkshop on HOMC + CDPS

23

Challenges in Higher-Order Setting• Model Checking– How to precisely analyze higher-order control flows?
⇒ Higher-order model checking!

• Predicate Abstraction– How to ensure consistency of abstraction?

• Predicate Discovery– How to find new predicates that can eliminate an
infeasible error trace from the abstraction?
2016/9/20

Workshop on HOMC + CDPS

24

Challenges in Higher-Order Setting• Predicate Abstraction– How to ensure consistency of abstraction?
let sum n k = if n≤0 then k 0 𝜆𝜆x’.x’≥n-1
else sum (n-1) (𝜆𝜆x’.k (x’+n))
let main m = sum m (𝜆𝜆x.assert(x≥m))
𝜆𝜆x.x≥n𝜆𝜆x.x≥m
2016/9/20

Workshop on HOMC + CDPS

25

Our Solution: Abstraction Types• Specify which predicates should be used for
abstraction of each expression• int 𝑃𝑃1 , … , 𝑃𝑃𝑛𝑛

Int. exps. that should be abstracted by 𝑃𝑃1 , … , 𝑃𝑃𝑛𝑛e.g., 3 ∶ int 𝜆𝜆𝜆𝜆. 𝑥𝑥 > 0, 𝑒𝑒𝑒𝑒𝑒𝑒𝑒𝑒? ↝ true, false• 𝑥𝑥 ∶ int 𝑃𝑃1 , … , 𝑃𝑃𝑛𝑛

→ int 𝑄𝑄1 , … , 𝑄𝑄𝑚𝑚

Assuming that argument 𝑥𝑥 is abstracted by 𝑃𝑃1 , … , 𝑃𝑃𝑛𝑛 ,abstract the return value by 𝑄𝑄1 , … , 𝑄𝑄𝑚𝑚

2016/9/20

Workshop on HOMC + CDPS

26

Example: Abstraction Types
let sum n k = if n≤0 then k 0 𝜆𝜆x’.x’≥n-1
else sum (n-1) (𝜆𝜆x’.k (x’+n))
let main m = sum m (𝜆𝜆x.assert(x≥m))
𝜆𝜆x.x≥n𝜆𝜆x.x≥msum: (n:int[]) → (int[𝜆𝜆x.x≥n] → ⋆) → ⋆no predicates for n

2016/9/20

predicate for
abstracting the 1stargument of k

Workshop on HOMC + CDPS

Unit type27

Example: Predicate Abstraction
𝜆𝜆x’.x’≥n-1

let sum n k = if n≤0 then k 0
else sum (n-1) (𝜆𝜆x’.k (x’+n)) n>0
let main m = sum m (𝜆𝜆x.assert(x≥m))
𝜆𝜆x.x≥nsum: (n:int[]) → (int[𝜆𝜆x.x≥n] → ⋆) → ⋆let sum () k =x’≥n-1 ∧ n>0 ⇒ x’+n≥n
if * then k trueelse sum () (𝜆𝜆b’.k (if b’ then true else rndbool))let main () = sum () (𝜆𝜆b. assert(b))
Successfullymodel checked!
2016/9/20
Workshop on HOMC + CDPS
28

Type-Directed Predicate Abstraction
HO Int Expression

Abstraction TypeΓ ⊢ 𝑀𝑀 ∶ 𝜏𝜏 ↝ 𝑡𝑡

Abstraction Type Environment

HO Bool Expression′Γ ⊢ 𝑀𝑀 ∶ 𝜏𝜏 → 𝜏𝜏 ↝ 𝑠𝑠′
Γ ⊢ 𝑁𝑁 ∶ 𝜏𝜏 ↝ 𝑡𝑡

Γ ⊢ 𝑀𝑀 𝑁𝑁 ∶ 𝜏𝜏 ↝ 𝑠𝑠 𝑡𝑡

Predicate Abstraction Rule for Function Applications
2016/9/20

Workshop on HOMC + CDPS

29

Challenges in Higher-Order Setting• Predicate Discovery– How to find new predicates that can eliminate an
infeasible error trace from the abstraction?

2016/9/20

Workshop on HOMC + CDPS

30

Challenges in Higher-Order Setting• Predicate Discovery– How to find abstraction types that can eliminate
an infeasible error trace from the abstraction?

2016/9/20

Workshop on HOMC + CDPS

31

Our Solution• Reduction to refinement type inference ofa straightline higher-order program (SHP)
Infeasible
Error Trace
Straightline
Higher-Order
Program (SHP)

2016/9/20

Abstraction
Types
Refinement Type
Inference[U. & Kobayashi ’09]

Workshop on HOMC + CDPS

Refinement
Types

32

Refinement Types [Xi & Pfenning ’98, ’99]
• 𝑥𝑥 ∶ int | 𝑥𝑥 ≥ 0

Non-negative integers

FOL formulas (e.g. QFLIA)
for type refinement• 𝑥𝑥 ∶ int → {𝑟𝑟 ∶ int | 𝑟𝑟 ≥ 𝑥𝑥}

Functions that take an integer 𝑥𝑥 andreturn an integer 𝑟𝑟 not less than 𝑥𝑥

Soundness of refinement type system ⊢𝑅𝑅𝑅𝑅𝑅𝑅 :𝑃𝑃 is safe (i.e., 𝑃𝑃 −→∗ assert false)
if 𝑃𝑃 is well-typed (i.e., ∃𝛤𝛤. 𝛤𝛤 ⊢𝑅𝑅𝑅𝑅𝑅𝑅 𝑃𝑃)

2016/9/20

Workshop on HOMC + CDPS

33

Example: Abstraction Type Finding (1/2)
let sum n k = if n≤0 then k 0
else sum (n-1) (𝜆𝜆x’.k (x’+n))
let main m = sum m (𝜆𝜆x.assert(x≥m))m≤00<m
2016/9/20

Infeasible error trace:
main m → sum m (𝜆𝜆x.assert(x≥m))→ if m≤0 then (𝜆𝜆x.assert(x ≥m)) 0 else …
→ (𝜆𝜆x.assert(x≥m)) 0→ assert(0≥m)→ failWorkshop on HOMC + CDPS

34

Example: Abstraction Type Finding (2/2)

let sum n k = if n≤0 then k 0
else sum (n-1) (𝜆𝜆x’.k (x’+n))
let main m = sum m (𝜆𝜆x.assert(x≥m))

main m →∗ if m≤0… →∗ m≤0 assert(0≥m) →0<m fail

Straightline Higher-Order Program (SHP):
let sum n k = assume(n≤0); k 0
let main m = sum m (𝜆𝜆x.assume(x<m); fail)[U. & Kobayashi ’09]
Abstraction Type:
Refinement
Type of SHP:
sum: (n:int[])(n:int) →→({x:int|x≥n}(int[𝜆𝜆x.x≥n]
→→
⋆)⋆)
→→
⋆ ⋆
2016/9/20

Workshop on HOMC + CDPS

35

Refinement Type Inference[U. & Kobayashi ’09]

SHP

2016/9/20

Constraint
Generation

Horn
ClauseConstraints

Workshop on HOMC + CDPS

Constraint
Solving

Refinement
Types

36

Example: Constraint Generation
Straightline Higher-Order Program (SHP):
let sum n k = assume(n≤0); k 0
let main m = sum m (𝜆𝜆x.assume(x<m); fail)
Refinement Type Templates:
sum: (n:{n:int|P(n)}) →({x:int|Q(n,x)} → ⋆) → ⋆2016/9/20

Horn Clause Constraints:⊤ ⇒ P(m)P(n) ∧ n≤0 ∧ x=0 ⇒ Q(n,x)P(m) ∧ Q(m,x) ∧ x<m ⇒ ⊥Workshop on HOMC + CDPS

37

Example: Constraint Solving (1/2)
Horn Clause Constraints:⊤ ⇒ P(m)P(n) ∧ n≤0 ∧ x=0 ⇒ Q(n,x)P(m) ∧ Q(m,x) ∧ x<m ⇒ ⊥Horn Clause Constraints with P eliminated:n≤0 ∧ x=0 ⇒ Q(n,x)
Q(m,x)⇒
Q(n,x)⇒ (n=mx≥m ⇒x≥m)

Interpolating Prover

2016/9/20

Solution: Q(n,x) ≡ x≥nWorkshop on HOMC + CDPS

38

Interpolating Prover• Input: 𝜙𝜙1 , 𝜙𝜙2 such that 𝜙𝜙1 ⇒ 𝜙𝜙2• Output: an interpolant 𝜙𝜙 of 𝜙𝜙1 , 𝜙𝜙2 such that:
1. 𝜙𝜙1 ⇒ 𝜙𝜙
2. 𝜙𝜙 ⇒ 𝜙𝜙2
3. 𝐹𝐹𝐹𝐹 𝜙𝜙 ⊆ 𝐹𝐹𝐹𝐹 𝜙𝜙1 ∩ 𝐹𝐹𝐹𝐹 𝜙𝜙2• Example: x≥n is an interpolant of:n≤0 ∧ x=0 and n=m ⇒x≥m
2016/9/20

Workshop on HOMC + CDPS

39

Example: Constraint Solving (2/2)
Horn Clause Constraints:⊤ ⇒ P(m)P(n) ∧ n≤0 ∧ x=0 ⇒ Q(n,x)P(m) ∧ Q(m,x) ∧ x<m ⇒ ⊥Substitute Q(n,x) with x≥nHorn Clauses with P1 substituted:⊤ ⇒ P(m)P(n) ⇒ (n≤0 ∧ x=0 ⇒ x≥n)Interpolating Prover

2016/9/20

Solution: P(n) ≡ ⊤Workshop on HOMC + CDPS

40

Example: Refinement Type Inference
Straightline Higher-Order Program (SHP):
let sum n k = assume(n≤0); k 0
let main m = sum m (𝜆𝜆x.assume(x<m); fail)
Refinement Type Templates:
sum: (n:{n:int|P(n)}) →({x:int|Q(n,x)} → ⋆) → ⋆2016/9/20

Refinement Types of SHP:
sum: (n:{n:int|⊤}) →({x:int|x≥n} → ⋆) → ⋆Workshop on HOMC + CDPS

41

Overall Flow of Safety Verification
OCaml Program
Function Encoding [Sato+ ’13]
Higher-order Integer Program
Predicate Abstraction+ CEGAR [Kobayashi+ ’11]

𝜆𝜆→ + recursion+ algebraic data types+ exceptions+ integers + booleans
𝜆𝜆→ + recursion+ integers + booleans

Higher-order Boolean Program

𝜆𝜆→ + recursion+ booleans

Higher-Order Model Checking(TRecS, HorSat, C-SHORe, Preface,…)Sound and complete!

2016/9/20

Workshop on HOMC + CDPS

42

Function Encoding of Lists• Encode a list as a pair (len, f) such that:– len is the length of the list
– f is a function from an index 𝑖𝑖 to the 𝑖𝑖-th element• e.g., [3;1;4] is encoded as (3, f) where:
f(0)=3, f(1)=1, f(2)=4, and undefined otherwise

let nil = (0, fun i -> ⊥)let cons a (len, l) = (len + 1, fun i -> if i = 0 then a else l (i - 1))
let hd (len, l) = assert (len ≠ 0); l 0
let tl (len, l) = assert (len ≠ 0); (len - 1, fun i -> l (i + 1))
let is_nil (len, l) = len = 0
2016/9/20

Workshop on HOMC + CDPS

43

Function Encoding of
Algebraic Data Structures• Encode an algebraic data structure as afunction from the path of a node to its label
type btree = Leaf of int | Node of btree * btree
Node
Node

Leaf

2016/9/20

3 LeafLeaf

1

4

A function f such that:f [] = Nodef [1] = Leaf
f [2] = Nodef [1;1] = 3
f [2;1] = Leaf f [2;2] = Leaf
f [2;1;1] = 1
f [2;2;1] = 4
Workshop on HOMC + CDPS

44

Function Encoding of Exceptions
exception NotPos

type exc = NotPos

let rec fact n =if n ≤ 0 thenraise NotPoselse
tryn × fact (n-1)
with NotPos -> 1

let rec fact n k exn =if n ≤ 0 thenexn NotPos
elsefact (n-1)(fun r -> k (n × r))(fun NotPos -> k 1)

2016/9/20

CPS
Trans.

Workshop on HOMC + CDPS

45

Summary: Safety Verification by MoCHi• For finite-data HO programs: sound, complete, and fullyautomatic verification by reduction to HO model checking[Kobayashi ’09]

• For infinite-data HO programs: sound and automatic (butincomplete) verification by a combination of:– HO model checking– predicate abstraction & discovery [Kobayashi+ ’11, U.+ ’09, ’15]
– program transformation [Sato+ ’13]

Necessarily incomplete but often more precise than otherapproaches
Sometimes relatively complete modulo certain assumptions– relatively complete refinement type system [U.+ ’13]
– relatively complete predicate discovery [Terauchi & U. ’15]
2016/9/20

Workshop on HOMC + CDPS

46

This Tutorial: Software Model Checker
MoCHi for OCaml based on HOMC
Prove Properties of Program Executions
OCaml Program:Specification:

𝑃𝑃 ⊨ Ψ

• Higher-order Functions
Safety• Exception Handling
Termination• Algebraic Data
Non-termination
Structures𝜔𝜔-regular properties
2016/9/20

Workshop on HOMC + CDPS

47

Termination Verification• Automatically prove that a program
terminates for every input (and nondeterminism)
Input

let rec fib n =if n<2 then 1else
fib(n-1) + fib(n-2)
let main () = fib *2016/9/20

Terminating

Unknown
Workshop on HOMC + CDPS

48

Tool Demonstration of MoCHi• Web interface available from:http://www.kb.is.s.utokyo.ac.jp/~kuwahara/termination/

2016/9/20

Workshop on HOMC + CDPS

49

1st Naïve Approach to Termination
Verification of HO Functional Programs• Abstract to a finite data HO program,and apply HO model checking• Problem: many terminating programs are turned into
non-terminating ones by abstraction
e.g. f(x) = if x<0 then 1 else 1+f(x-1) terminating f(bx<0) = if bx<0 then 1 else 1+f(*) non-terminating

2016/9/20

Workshop on HOMC + CDPS

50

Termination Verification
for Imperative Programs• Binary Reachability Analysis [Cook+ ’06]
– Theorem [Podelski & Rybalchenko ’04]:
𝑃𝑃 is terminating iff
𝑇𝑇 + is disjunctively well-founded (dwf)• 𝑇𝑇: the transition relation of 𝑃𝑃• dwf: a finite union of well-founded relations

2016/9/20

Workshop on HOMC + CDPS

51

Example: Binary Reachability Analysis
1: x = *;2: while(x>0){
3: x--;
4: }𝑻𝑻+ ⊆ {(s, s’) | s.pc < s’.pc}∪ {(s, s’) | s.pc > s’.pc}∪ {(s, s’) | s.x > s’.x ≧ 0}

Terminating!
pc=1
x=2

2016/9/20

pc=2
x=2

pc=3
x=2

pc=2
x=1

Workshop on HOMC + CDPS

pc=3
x=1

pc=2
x=0

pc=4
x=0

52

2nd Naïve Approach to Termination
Verification of HO Functional Programs• Check that →+ is dwf by [Cook+ ’06]

→ : the one-step reduction relation of the HO program 𝑃𝑃• Problem: [Cook+ ’06] needs to reason aboutchange in calling context / call stack– Theorem [Berardi+’14, Yokoyama’14]:[Cook+ ’06] can only prove termination of primitive
recursive functions (when usable wf relations haveheight at most 𝜔𝜔)
2016/9/20

Workshop on HOMC + CDPS

53

2nd Naïve Approach to Termination
letrec ack m n =of HO Functional Programs
Verification

if m = 0 then n+ + 1• elseCheckdwf(m-1)
by [Cook+’06]
if nthat= 0→
thenis ack
1→ : thereduction
relation of the HO program 𝑃𝑃
else
ackone-step(m-1) (ackm (n-1))•let
Problem:
needs
about
main m [Cook+n = if m’06]> 0 &&n >to0 reason
then ackmnchange in calling
contextrelation/ call stack
Terminates
but transitionis quite complex– Theorem [Berardi+’14, Yokoyama’14]:[Cook+ ’06] can only prove termination of primitive
recursive functions (when usable wf relations haveheight at most 𝜔𝜔)
2016/9/20

Workshop on HOMC + CDPS

54

Our Solution: Binary Reachability
Analysis Generalized to HO [Kuwahara+ ’14]
• Theorem [Kuwahara+ ’14]:

HO functional program 𝑃𝑃 is terminating iff 𝐶𝐶𝐶𝐶𝐶𝐶𝑙𝑙𝑃𝑃+ is dwf– The calling relation 𝐶𝐶𝐶𝐶𝐶𝐶𝑙𝑙𝑃𝑃 of 𝑃𝑃:
𝑓𝑓𝑣𝑣,
� 𝑔𝑔𝑤𝑤
� ∣ 𝑔𝑔𝑤𝑤
� is called from 𝑓𝑓𝑣𝑣� in an execution of 𝑃𝑃– 𝐶𝐶𝐶𝐶𝐶𝐶𝑙𝑙𝑃𝑃+ = 𝑓𝑓 𝑣𝑣,
� 𝑔𝑔𝑤𝑤
� ∣ 𝑚𝑚𝑚𝑚𝑚𝑚𝑚𝑚() →∗ 𝐸𝐸 𝑓𝑓𝑣𝑣� , 𝑓𝑓𝑣𝑣� →+ 𝐸𝐸 ′ 𝑔𝑔𝑤𝑤
�

2016/9/20

Workshop on HOMC + CDPS

55

Example: Generalized Binary
Reachability Analysis
let rec fib n =if n<2 then 1
else fib (n-1)+ fib (n-2)
let main()=fib(rand())

Call={(fib(n),fib(n-1))|n>1}∪{(fib(n),fib(n-2))|n>1}⊆{(fib m,fib n) | m>n≥0}
2016/9/20(Tree representation)Workshop on HOMC + CDPS

main()
fib3
fib2

fib1
fib0

fib1
56

Reduce Binary Reachability
to Plain Reachability• Goal: check 𝐶𝐶𝐶𝐶𝐶𝐶𝑙𝑙𝑃𝑃 ⊆ 𝑊𝑊 for some dwf 𝑊𝑊• Approach: reduction to a safety verification problem
by program transformation– To each function 𝑓𝑓, add an extra argument to record theargument of an ancestor call to 𝑓𝑓– Assert that 𝑊𝑊 holds when 𝑓𝑓 is called

fib n =
if n<2 then nelse fib(n-1)+fib(n-2)
main() = fib(rand())
W = {(m,n) | m>n≥0}

2016/9/20

fib m n =assert(m>n≥0);
let m’= if * then m else n in
if n<2 then nelse fib m’ (n-1)+fib m’ (n-2)
main() = fib ⊥ (rand())

Workshop on HOMC + CDPS

57

This Tutorial: Software Model Checker
MoCHi for OCaml based on HOMC
Prove Properties of Program Executions
OCaml Program:Specification:

𝑃𝑃 ⊨ Ψ

• Higher-order Functions
Safety• Exception Handling
Termination• Algebraic Data
Non-termination
Structures𝜔𝜔-regular properties
2016/9/20

Workshop on HOMC + CDPS

58

Automata-Theoretic Approach [Vardi’91]• Input:– Program 𝑃𝑃– 𝜔𝜔-regular temporal property Ψ

1. Construct 𝜔𝜔-automaton 𝐴𝐴¬Ψ (with a fairness
acceptance condition) that recognizes 𝐿𝐿 ¬Ψ
2. Construct product program 𝑃𝑃 × 𝐴𝐴¬Ψ
3. Verify that 𝑃𝑃 × 𝐴𝐴¬Ψ is fair terminating(i.e., no infinite execution trace that is fair)
Theorem: 𝑃𝑃 ⊨ Ψ iff 𝑃𝑃 × 𝐴𝐴¬Ψ is fair terminating
2016/9/20

Workshop on HOMC + CDPS

59

Definition: Fair Termination of 𝑃𝑃• Fairness Constraint: 𝐶𝐶 = 𝐴𝐴1 , 𝐵𝐵1 , … , 𝐴𝐴𝑛𝑛 , 𝐵𝐵𝑛𝑛
• Infinite sequence 𝜋𝜋 is fair wrt 𝐶𝐶 if ∀ 𝐴𝐴, 𝐵𝐵 ∈ 𝐶𝐶,– 𝐴𝐴 occurs only finitely often in 𝜋𝜋 or– 𝐵𝐵 occurs infinitely often in 𝜋𝜋• 𝑃𝑃 is fair terminating wrt 𝐶𝐶 if 𝑃𝑃 has
no infinite execution trace that is fair wrt 𝐶𝐶
2016/9/20

Workshop on HOMC + CDPS

60

Fair Termination Verification for
Imperative Programs [Cook+ ’07]
• Theorem:
𝑃𝑃 is fair terminating wrt 𝐶𝐶 iff 𝑇𝑇 +↾𝐶𝐶 is dwf– 𝑇𝑇: transition relation of 𝑃𝑃– fair transitive closure 𝑅𝑅 +↾𝐶𝐶 of 𝑅𝑅 is defined by:∀1 ≤ 𝑖𝑖 < 𝑛𝑛. 𝑠𝑠𝑖𝑖 , 𝑠𝑠𝑖𝑖+1 ∈ 𝑅𝑅,+↾𝐶𝐶 =
𝑠𝑠1 , 𝑠𝑠𝑛𝑛
𝑅𝑅
𝑠𝑠1 ⋯ 𝑠𝑠𝑛𝑛 is fair wrt 𝐶𝐶, 𝑛𝑛 ≥ 2(Intuitively means the subset of 𝑅𝑅 + that is fair wrt 𝐶𝐶)

2016/9/20• Finite sequence 𝑠𝑠1 ⋯ 𝑠𝑠𝑛𝑛 is fair wrt 𝐶𝐶 if ∀ 𝐴𝐴, 𝐵𝐵 ∈ 𝐶𝐶,
𝐴𝐴 does not occur in 𝑠𝑠1 ⋯ 𝑠𝑠𝑛𝑛 or 𝐵𝐵 occurs in 𝑠𝑠1 ⋯ 𝑠𝑠𝑛𝑛
Workshop on HOMC + CDPS

61

1st Naïve Approach to Fair Termination
Verification of HO Functional Programs• Check that →+↾𝐶𝐶 is dwf→ : the one-step reduction relation of the HO program 𝑃𝑃• Suffers from the same problem as the 2nd naïve
approach to plain termination verification of HO
functional programs:– [Cook+ ’07] needs to reason about change in calling
context / call stack

2016/9/20

Workshop on HOMC + CDPS

62

2nd Naïve Approach to Fair Termination
Verification of HO Functional Programs• Check that 𝐶𝐶𝐶𝐶𝐶𝐶𝐶𝐶𝑃𝑃+↾𝐶𝐶 is dwf+↾𝐶𝐶• Unsound: There is a case that 𝐶𝐶𝐶𝐶𝐶𝐶𝐶𝐶𝑃𝑃 is dwf

but 𝑃𝑃 is not fair-terminating wrt 𝐶𝐶– For example,
f x = if x ≤ 0 then () else (f 0; f 1)
𝐶𝐶 = true, 𝑓𝑓 0
(fair wrt 𝐶𝐶 iff f 0 is called infinitely often)
𝑓𝑓 2 →∗ 𝑓𝑓 0; 𝑓𝑓 1 →∗ 𝑓𝑓 1 →∗ 𝑓𝑓 0; 𝑓𝑓 1 →∗ …

2016/9/20

Workshop on HOMC + CDPS

63

Our Solution: Fair-Termination Analysis
Generalized to HO Programs [Murase+ ’16]
• Check disjunctive well-foundedness of ⊳𝐶𝐶𝑃𝑃 :𝑓𝑓 𝑣𝑣,
� 𝑔𝑔𝑤𝑤
� ∣ 𝑚𝑚𝑚𝑚𝑚𝑚𝑚𝑚() →∗ 𝐸𝐸 𝑓𝑓 𝑣𝑣� , 𝑓𝑓 𝑣𝑣� →+↾𝐶𝐶 𝐸𝐸 ′ 𝑔𝑔𝑤𝑤
�
– Note that ⊳𝐶𝐶𝑃𝑃 is 𝐶𝐶𝐶𝐶𝐶𝐶𝑙𝑙𝑃𝑃+ but →+ replaced by →+↾𝐶𝐶• Theorem:𝐶𝐶
𝑃𝑃 is fair-terminating wrt 𝐶𝐶 iff ⊳𝑃𝑃 is dwf

2016/9/20

Workshop on HOMC + CDPS

64

𝐶𝐶
How to Check that ⊳𝑃𝑃 is dwf?

• By reduction to a safety verification problem
via program transformation similar to the one
for binary reachability analysis(see our POPL’16 paper [Murase+ ’16] for details)

2016/9/20

Workshop on HOMC + CDPS

65

Summary: Plain and Fair Termination
Verification by MoCHi• Naïve combination of HO model checking andpredicate abstraction into HO Boolean
programs is too imprecise• Generalize binary reachability analysis to the
HO setting by introducing the calling relations
𝐶𝐶𝐶𝐶𝐶𝐶𝑙𝑙𝑃𝑃 and ⊳𝐶𝐶𝑃𝑃
2016/9/20

Workshop on HOMC + CDPS

66

This Tutorial: Software Model Checker
MoCHi for OCaml based on HOMC
Prove Properties of Program Executions
OCaml Program:Specification:

𝑃𝑃 ⊨ Ψ

• Higher-order Functions
Safety• Exception Handling
Termination• Algebraic Data
Non-termination
Structures𝜔𝜔-regular properties
2016/9/20

Workshop on HOMC + CDPS

67

Verifying Non-Termination(or Disproving Termination) of HO programs• Goal: prove that a program is non-terminating
for some input (or for some non-deterministic
choice)– complementary to termination verification

2016/9/20

Workshop on HOMC + CDPS

68

Our approach [Kuwahara+ ’15]
• combine over- and under-approximation– over-approximate deterministic branches, andcheck that all the branches are non-terminating– under-approximate non-deterministic branches, andcheck that one of the branches is non-terminating

…
…

…
…

…

∃

spurious path
introduced byoverapproximation

computation tree ofthe abstract program

2016/9/20
computation tree ofthe original program

2016/9/20∀…

path eliminatedby underapproximation

Workshop on HOMC + CDPS

69

Our Approach:
Combination of Under-/Over-approximation
x=0

x=1

y=0 y=1

y=0 y=1

∃
¬x>0

x>0

・・・

∃( ...
/* case ¬x>0 */, ...
/* case x>0 */)・・・

Only one of the
branches needs tobe non-terminating

・・・

・・・

let x=* in
let y=* in
f(x+y)

pred: x>0

Our Approach:
Combination of Under-/Over-approximation
x=0

x=1

y=0 y=1

y=0 y=1

pred: 0≤y≤x

discarded∃( /* case ¬x>0 */
¬x>0
∃(...
∃
/* case ¬0≤y≤x */ )¬0≤y≤x, ...
Under-approximation:)case for ¬x>0∧ 0≤y≤x
is discarded

∃
x>0
0≤y≤x

・・・

・・・

・・・

・・・

let x=* in
let y=* in
f(x+y)

pred: x>0

Our Approach:
Combination of Under-/Over-approximation
x=0

x=1

y=0 y=1

y=0 y=1

pred: 0≤y≤x・・・∃( /* case ¬x>0 */
¬x>0
∃(...
∃
/* case ¬0≤y≤x */ )¬0≤y≤x, ...
Under-approximation:)case for ¬x>0∧ 0≤y≤x
is discarded

・・・

・・・

・・・

let x=* in
let y=* in
f(x+y)

pred: x>0

∃
x>0

∃

¬0≤y≤x0≤y≤xOur Approach:
Combination of Under-/Over-approximation
pred: 0≤y≤x
pred: x+y>0

x=1

y=0 y=1

y=0 y=1
・・・

・・・

・・・

∃( /* case ¬x>0 */∃(/* case ¬0≤y≤x */
... )
, ...
)

x=0

・・・

let x=* in
let y=* in
f(x+y)

pred: x>0

∃
¬x>0

∃
¬0≤y≤xx>0∃¬0≤y≤x0≤y≤xOur Approach:
Combination of Under-/Over-approximation
pred: 0≤y≤x
pred: x+y>0

)

)
, ...

y=0 y=1
・・・

f false /*case ¬x+y>0 */)y=0 y=1

・・・∀( f true /*case x+y>0 */,

x=1

・・・

Overapproximation:
both branches shouldhave an infinite path∃( /* case ¬x>0*/ we don’t know
(sinceis valid)∃(/* case which¬0≤y≤xbranch
*/

x=0

・・・

let x=* in
let y=* in
f(x+y)

pred: x>0

∃
x>0

¬x>0

∃

∃

¬0≤y≤x¬0≤y≤x

0≤y≤x

∀

∀

∀

Summary: Non-Termination
Verification by MoCHi• Underapproximate non-deterministic computation,and check that one of the branches has a nonterminating path
• Overapproximate deterministic computation, andcheck that all the branches have non-terminating
paths• Check them by using HO model checking
∃

∀

∀

∃

…

…

…

Workshop on HOMC + CDPS

…

…

…

…
…

2016/9/20…
…

…

2016/9/20

…

∃

75

Conclusions• HO model checking alone is not enough toconstruct practical software model checkers
for OCaml, Java, …
• It is often the case that software verification
techniques developed for imperative
programs cannot be reused in the HO setting– Types are useful for generalization to HO

2016/9/20

Workshop on HOMC + CDPS

76