Higher-order Program Verificatio n as Refinement Type Inference Hiroshi Unno (University of Tsukuba) Joint work with: Naoki Kobayashi, Tachio Terauchi, Ryosuke Sato, Takuya Kuwahara, Kodai Hashimoto, Sho Torii 2015/7/4 HOPA 2015 1 Path-Sensitive Verifiers for H.O. Programs (cf. SLAM, BLAST, for Imperative Programs) Refinement Caml [Unno+ FLOPS08, PPDP09, POPL13, TACAS15, SAS15, ] MoCHi [Kobayashi+ PLDI11, PEPM13, ESOP14, ESOP15, PEPM15, CAV15, ] Liquid Types [Jhala+ PLDI08, PLDI09, CAV10, , ESOP13, ICFP14, ] Depcegar [Terauchi POPL10] HMC [Jhala, Majumdar & Rybalchenko CAV11]

Popeye [Zhu & Jagannathan VMCAI13] Program & Spec. let rec mc x = if x > 100 then x 10 else mc (mc (x + 11)) in let n = randi() in if n 101 then assert (mc n = 91) 2015/7/4 Result Certificate or Counterexample Verifier HOPA 2015 2 MoCHi: Software Model Checker for Highe r-Order Functional Programs Automatically prove/disprove safety and liveness

properties of high-level programs High-level control structures: higher-order functions and exceptions High-level data structures: algebraic data types and multidimensional arrays Absence of assertion failures, pattern matching errors, uncaught exceptions, array bounds errors, Termination for all / Nontermination for some inputs (ongoing extension to omega-regular properties) 2015/7/4 HOPA 2015 3 Path-Sensitive Verifiers for H.O. Programs (cf. SLAM, BLAST, for Imperative Programs) Refinement Caml [Unno+ FLOPS08, PPDP09, POPL13, TACAS15, SAS15, ] MoCHi [Kobayashi+ PLDI11, PEPM13, ESOP14, ESOP15, PEPM15, CAV15, ]

Liquid Types [Jhala+ PLDI08, PLDI09, CAV10, , ESOP13, ICFP14, ] Depcegar [Terauchi POPL10] HMC [Jhala, Majumdar & Rybalchenko CAV11] Popeye [Zhu & Jagannathan VMCAI13] Program & Spec. All these verifiers are based on Result refinement type system Certificate or (cf. Hoare logic for first-order Counterexample Verifier imperative programs) let rec mc x = if x > 100 then x 10 else mc (mc (x + 11)) in let n = randi() in if n 101 then

assert (mc n = 91) 2015/7/4 HOPA 2015 4 Refinement Types [Freeman & Pfenning PLDI91][Xi & Pfenning PLDI98, POPL99] Non-negative integers FOL formulas (e.g. QFLIA) for type refinement Functions that take an integer and return an integer not less than Soundness of refinement type system : is safe (i.e., ) if is well-typed (i.e., ) 2015/7/4 HOPA 2015

5 Example: Refinement Type Checking , = = = + sum x = if x = 0 then 0 else x + sum (x - 1) main a = assert (sum a >= a) Automated H.O. Verification as Type Inference: Input: Output: such that 2015/7/4 HOPA 2015 6 Refinement Type Inference via Horn Constraint Solving [U.&Kobayashi FLOPS08,PPDP09] Refinement Types

sum x = if x = 0 then 0 else x + sum (x - 1) main a = assert (sum a >= a) Program + Spec. { Horn Clause Constraint Generator Horn Clauses Solution: = = ( , ) , ( , ) ( , ) , = + ( , ) 2015/7/4 HOPA 2015 sat

} Horn Clause Constraint Solver unsat Counter example 7 Horn Constraint Solving Techniques Quantifier elimination [U. & Kobayashi FLOPS08] Predicate abstraction [Rondon+ PLDI08] Craig interpolation [U.+ PPDP09, PEPM13][Terauchi POPL10] [McMillan & Rybalchenko13] Tree interpolation [Gupta+ POPL11, APLAS11] [Hoder+ CAV11] [Rummer+ CAV13][Terauchi & U. ESOP15][U. & Terauchi TACAS15] Template-based synthesis [Hashimoto & U. SAS15] 2015/7/4

HOPA 2015 8 Refinement Type System as Axiomatic Seman tics of H.O. Functional Programs Imperative Axiomatic Semantics Hoare Logic of of Partial Correctness Partial Correctness Axiomatic Semantics of Total Correctness Hoare Logic of Total Correctness Axiomatic Semantics of Angelic Nondeterminism Predicate Transformer Semantics Hoare Logic of Angelic Nondet.

