First-Order Fixpoint Constraints

Horn Clauses and Beyondfor Relational and Temporal
Program Verification
Hiroshi Unno (University of Tsukuba, Japan)
part of this is joint work with Tachio Terauchi, Eric Koskinen,
Sho Torii, Hiroki Sakamoto, and Yoji Nanjo

2018/7/13

HCVS'18, Oxford, UK

1

My Research: Automated Verificationof Higher-Order Functional Programs• MoCHi: Software Model Checker for OCaml• Assertion safety verification [PLDI’11, PEPM’13, ESOP’15, TACAS’15]• Termination verification [ESOP’14]• Non-termination verification [CAV’15]• Fair-termination verification [POPL’16]

Based on: higher-order model checking, binary reachability analysis, predicate
abstraction, CEGAR based on recursion-free Constrained Horn Clause (CHC) solving• RCaml: Refinement Type Checking and Inference System for OCaml• Assertion safety verification [FLOPS’08, PPDP’09, POPL’13, POPL’18]• (Maximally-weak) precondition inference [SAS’15]• Termination and non-termination verification [SAS’15, POPL’18]• Relational verification [CAV’17]• Temporal safety and liveness verification [LICS’18, CAV’18]

Based on: dependent refinement types and CHC / fixpoint constraint solving
2018/7/13

HCVS'18, Oxford, UK

2This Talk
• MoCHi: Software Model Checker for OCaml• Assertion safety verification [PLDI’11, PEPM’13, ESOP’15, TACAS’15]• Termination verification [ESOP’14]• Non-termination verification [CAV’15]• Fair-termination verification [POPL’16]

Based on: higher-order model checking, binary reachability analysis, predicate
abstraction, CEGAR based on recursion-free Constrained Horn Clause (CHC) solving• RCaml: Refinement Type Checking and Inference System for OCaml• Assertion safety verification [FLOPS’08, PPDP’09, POPL’13, POPL’18]• (Maximally-weak) precondition inference [SAS’15]• Termination and non-termination verification [SAS’15, POPL’18]• Relational verification [CAV’17]• Temporal safety and liveness verification [LICS’18, CAV’18]

Based on: dependent refinement types and CHC / fixpoint constraint solving
2018/7/13

HCVS'18, Oxford, UK

3Outline
1. CHC / Fixpoint Constraints for Program Verification
2. CHC Constraint Solving for Relational Verification• Based on [Unno, Torii and Sakamoto, CAV’17]

3. Fixpoint Constraint Solving for Temporal Verification• Based on [Nanjo, Unno, Koskinen and Terauchi, LICS’18]

2018/7/13

HCVS'18, Oxford, UK

4Outline
1. CHC / Fixpoint Constraints for Program Verification
2. CHC Constraint Solving for Relational Verification• Based on [Unno, Torii and Sakamoto, CAV’17]

3. Fixpoint Constraint Solving for Temporal Verification• Based on [Nanjo, Unno, Koskinen and Terauchi, LICS’18]

2018/7/13

HCVS'18, Oxford, UK

5

CHC based Program Verification
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]) with
Advanced Language Features (e.g., algebraic data structures,
linked data structures, exceptions, higher-order functions) with
Side-Effects (e.g., non-termination, non-determinism, concurrency,
assertions, destructive updates)

ReduceCHC Constraint Solving Problems
2018/7/13

HCVS'18, Oxford, UK

6

Overall Flow of CHC Constraint
based Program Verification
Program & Specification
Constraint Generation
CHC Constraint Set
Constraint Solving
Solution or Counterexample
2018/7/13

HCVS'18, Oxford, UK

7

Overall Flow of CHC 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 sSet= 0;
CHC Constraint
else x + mult x (y - 1)
while(y != 0){s += x;{- Haskell -}Constraint Solvingy--;mult :: Int -> Int -> Int}
mult x 0 = 0
return s;
Solutionor Counterexample
mult x y = x + multx (y - 1)}
2018/7/13
HCVS'18, Oxford, UK

8

Overall Flow of CHC Constraint
based Program Verification
Program & Specification
Constraint Generation
CHC Constraint Set
Constraint Solving
Solution or Counterexample
2018/7/13

