Higher-order Program Verification as Refinement Type Inference

Higher-order Program Verification as Refinement Type Inference

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

Recently Viewed Presentations

  • Wcla Mcle 7-9-13

    Wcla Mcle 7-9-13

    The Venure-Newberg-Perini v. IWCC2010 MR 509. Circuit Court Seventh Judicial Circuit, Sangamon County, 8-28-11. Undisputed facts "Misapplied the law to the facts…decision of the Commission is improper as a matter of law…decision of Arbitrator denying the claim is reinstated."
  • Organic Chemistry

    Organic Chemistry

    Naming Alkenes & Alkynes Change suffix from -ane to -ene for base name of the alkene, or to -yne for base name of the alkyne. Number chain from end closest to the multiple bond. Number in front of main name...
  • Welcome to ELA 7! - Clarence High School

    Welcome to ELA 7! - Clarence High School

    Welcome to ELA 7 Mrs. Lynn Elibol Routines: Daily Warm-up - Writing Prompts each day completed in the writer's notebook Homework Review with whole class or small groups Class instruction and guided practice ... (Lucy Calkins) Technology Miscellaneous ...
  • Productive GPU Software This conference uses integrated audio.

    Productive GPU Software This conference uses integrated audio.

    Productive GPU Software. This conference uses integrated audio. To interact with the host, you need a working microphone and speakers. To speak, please click on the "Raise Hand" button in the Participants box.
  • CITI Course Site Updates Paul Braunschweiger Ph.D. Update

    CITI Course Site Updates Paul Braunschweiger Ph.D. Update

    Pre- and post-course completion surveys can be set up to collect feedback from learners. Automatic Downloads for Institutional Administrators- Record Set Formats Available (comma or tab-delimited files) All completion reports earned at the institution since ~January 2006 (+/- module names...
  • Interlude - Artistic Revolution #1 Greek Art Greek

    Interlude - Artistic Revolution #1 Greek Art Greek

    Everything that is important about a figure is included a facial profile, but eyes from the front the instep of a foot (both are left here) square shoulders Portrait of Hesire, Egyptian, ~2770 B.C. a wooden door Portrait of Head,...
  • North Staffs Mood Pathway Update. 20/09/2012

    North Staffs Mood Pathway Update. 20/09/2012

    Providing structure to previously informal service. Inclusion within ASU standardised 72 hour monitoring paperwork. ASU exceeding ASI target 40% significantly. ESD / rehab unit screening 100% of patients. Improved handover re: mood issues / management between services / links with...
  • Definite and Indefinite Articles

    Definite and Indefinite Articles

    Definite and Indefinite Articles P. 60 Realidades 1 Definite Articles El , La , Los and Las are called definite articles. Definite Articles In English they mean "the" Definite Articles We use El and Los with masculine nouns and La...