2015/7/4 [Mamouras FoSSaCS15] Weakest Precondition Generation HOPA 2015 H.O. Functional ? ? ? Horn Clause Constraint Generation [U. & Kobayashi PPDP09] 9 Refinement Type System as Axiomatic Semantics of H.O. Functional Programs Imperative Axiomatic Semantics Hoare Logic of of Partial Correctness Partial Correctness

H.O. Functional Relatively Complete Refinement Type System [U., Terauchi & Kobayashi POPL13] Axiomatic Semantics of Total Correctness Hoare Logic of Total Correctness Axiomatic Semantics of Angelic Nondeterminism Predicate Transformer Semantics Hoare Logic of Angelic Nondet. 2015/7/4 [Mamouras FoSSaCS15]

Weakest Precondition Generation HOPA 2015 ? ? Horn Clause Constraint Generation [U. & Kobayashi PPDP09] 10 Limitation of Refinement Type System Incompleteness: There is a safe but untypable program whereas Hoare logic is relatively complete 2015/7/4 HOPA 2015 11 Example: Safe and Typable Program

( : ) {=} Well-typed! ( : )({= } ) = ( { = } ) {= } 2015/7/4 HOPA 2015 12 Example: Safe but Untypable Program Refinement predicate for the 1st arg. of Cannot depend on ( {|()} ) : {|()} Refinement predicate for

= { = } Untypable because: there is no s.t. 2015/7/4 HOPA 2015 13 Our Contributions Relatively complete extension of ordinary refinement type system Type inference method for 2015/7/4 HOPA 2015 14 Our Contributions Relatively complete extension of

ordinary refinement type system Type inference method for for any safe program given an oracle for validity of formulas of Peano arithmetic 2015/7/4 HOPA 2015 15 Our Design Goal of Easy to automate type checking & inference By exploiting techniques from first-order automated theorem proving (e.g., interpolation, SMT) Rejected alternative designs: Refinement predicates on functions (cf. Coq) Unrestricted use of quantification (cf. Dependent ML) 2015/7/4 HOPA 2015 16

Our Approach: Restricted Use of Quantification Add one universal quantifier over integer just before each function parameter [Goerdt 1985, German, Clarke, and Halpern 1983, 1989] . ( { ( , ) } ) { ( , ) } = A quantifier instantiation for 2015/7/4 HOPA 2015 17 Example: Typing under ( , }) .( ({ { = { { = . ( , }) }

) } = [ ] Well-typed! 2015/7/4 { |= } { |= } HOPA 2015 18 Theorem: Relative Completeness of A program is safe There exists a substitution for ?s such that 2015/7/4 HOPA 2015

19 Our Contributions Relatively complete extension of ordinary refinement type system Type inference method for 2015/7/4 HOPA 2015 20 Refinement Type Inference for Find a substitution for all as well as a type environment such that = 2015/7/4 HOPA 2015 21 Reduction to Quantified

Horn Constraint Solving . ( { ( , ) } ) { ( , ) } = ( : ) { : = } , . 2015/7/4 { , . ( ( , ) ( , )) , . . . HOPA 2015 ( ( ( , ) = ) ) ( , ) 22 }

Quantified Horn Constraint Solving (1/3) , . . . ( ( + , ) = ) , Skolemize , . ( + , ) } } . . ( ( + , ) = ) , . , . ( + , ) } , . Elim. Elim.