HCVS'18, Oxford, UK

9Overall Flow of CHC Constraint
based Program Verification
Program & Specification
Constraint Generation
CHC Constraint Set

𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑟𝑟 Constraint≡ 𝑟𝑟 = 𝑥𝑥 ×Solving𝑦𝑦

Solution or Counterexample

2018/7/13

HCVS'18, Oxford, UK

10

CHC Constraint Set

predicate variables

CHC constraint sets 𝐻𝐻 ∷= 𝐶𝐶1 , … , 𝐶𝐶𝑛𝑛
CHCs 𝐶𝐶 ∷= ∀𝑥𝑥.
� ℎ ⇐ 𝑃𝑃1 𝑡𝑡�1 ∧ ⋯ ∧ 𝑃𝑃𝑛𝑛 𝑡𝑡�𝑛𝑛 ∧ 𝜙𝜙heads ℎ ∷= ⊥ ∣ 𝑃𝑃 𝑡𝑡̃
formulas 𝜙𝜙 ∷= ⊤ ∣ ⊥ ∣ 𝐴𝐴 𝑡𝑡̃ ∣ ¬𝜙𝜙 ∣ 𝜙𝜙 ∧ 𝜙𝜙 ∣ 𝜙𝜙 ∨ 𝜙𝜙terms 𝑡𝑡 ∷= 𝑥𝑥 ∣ 𝑓𝑓 𝑡𝑡̃
function symbols of the
background theory

predicate symbols of the
background theory

Predicate substitution 𝜃𝜃 ∶ PVars → Preds
is called a solution of 𝐻𝐻 if ⊨ 𝜃𝜃 ⋀𝐻𝐻

2018/7/13

HCVS'18, Oxford, UK

11

Overall Flow of CHC Constraint
based Program Verification
Imperative Program &Safety Specification

Initial states: 𝑥𝑥 = 10
Program:while ( x > 0 ) { x--; }Error states: 𝑥𝑥 < 0

𝑅𝑅 𝑥𝑥 ⇐ 𝑥𝑥 = 10
𝑅𝑅 𝑥𝑥 − 1 ⇐ 𝑅𝑅 𝑥𝑥 ∧ 𝑥𝑥 > 0⊥ ⇐ 𝑅𝑅 𝑥𝑥 ∧ 𝑥𝑥 < 0𝜃𝜃 = 𝑅𝑅 ↦ 𝜆𝜆𝜆𝜆. 𝑥𝑥 ≥ 0

Init

2018/7/13

𝑅𝑅 𝜃𝜃(𝑅𝑅)

Error

Constraint Generation
CHC Constraint Set
Constraint Solving
Solvable or Not
HCVS'18, Oxford, UK

12

First-Order Fixpoint Logic ℒ• First-order logic extended with least fixpoints (LFPs)
and greatest fixpoints (GFPs)
predicatevariables

function symbols of the
background theory

2018/7/13

predicate symbols of the
background theory

LFPs(𝑋𝑋 occurs only
positively in 𝜙𝜙)
HCVS'18, Oxford, UK

sorts (e.g. ℤ) of the
background theory

GFPs(𝑋𝑋 occurs only
positively in 𝜙𝜙)
13

Fixpoint Constraint Solving• Fixpoint constraint 𝜙𝜙 represented by an ℒ-formulais called solvable if ⊨ 𝜙𝜙
• Generalizes CHC Constraint Solving
𝑅𝑅 𝑥𝑥 ⇐ 𝑥𝑥 = 10
𝑅𝑅 𝑥𝑥 − 1 ⇐ 𝑅𝑅 𝑥𝑥 ∧ 𝑥𝑥 > 0⊥ ⇐ 𝑅𝑅 𝑥𝑥 ∧ 𝑥𝑥 < 0

has a solution

2018/7/13⇔⊥⇐

𝜇𝜇𝜇𝜇 𝑥𝑥 .

is solvable

HCVS'18, Oxford, UK

