Verification of Higher-Order Non-deterministic Programs with Refinement Types

relatively complete refinement type system n.w
1 / 42
Embed
Share

Explore a novel dependent refinement type system for verifying higher-order non-deterministic programs, ensuring safety, termination, and more. Learn about universal and existential reasoning, meta-theoretic properties, and the extension of type systems with qualified types.

  • Verification
  • Refinement Types
  • Higher-Order Programs
  • Non-deterministic
  • Meta-theoretic

Uploaded on | 0 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

E N D

Presentation Transcript


  1. Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs Hiroshi Unno (University of Tsukuba) Yuki Satake (University of Tsukuba) Tachio Terauchi (Waseda University) POPL'18, Los Angeles, United States 1

  2. Background Recent advances in (semi-)automated methods for verifying higher-order functional programs safety [Rondon+ 08; U. & Kobayashi 08, 09; Terauchi 10; Ong & Ramsay 11; Jhala+ 11; Kobayashi+ 11; U.+ 13; ] termination [Sereni & Jones 05; Giesl+ 11; Kuwahara+ 14; Vazou+ 14] non-termination [Kuwahara+ 15; Hashimoto & U. 15] temporal properties [Koskinen & Terauchi 14; Murase+ 16] Different techniques are used to verify the different classes of properties, and are hard to combine in a unified framework dependent refinement types, predicate abstraction for higher-order model checking, program transformation for (binary) reachability analysis, POPL'18, Los Angeles, United States 2

  3. Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 3

  4. Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 4

  5. Dependent Refinement Types ? predicates on ? ??? | ? ? Non-negative integers program values ? ??? {? ??? | ? ?} Functions that take an integer ? and (if terminated) return ? not less than ? A type system ensures that a type-checked expression behaves according to the type Only universal branching properties can be expressed POPL'18, Los Angeles, United States 5

  6. Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 6

  7. Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 7

  8. Qualified Types ????? ?? , (universal/existential non-det.) specifies whether the expression being typed behaves according to the type: for any non-det. evaluation (??= ), or for some non-det. evaluation (??= ) ?? , (partial/total correctness) specifies whether: ? holds for all value obtained (??= ), or there exists a final value for which ? holds (??= ) POPL'18, Los Angeles, United States 8

  9. Qualified Types ????? ?? , (universal/existential non-det.) specifies whether the expression being typed behaves according to the type: for any non-det. evaluation (??= ), or for some non-det. evaluation (??= ) ?? , (partial/total correctness) specifies whether: the evaluation diverges or ? is satisfied (??= ), or the evaluation terminates and ? is satisfied (??= ) POPL'18, Los Angeles, United States 9

  10. Examples: Qualified Types ????? ? ? ??? ? > ? for any non-deterministic evaluation of ?, if any integer ? is obtained, then ? is positive ? ? ??? ? > ? for some non-deterministic evaluation of ?, some integer ? is obtained, and ? is positive POPL'18, Los Angeles, United States 10

  11. Typing Integer Constants Integer constant Rule: ? ? ? ??? ? = ? Type Universal and Total environment POPL'18, Los Angeles, United States 11

  12. Converting Qualified Types Subtyping Rule: ???? ???? ? ??< ?? ???? ???? ? ?? < ?? Universal and Partial Universal and Total Existential and Partial Existential POPL'18, Los Angeles, United States and Total 12

  13. Typing Let-Bindings Rule: ???? ? ?? ?? ???? ?,? ?? ?? ?? ? ??? ? = ?? ?? ?? ?? ? ??? ?? ???? POPL'18, Los Angeles, United States 13

  14. Typing Recursive Functions for Partial Correctness Rule: ? ? ?? ? ?,? ??,? ? ?? ?? ? ??? ?,?,? ? ?? ?? ? (recursive) function ??? ??? ? ? = ? POPL'18, Los Angeles, United States 14

  15. Typing Recursive Functions for Total Correctness (cf. [Xi 01]) Well-founded relation witnessing the termination of ?, as a recursion guard Rule: ? ????= ? :?? ? ?? ? =? ? ?? ?? ? ?? ? ?,? .? ?,? ??,? ???? ? ?? ? ??? ?,?,? ? ?? ?? Example: ? ? ? ? ,??? ???? ?? ? = ? ???? ? ???? ??? ?? ? ?,? .? > ? ? ??? ???,?,?? ? = ? ???? ? ???? ? + ??? ? ? ? ? ? > ? ? ? ? ? ? ? ? ? ? ??? ? ? ? ? POPL'18, Los Angeles, United States 15

  16. Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 16

  17. Qualified Bindings ??? Occur in type environments and the argument of dependent function types ? , specifies whether a certain fact must hold for: any input ? that satisfies ? (? = ), or some input ? that satisfies ? (? = ) POPL'18, Los Angeles, United States 17

  18. Examples: Qualified Bindings ??? ? ??? ? ??? ? > ? functions that, for any integer ? and for any run with the argument ?, return some integer ?, which is greater than ? ? ??? ? ??? ? > ? functions that, there exists an integer ?, for any run with the argument ?, return some integer ?, which is greater than ? POPL'18, Los Angeles, United States 18

  19. Skolemizing Existential Bindings Rule: Skolemization Predicate ?,? : ? ? ?,? : ?,?,? ? ? ?,? : ?,? ? ? Type environment consisting of only -bindings Type environment consisting of both - and -bindings Example: ? : ???,? : ??? ? = ? ? : ???,? : ???,? = ? ? + ? ? ? = ? ? : ???,? : ??? ? + ? ? ? = ? POPL'18, Los Angeles, United States 19

  20. Typing Non-deterministic Choice Rule: ?,? ????? ? ????? ? ??? ? = ?? ? ????? ? ??? ? Example: ? ???,? ??? ? + ? ? ? = ? ? ??? ??? ? = ?? ? + ? ? ? = ? POPL'18, Los Angeles, United States 20

  21. Typing Function Applications (Universal Bindings) Rule: ? ?? ? : ? ? ? ?? ?? [??/?]? ? ?? ? POPL'18, Los Angeles, United States 21

  22. Typing Function Applications (Existential Bindings) Rule: Observational equivalence ? ?? ? ? ? ?,? ?? ?? [??/?]? ?,? ?,? ? ?? Example: ? ? ? ? ? ?,? ???,? ??? ? = ? ? ?,? ??? ? ? ? ? ? ??? ? = ?? ? ? ? ? : ??? ? POPL'18, Los Angeles, United States 22

  23. Converting Function Types (1/4) Subtyping Rule: ?,? ?? ??< ?? ? ??< ?? ? ? ?? ??< ? ?? ?? Example: ? ??? ? ? = ? < ? ? ? ? ? ? ? POPL'18, Los Angeles, United States 23

  24. Converting Function Types (2/4) Subtyping Rule: ?,? ?? ??< ?? ? ??< ?? ? ? ?? ??< ? ?? ?? Example: ? ? ? ? < ? ??? ? ? ? ? ? = ? POPL'18, Los Angeles, United States 24

  25. Converting Function Types (3/4) Subtyping Rule: ? ? < ?? ?,? ? ??< ?? ? ? ?? ??< ? ?? ?? ? ? < ?? Example: ? ? ? < ??? ? ? ? ? ? ? = ? < ? ? = ? ? ??? ? ? = ? < ? ??? ? ? = ? ? ? ? < ??? POPL'18, Los Angeles, United States 25

  26. Converting Function Types (4/4) Subtyping Rule: ?,? ?? ??,? ?? ?? ? ? ?,? ?? ?? ??< ?? ?,? ?? ?? ??< ?,? ?? ?? < ?? ? ? ?? ??< ? ?? ?? Example: Observational equivalence ? ? ? = ? < ? ? ? = ? ? ? = ? ? ? = ? POPL'18, Los Angeles, United States 26

  27. Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 27

  28. Gdel Encoding of Function-Type Values Enables predicates of the underlying logic ? (e.g., second-order arithmetic) to depend on function-type arguments encoded as ?-objects ? ??? ??? ? ??? ??? ? ? ? Functions that, given two terminating functions ? and ?, always diverge if ? is not observationally equivalent to ? POPL'18, Los Angeles, United States 28

  29. Guarded Intersection Types ??? ?? ???? Collectively express different behaviors of functions depending on the arguments ? > ? ??? ? < ? ? ? = ? ??? ? = ? ? Functions that, given the argument ? : always terminate if ? > ?, always diverge if ? < ?, and otherwise, non-deterministically terminate or diverge ? : ??? POPL'18, Los Angeles, United States 29

  30. Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 30

  31. Complement Types ? Thanks to having both modes of non-determinism, the type complement operator can be defined: ????? ? ? ??? ? ? ??? ? ? ?? ? ? : ?? ? ?? ?? POPL'18, Los Angeles, United States 31

  32. Example: Complement Types ? ? ? ??? ? ??? ? = ? functions that, for any integer ? and for any run with the argument ?, diverge or return an integer ? = ? ? = ? ??? ? ??? ? ? functions that, for some integer ? and for some run with the argument ?, terminate and return an integer ? ? POPL'18, Los Angeles, United States 32

  33. Example: Combined Reasoning (Non-safety via Termination) Goal: prove that ??? ??? ? ? ? = ?? ? = ? ???? ? ???? ? ? ? ? ??? ? = ? ??? ? ?? ??? ? = ?? ? + ? violates ? ? = ? POPL'18, Los Angeles, United States 33

  34. Example: Combined Reasoning (Non-safety via Termination) Goal: prove that ??? ??? ? ? ? = ?? ? = ? ???? ? ???? ? ? ? ? ??? ? = ? ??? ? ?? ??? ? = ?? ? + ? satisfies ? ? = ? POPL'18, Los Angeles, United States 34

  35. Example: Combined Reasoning (Non-safety via Termination) Goal: prove that ??? ??? ? ? ? = ?? ? = ? ???? ? ???? ? ? ? ? ??? ? = ? ??? ? ?? ??? ? = ?? ? + ? satisfies ? ? ? 1. Show that ? is conditionally terminating: The well-founded relation ? ?,? , ? ,? . ? > ? ? = ? ? ? witnesses that ? has the type: ? ??? ? ? ? ? 2. Show that the actual call ? ??? ? always terminates by checking ? ??? 3. Show that, for any integer ?, we can choose an integer ? such that ? + ? ? ??? Q.E.D. POPL'18, Los Angeles, United States 35

  36. Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 36

  37. Closure of Types under Complement For any type ? refining a simple type ?, ? ? = and ? ? = ? where ? : the set of expressions that behave according to ? ? : the set of expressions of the type ? POPL'18, Los Angeles, United States 37

  38. Soundness ? ? ? implies ? ? ? the set of expressions that behave according to ? under any valuation conforming to ? POPL'18, Los Angeles, United States 38

  39. Relative Completeness ? ? implies ? ? under the assumption that the underlying logic is sufficiently expressible to G del encode arbitrary functions definable in the target programming language to represent well-founded relations witnessing the termination of the definable functions POPL'18, Los Angeles, United States 39

  40. Summary Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 40

  41. Future Work Extensions with temporal specifications: Temporal trace specs. (e.g., LTL) Branching temporal specs. (e.g., CTL, modal-?) Extensions with language features: Recursive data structures Linked data structures Call-by-name evaluation Probabilistic choice Automation of type checking and inference POPL'18, Los Angeles, United States 41

  42. Towards Automation (Ongoing) Type Checking How to leverage off-the-shelf SMT solvers? Abstraction and counterexample guided refinement for the encoding of function-type values Type Inference How to synthesize inductive invariants, well-founded relations, and Skolemization predicates? Reduction to existentially-quantified Horn clause and well-foundedness constraints How to achieve scalable inference? Combination of universal and existential reasoning POPL'18, Los Angeles, United States 42

Related


More Related Content