2015/7/4 { { , . ( ( , ) ( , )) , ( ( , ) = ) . . . ( ( , ) ) , . ( ( , ) ( , )) , {

, . , . ( = = ) HOPA 2015 23 Quantified Horn Constraint Solving (2/3) , . , . ( = = ) to , . , . ( ) = SMT Solver Farkas lemma: if , 2015/7/4 = HOPA 2015 24

Quantified Horn Constraint Solving (3/3) ( , }) ( ,}) .( ({ { = { { = . } ) } = , .( ( , ) ( , )) , , . . . ( ( , ) = ) , .( , ) { } Horn Clause Constraint Solver 2015/7/4

HOPA 2015 25 Refinement Type System as Axiomatic Seman tics of H.O. Functional Programs Imperative Axiomatic Semantics Hoare Logic of of Partial Correctness Partial Correctness H.O. Functional Relatively Complete Refinement Type System [U., Terauchi & Kobayashi POPL13] Axiomatic Semantics of Total Correctness Hoare Logic of Total Correctness ? Axiomatic Semantics of Angelic

Nondeterminism Predicate Transformer Semantics Hoare Logic of Angelic Nondet. Refinement Type System of Angelic Nondet. [Mamouras FoSSaCS15] [Hashimoto & U. SAS15] Weakest Precondition Generation Horn Clause Constraint Generation 2015/7/4 HOPA 2015

[U. & Kobayashi PPDP09] 26 Refinement Type System of Angelic Nondeterminism [Hashimoto & U. SAS15] Model nondeterministic behaviors in program s user inputs, inputs from communication channels, interrupts, and thread schedulers Verify branching time properties of programs non-termination verification [Kuwahara+ CAV15] Proving that a program does NOT terminate for some inputs 2015/7/4 HOPA 2015 27 Example: Non-Termination Verification sum x = if x = 0 then 0 else x + sum (x - 1) main () = let x = read_int () in sum x; assert false sum does NOT terminate for some inputs

a winning strategy for the user such that 2015/7/4 HOPA 2015 28 Typing Rules of for Nondeterminism [Hashimoto & U. SAS15] Rule for Demonic Nondeterminism: For some integers , has Rule for Angelic Nondeterminism: under 2015/7/4 HOPA 2015 29 Example: Refinement Type Checking , <

= + < = = < < sum x = if x = 0 then 0 else x + sum (x - 1) main () = let x : = in sum x; assert false . < 2015/7/4 HOPA 2015 30 Refinement Type Inference for Find a substitution for all as well as a type environment such that sum x = if x = 0 then 0 else x + sum (x - 1) main () = let x : = in sum x; assert false

2015/7/4 HOPA 2015 31 Reduction to Quantified Horn Constraint Solving sum x = if x = 0 then 0 else x + sum (x - 1) main () = let x : = in sum x; assert false ( ) ( , ) , ( ) ( ) , , , . ( ) ( , ) ( , + ) , , , . ( ) ( ) , . ( ), ( ) ( , ) { 2015/7/4 HOPA 2015 32

} Quantified Horn Constraint Solving : (:( : { : ) )} : {:{ : ( )< } ) } {) : ( , sum x = if x = 0 then 0 else x + sum (x - 1) main () = let x : = in sum x; assert false ( ) ( , ) , ( ) ( ) , , , . ( ) ( , ) ( , + ) , , , . ( ) ( ) , . ( ), ( ) ( , ) { Quantified Horn

Constraint Solver 2015/7/4 HOPA 2015 33 } Refinement Type System as Axiomatic Seman tics of H.O. Functional Programs Imperative Axiomatic Semantics Hoare Logic of of Partial Correctness Partial Correctness H.O. Functional Relatively Complete Refinement Type System [U., Terauchi & Kobayashi POPL13] Axiomatic Semantics of Total Correctness Hoare Logic of Total Correctness

Refinement Type System of Total Correctness Axiomatic Semantics of Angelic Nondeterminism Predicate Transformer Semantics Hoare Logic of Angelic Nondet. Refinement Type System of Angelic Nondet. [Mamouras FoSSaCS15] [Hashimoto & U. SAS15] Weakest Precondition Generation Horn Clause

Constraint Generation 2015/7/4 HOPA 2015 [U., Hashimoto & Torii 15] [U. & Kobayashi PPDP09] 34 Refinement Type System of Total Correctness [U., Hashimoto & Torii 15] Verify the termination in addition to the partial correctness of programs sum x = if x = 0 then 0 else x + sum (x 1) 2015/7/4 HOPA 2015 35 Example: Refinement Type Checking

sum x = if x = 0 then 0 else x + sum (x - 1) ( , ) 2015/7/4 HOPA 2015 36 Refinement Type Inference for Find a well-founded relation for all recursive function as well as a type environment such that sum x = if x = 0 then 0 else x + sum (x - 1) 2015/7/4 HOPA 2015 37

Reduction to Constraint + Horn Constraint Solving sum x = if x = 0 then 0 else x + sum (x - 1) : { : ( ) } . . . 2015/7/4 ( ) ( ) , ( ) ( , ) { HOPA 2015 } 38 Constraint + Horn Constraint Solving [Popeea & Rybalchecnko TACAS12][Kuwahara+ ESOP14, ] : { :

( ) } sum x = if x = 0 then 0 else x + sum (x - 1) ( ) ( ) , . . . ( ) ( , ) { { . . .

Quantified Horn Constraint Solver 2015/7/4 ( ) ( ) , ( ) ( ) > ( ) ( )= HOPA 2015 39 } } Summary: H.O. Program Verification as Refin ement Type Inference (Incomplete) (Incomplete) Partial Partial Correctness Correctness Partial Correctness Partial Correctness Total Correctness

Total Correctness Angelic Nondeterminism Angelic Nondeterminism 2015/7/4 Type System Type Inference Ordinary Refinement Type System Relatively Complete Refinement Type System Horn Horn Clause Clause Constraint Constraint Solving Solving Refinement Type System of Total Correctness [U.,

Constraint + Quantified Horn Constraint Solving Quantified Horn Constraint Solving [U., Terauchi & Kobayashi POPL13] Hashimoto&Torii 15] Refinement Type System of Angelic Nondet. Quantified Horn Constraint Solving [Hashimoto & U. SAS15] HOPA 2015 40