𝑥𝑥 = 10 ∨𝑅𝑅 𝑥𝑥 + 1 ∧ 𝑥𝑥 + 1 > 0∧ 𝑥𝑥 < 014𝑥𝑥Applications to Verification ofLiveness and Existential Properties• Safety verification• 𝜇𝜇Reachable 𝑥𝑥� . 𝜙𝜙 𝑥𝑥� ⇒ ¬Error 𝑥𝑥�

• Termination verification• 𝜈𝜈Diverging 𝑥𝑥� . 𝜙𝜙 𝑥𝑥� ⇒ ¬Init 𝑥𝑥�

• Non-safety verification• ∃𝑥𝑥.
� Error 𝑥𝑥� ∧ 𝜇𝜇Reachable 𝑥𝑥� . 𝜙𝜙 𝑥𝑥�

• Non-termination verification• ∃𝑥𝑥.
� Init 𝑥𝑥� ∧ 𝜇𝜇Diverging 𝑥𝑥� . 𝜙𝜙 𝑥𝑥�
2018/7/13

HCVS'18, Oxford, UK

15

Outline CHC / Fixpoint Constraints for Program Verification
2. CHC Constraint Solving for Relational Verification• Based on [Unno, Torii and Sakamoto, CAV’17]

3. Fixpoint Constraint Solving for Temporal Verification• Based on [Nanjo, Unno, Koskinen and Terauchi, LICS’18]

2018/7/13

HCVS'18, Oxford, UK

16

This WorkCHC Constraint Solving

CHC Constraint Set
Constraint Solving

ReduceSolvable or Not

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

HCVS'18, Oxford, UK

17

Relational Specifications• Specifications that relate
the inputs and outputs of multiple function calls• Equivalence• Invertibility• Non-interference• Associativity• Commutativity• Distributivity• Monotonicity• Idempotency•…

2018/7/13

HCVS'18, Oxford, UK

18

Overall Flow of CHC Constraint
based Program Verification(Functional) Program &Relational Specification
Constraint Generation
CHC Constraint Set
Constraint Solving
Solvable or Not
2018/7/13

HCVS'18, Oxford, UK

19

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)
2018/7/13

HCVS'18, Oxford, UK

20

Overall Flow of CHC Constraint
based Program Verification(Functional) Program &Relational Specification
Constraint Generation
CHC Constraint Set
Constraint Solving
Solvable or Not
2018/7/13

HCVS'18, Oxford, UK

21

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

2018/7/13

let main x y a =assert (mult x y + a= mult_acc x y a)

HCVS'18, Oxford, UK

22

Overall Flow of CHC Constraint
based Program Verification(Functional) Program &Relational Specification
Constraint Generation
CHC Constraint Set
Constraint Solving
Solvable or Not
2018/7/13

HCVS'18, Oxford, UK

23

CHC Constraint Solving• Check the existence of a solution for predicate
variables satisfying all the CHC 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
2018/7/13

HCVS'18, Oxford, UK

QF-LIA
24

Previous Methods for CHC Solving[U.+ ’08,’09, Gupta+ ’11, Hoder+ ’11,’12, McMillan+ ’13,
Rümmer+ ’13, …] (w/o Predicate Pairing [De Angelis+ ’16])

Find a solution expressible in QF-LIA (or QF-LRA)

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

HCVS'18, Oxford, UK

QF-LIA

QF-NIA
25

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

QF-NIA

Analyzed
Analyzed
separately from 𝑄𝑄 separately from 𝑃𝑃

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

2018/7/13

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

HCVS'18, Oxford, UK

26

Our Constraint Solving Method
CHC Constraint Set
Constraint Solving

ReduceInductive
Theorem Proving

Solvable or Not
Simultaneously analyze
multiple predicates byusing mutual invariants
expressed as IHs
2018/7/13

HCVS'18, Oxford, UK

27

Reduction from Constraint Solving
to Inductive Theorem Proving
𝑃𝑃 𝑥𝑥, 0,0 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑥𝑥 + 𝑟𝑟 ⇐ 𝑃𝑃 𝑥𝑥, 𝑦𝑦 − 1, 𝑟𝑟 ∧ 𝑦𝑦 ≠ 0
𝑄𝑄 𝑥𝑥, 0, 𝑎𝑎, 𝑎𝑎 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑟𝑟 ⇐ 𝑄𝑄 𝑥𝑥, 𝑦𝑦 − 1, 𝑎𝑎 + 𝑥𝑥, 𝑟𝑟 ∧ 𝑦𝑦 ≠ 0
𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2 ⇐ 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧ 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2
Prove this by
induction onderivation of
𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1∀𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 , 𝑎𝑎, 𝑠𝑠2 . 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧ 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2 ⇒ 𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2
2018/7/13

HCVS'18, Oxford, UK

28

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

𝐷𝐷 =2018/7/13

𝐷𝐷1
𝐽𝐽3

𝐽𝐽2

𝐷𝐷2

𝐽𝐽1

𝐷𝐷3

𝐷𝐷4
𝐽𝐽4

HCVS'18, Oxford, UK

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

Horn Constraint Solving:

InductionTheorem
hypotheses
and lemmas
Inductive
Proving:

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

2018/7/13

HCVS'18, Oxford, UK

30

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

Unfold Case analysis on the last rule used

HCVS'18, Oxford, UK

31

Case analysis on the last rule used
Unfold2018/7/13

HCVS'18, Oxford, UK

32

2018/7/13

HCVS'18, Oxford, UK

33

Validity checking
Valid2018/7/13

HCVS'18, Oxford, UK

34

2018/7/13

HCVS'18, Oxford, UK

35

Valid2018/7/13

HCVS'18, Oxford, UK

36

2018/7/13

HCVS'18, Oxford, UK

37

2018/7/13

HCVS'18, Oxford, UK

38

Unfold

2018/7/13

Case analysis on the last rule used

HCVS'18, Oxford, UK

39

2018/7/13

HCVS'18, Oxford, UK

40

Valid2018/7/13

HCVS'18, Oxford, UK

41

2018/7/13

HCVS'18, Oxford, UK

42

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

2018/7/13

HCVS'18, Oxford, UK

43

Valid2018/7/13

HCVS'18, Oxford, UK

QED

44

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

2018/7/13

HCVS'18, Oxford, UK

45

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• CHC constraint solvers: provide bit costly but powerfulreasoning about inductive predicates2018/7/13

HCVS'18, Oxford, UK

46

Prototype Constraint Solver• Use Z3 and 𝝁𝝁Z PDR engine respectively
as the backend SMT and CHC 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)
2018/7/13

HCVS'18, Oxford, UK

47

Experiments on IsaPlanner
Benchmark Set• 85 (mostly) relational verification problems of
total functions on inductively defined data structures
Inductive Theorem Prover#Successfully Proved
RCaml
68
Zeno
82 [Sonnex+ ’12]
Support automatic
HipSpec
80 [Claessen+ ’13]
lemma discovery &CVC4goal generalization 80 [Reynolds+ ’15]
ACL2s
74 (according to [Sonnex+ ’12])
IsaPlanner
47 (according to [Sonnex+ ’12])
2018/7/13
HCVS'18, Oxford, UK 45 (according to [Sonnex+ ’12])
48
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

2018/7/13

HCVS'18, Oxford, UK

49

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

2018/7/13

HCVS'18, Oxford, UK

50

Summary of [Unno+ CAV’17]• Proposed an automated verification method combining
CHC 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)• Ongoing work:• Automatic lemma discovery and goal generalization using
invariant synthesis techniques (e.g. Craig interpolation)• Relational program synthesis
2018/7/13

HCVS'18, Oxford, UK

51

Outline CHC / Fixpoint Constraints for Program Verification
 CHC Constraint Solving for Relational Verification
Based on [Unno, Torii and Sakamoto, CAV’17]

3. Fixpoint Constraint Solving for Temporal Verification• Based on [Nanjo, Unno, Koskinen and Terauchi, LICS’18]

2018/7/13

HCVS'18, Oxford, UK

52

Temporal Property Verification
Program?

Temporal property

𝑃𝑃 ⊨ Φ
Check whether 𝑃𝑃 satisfies Φ

2018/7/13

HCVS'18, Oxford, UK

53This Work
Higher-orderfunctional program?

Value-dependent
temporal property

𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ by using(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/13

HCVS'18, Oxford, UK

54

Main Contribution• Foundation for compositional & algorithmic
verification of value-dependent temporal
properties of higher-order programs• cf. previous proposals are:• fully automated but whole program analysis [Kobayashi+
PLDI’11], [U.+ POPL’13], [Kuwahara+ ESOP’14], [Kuwahara+
CAV’15], [Murase+ POPL’16]• compositional but no support of the class of properties[Koskinen+ CSL-LICS’14], [U.+ POPL’18]

2018/7/13

HCVS'18, Oxford, UK

55

This Work
Higher-orderfunctional program?

Value-dependent
temporal property

𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ by using(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/13

HCVS'18, Oxford, UK

56

Example: Functional Program
let rec send_msgs n =emit Send event
if n = 0 then ()else (event[Send]; send_msgs (n-1))

2018/7/13

Generated event sequences:
n < 0 ∶ Send𝜔𝜔 (infinite repetition of Send)
n = 0 ∶ 𝜖𝜖(empty sequence)n = 1 ∶ Sendn = 2 ∶ Send, Send⋮
HCVS'18, Oxford, UK

57

This Work
Higher-orderfunctional program?

Value-dependent
temporal property

𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ by using(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/13

HCVS'18, Oxford, UK

58

This Work?

predicate for finite
event sequencespredicate for infinite
event sequences

𝑃𝑃 ⊨ Φ𝜇𝜇 , Φ𝜈𝜈
Check whether finite event sequences generated
by 𝑃𝑃 satisfy Φ𝜇𝜇 and infinite event sequences
generated by 𝑃𝑃 satisfy Φ𝜈𝜈2018/7/13

HCVS'18, Oxford, UK

59

Example: Value-Dependent
Temporal Property
let rec send_msgs n =if n = 0 then()else(event[Send];
send_msgs (n-1))
n < 0 ∶ Send𝜔𝜔n = 0 ∶ 𝜖𝜖n = 1 ∶ Sendn = 2 ∶ Send, Send⋮
2018/7/13

For terminating
executions⊨

Φ𝜇𝜇 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ ∗ . 𝑥𝑥 = SendnΦ𝜈𝜈 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ 𝜔𝜔 . 𝑥𝑥 = Send𝜔𝜔For diverging
executions

HCVS'18, Oxford, UK

n-times repetitionof Sendinfinite repetitionof Send60

Further Examples• See our LICS’18 paper for further examples that
demonstrate the range of applications

2018/7/13

HCVS'18, Oxford, UK

61

This Work
Higher-orderfunctional program?

Value-dependent
temporal property

𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ by using(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/13

HCVS'18, Oxford, UK

62

Contributions
1. A dependent refinement type & effect system forcompositional & algorithmic temporal verification• Compositional analysis of dependent temporal effects
represented by predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

2. A deductive system for the validity of ℒ

• Use invariants and well-founded relations toover- and under-approximate fixpoints• Designed by transferring ideas from verification research• Can be used with any background first-order theory
2018/7/13

HCVS'18, Oxford, UK

63

Contributions
1. A dependent refinement type & effect system forcompositional & algorithmic temporal verification• Compositional analysis of dependent temporal effects
represented by predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

2. A deductive system for the validity of ℒ

• Use invariants and well-founded relations toover- and under-approximate fixpoints• Designed by transferring ideas from verification research• Can be used with any background first-order theory
2018/7/13

HCVS'18, Oxford, UK

64

First-Order Fixpoint Logic ℒ(revisited)• First-order logic extended with least fixpoints (LFPs)
and greatest fixpoints (GFPs)
predicatevariables

function symbols of
the background theory

predicate symbols of the
background theory

LFPs (𝑋𝑋 occurs only
positively in 𝜙𝜙)

the set of finite
event sequences

GFPs (𝑋𝑋 occurs only
positively in 𝜙𝜙)

the set of infinite
event sequences

We here fix the theory as the one above for temporal effect analysis , though
we could choose any background first-order theory
2018/7/13

HCVS'18, Oxford, UK

65

Temporal Effect Analysis
functional program𝜇𝜇(Φ𝑒𝑒 , Φ𝑒𝑒𝜈𝜈 )𝑒𝑒Example:let rec send_msgs n =if n = 0 then ()else (event[Send]; send_msgs (n-1))
predicate variable that relates 𝑛𝑛 andthe finite event sequence 𝑥𝑥𝜇𝜇Φ𝑒𝑒 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ ∗ . (𝜇𝜇𝑋𝑋𝜇𝜇 𝑛𝑛, 𝑥𝑥 .

dependent temporal effectthat describe the temporal
behavior of 𝑒𝑒

The use of first-order fixpoint logic
allows precise representation(cf. previous work only allowed(𝜔𝜔-)regular expressions [Skalka+’08,
Hofmann+’14] or did not specify theeffect language [Koskinen+’14])

𝑛𝑛 = 0 ∧ 𝑥𝑥 = 𝜖𝜖 ∨𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = 𝐒𝐒𝐒𝐒𝐒𝐒𝐒𝐒 ⋅ 𝑦𝑦 ∧ 𝑋𝑋𝜇𝜇 𝑛𝑛 − 1, 𝑦𝑦)(𝑛𝑛, 𝑥𝑥)Φ𝑒𝑒𝜈𝜈 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ 𝜔𝜔 . (𝜈𝜈𝑋𝑋𝜈𝜈 𝑛𝑛, 𝑥𝑥 . 𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = 𝐒𝐒𝐒𝐒𝐒𝐒𝐒𝐒 ⋅ 𝑦𝑦 ∧ 𝑋𝑋𝜈𝜈 𝑛𝑛 − 1, 𝑦𝑦 )(𝑛𝑛, 𝑥𝑥)predicate variable that relates 𝑛𝑛 andthe infinite event sequence 𝑥𝑥
2018/7/13
HCVS'18, Oxford, UK

66

Dependent Refinement Type & Effect System
Type EnvironmentΓ ⊢ 𝑒𝑒 ∶ (𝜏𝜏 & (Φ𝜇𝜇 , Φ𝜈𝜈 ))Program

Dependent Refinement Type

Dependent Temporal
EffectExtends existing refinement type systems [Koskinen+’14, Rondon+’08, U.+’09, Terauchi’10, …]• Types & effects facilitate compositional analysis of dependent temporal effects• Fixpoint logic deduction ⊩ enables algorithmic type checking

Key typing rules:

Sequential composition of effects
Fixpoints describing a dependent
temporal effect of a recursive function

Subtyping

Check sub-effectrelation via fixpoint
logic deduction

Theorem 1 (Soundness): Γ ⊢ 𝑒𝑒 ∶ 𝜏𝜏 & Φ𝜇𝜇 , Φ𝜈𝜈 implies 𝑒𝑒 ∈ Γ ⊢ 𝜏𝜏 & Φ𝜇𝜇 , Φ𝜈𝜈𝜇𝜇𝜈𝜈(𝑒𝑒 behavesa valuation conforming to Γ) 67
2018/7/13as specified by 𝜏𝜏& Φ , Φ
HCVS'18,under
Oxford, UK

Contributions
1. A dependent refinement type & effect system forcompositional & algorithmic temporal verification• Compositional analysis of dependent temporal effects
represented by predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

2. A deductive system for the validity of ℒ

• Use invariants and well-founded relations toover- and under-approximate fixpoints• Designed by transferring ideas from verification research• Can be used with any background first-order theory
2018/7/13

HCVS'18, Oxford, UK

68

First-Order Fixpoint Logic ℒ(revisited)• First-order logic extended with least fixpoints (LFPs)
and greatest fixpoints (GFPs)
predicatevariables

function symbols of the
background theory

2018/7/13

predicate symbols of the
background theory

LFPs(𝑋𝑋 occurs only
positively in 𝜙𝜙)
HCVS'18, Oxford, UK

sorts (e.g. ℤ) of the
background theory

GFPs(𝑋𝑋 occurs only
positively in 𝜙𝜙)69

Deductive System ⊩ 𝜙𝜙 for
the Validity of ℒ

1. Over- and under-approximate fixpoint subformulas of 𝜙𝜙by non-fixpoint formulas• For soundness, subformulas that occur positively and negatively are
respectively under- and over-approximated

2. Resulting non-fixpoint formulas are discharged by a solver
for the background first-order theory• Techniques for obtaining approximations:Over-Approximation

Under-Approximation

LFP

Invariant (induction)

Well-founded relation

GFP

Well-founded relation

Invariant (co-induction)

Analogous to techniques in safety and liveness property verification
2018/7/13

HCVS'18, Oxford, UK

70

Example: Fixpoint Deduction via
Over-Approx. of LFPCheck that 𝑝𝑝 is a pre-fixpoint of 𝐹𝐹 (or,equivalently, perform induction by
unfolding LFP and applying I.H. to therecursive occurrences of 𝑋𝑋)

Deduction in background first-order theory⊨ 𝑝𝑝 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝑛𝑛⊨ 𝐹𝐹 𝑝𝑝 𝑥𝑥 ⇒ 𝑝𝑝 𝑥𝑥⊩ 𝑝𝑝 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝑛𝑛
𝜇𝜇⊩ Φ𝑒𝑒 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝑛𝑛
Over-approx. of LFP by𝜆𝜆𝜆𝜆 ∈ Σ ∗ . 𝑥𝑥 = Send𝑛𝑛
pre-fixpoint𝜆𝜆𝜆𝜆 ∈ Σ ∗ . 𝜇𝜇𝑋𝑋𝜇𝜇 𝑛𝑛, 𝑥𝑥 . 𝐹𝐹 𝑋𝑋𝜇𝜇 𝑛𝑛, 𝑥𝑥

where 𝐹𝐹 𝑋𝑋 𝑛𝑛, 𝑥𝑥 =2018/7/13

𝑛𝑛, 𝑥𝑥𝑛𝑛 = 0 ∧ 𝑥𝑥 = 𝜖𝜖 ∨𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = Send ⋅ 𝑦𝑦 ∧ 𝑋𝑋 𝑛𝑛 − 1, 𝑦𝑦

HCVS'18, Oxford, UK

71

Example: Fixpoint Deduction via
Over-Approx. of GFPCheck that the given well-founded relation 𝑝𝑝2
witnesses that the given predicate 𝒑𝒑𝟏𝟏 and 𝚽𝚽𝒆𝒆𝝂𝝂 have nointersection (see the paper for details)

Deduction in backgroundfirst-order theory

𝑝𝑝1 𝑛𝑛, 𝑥𝑥 ∧ 𝑛𝑛 ≠ 0 ∧ 𝑥𝑥 = Send ⋅ 𝑥𝑥 ′ ⇒⊨𝑝𝑝1 (𝑛𝑛 − 1, 𝑥𝑥 ′ ∧ 𝑝𝑝2 (𝑛𝑛, 𝑥𝑥, 𝑛𝑛 − 1, 𝑥𝑥𝑥))⋮𝑋𝑋𝜈𝜈 𝑛𝑛, 𝑥𝑥 ; 𝑝𝑝1 ; 𝑝𝑝2 ; ⊤ ↑� 𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = Send ⋅ 𝑦𝑦 ∧ 𝑋𝑋𝜈𝜈 (𝑛𝑛 − 1, 𝑦𝑦)⊩ Φ𝑒𝑒𝜈𝜈 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝜔𝜔𝜆𝜆𝜆𝜆 ∈ Σ𝜔𝜔 . 𝑛𝑛 ≥ 0 ∨ 𝑥𝑥 ≠ Send𝜔𝜔

𝜆𝜆 𝑛𝑛1 , 𝑥𝑥1 , 𝑛𝑛2 , 𝑥𝑥2 . 𝑛𝑛1 > 𝑛𝑛2 ≥ 0
2018/7/13

𝜆𝜆𝜆𝜆 ∈ Σ𝜔𝜔 .

𝜈𝜈𝑋𝑋𝜈𝜈 𝑛𝑛, 𝑥𝑥 . 𝑛𝑛 ≠ 0 ∧HCVS'18, Oxford, UK⊨ ¬𝑝𝑝1 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝜔𝜔⊩ ¬𝑝𝑝1 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝜔𝜔Over-approx. of GFP by
negation of 𝑝𝑝1∃𝑦𝑦. 𝑥𝑥 = Send ⋅ 𝑦𝑦 ∧𝑋𝑋𝜈𝜈 𝑛𝑛 − 1, 𝑦𝑦

𝑛𝑛, 𝑥𝑥72

Deductive System ⊩ 𝜙𝜙 for ℒ

Over-approximation of
LFP (induction)

Backgroundfirst-ordertheory solver

Approximation of fixpoints
using well-founded relation(the next slide)

Under-approximation of
GFP (co-induction)𝜓𝜓 represents a fixpoint-free formula.

𝑛𝑛𝑛𝑛𝑛𝑛(𝜓𝜓) is negation normal form of 𝜓𝜓.
𝐶𝐶 + (resp. 𝐶𝐶 − ) is positive (resp. negative) context.

Theorem 2 (Soundness of ⊩): ⊩ 𝜙𝜙 implies ⊨ 𝜙𝜙2018/7/13

HCVS'18, Oxford, UK73

Fixpoint Approximation Rules
based on Well-Founded Relation
Dual

Under-approximation of LFPOver-approximation of GFP

Lemma: Suppose that 𝜓𝜓 is in negation normal form, 𝑋𝑋 is not free in 𝜓𝜓′and 𝑝𝑝2 is a well-founded relation. We have:• 𝑋𝑋 𝑥𝑥� ; 𝑝𝑝1 ; 𝑝𝑝2 ; 𝜓𝜓 ′ ↓ 𝜓𝜓 implies 𝑝𝑝1 𝑥𝑥� ⇒ (𝜇𝜇𝜇𝜇 𝑥𝑥� . ¬𝜓𝜓 ′ ∨ 𝜓𝜓)(𝑥𝑥)�′ ∧ 𝜓𝜓 𝑥𝑥• 𝑋𝑋2018/7/13
𝑥𝑥� ; 𝑝𝑝1 ; 𝑝𝑝2 ; 𝜓𝜓 ′ ↑� 𝜓𝜓 implies HCVS'18,
𝜈𝜈𝜈𝜈 𝑥𝑥�Oxford,. 𝜓𝜓UK� ⇒ ¬𝑝𝑝1 (𝑥𝑥)�74

Summary of [Nanjo+ LICS’18]• Foundation for compositional & algorithmic verification of valuedependent temporal properties of higher-order programs
1. Dependent refinement type & effect system

2.

• Compositional analysis of dependent temporal effects represented by
predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

Deductive system for the validity of ℒ
Over-Approximation

Under-Approximation

LFP

Invariant (induction)

Well-founded relation

GFP

Well-founded relation

Invariant (co-induction)• Can be used with any background first-order theory• Ongoing Work

• Automation and implementation• Extensions to branching- and relational-properties verification

2018/7/13

HCVS'18, Oxford, UK

75

Outline CHC / Fixpoint Constraints for Program Verification
 CHC Constraint Solving for Relational Verification
Based on [Unno, Torii and Sakamoto, CAV’17]

 Fixpoint Constraint Solving for Temporal Verification
Based on [Nanjo, Unno, Koskinen and Terauchi, LICS’18]

2018/7/13

HCVS'18, Oxford, UK

76

Conclusion• Fixpoint constraint solving generalizes CHC solving• Significantly widen the range of applications to verification of
liveness and existential properties• Inductive theorem proving techniques
facilitate (relational) CHC solving, and vice versa• Safety and liveness verification techniques (invariants andwell-founded relations) facilitate fixpoint constraint solving• Future Work• Fixpoint constraint solving based on inductive and co-inductive
theorem proving for verification of temporal relational properties(e.g. trace equivalence) and hyperproperties [Clarkson+ ’09]

2018/7/13

HCVS'18, Oxford, UK

77