Language-Integrated Verification
Ranjit Jhala
[PDF]
1.
Follow Along at This URL
1.1.
Whats this?
1.2.
The First
Bug
1.3.
Fast forward to Present Day
1.4.
Fast forward to Present Day
1.5.
Fast forward to Present Day
1.6.
Programming Languages Research
1.7.
Modern Languages
1.8.
Modern Languages
1.9.
Modern Languages
1.10.
Modern Languages?
1.11.
Well-typed programs can go very wrong!
1.12.
Well-typed programs can go very wrong!
1.13.
Well-typed programs can go very wrong!
1.14.
Goal: Language-Integrated Verification
1.15.
Goal: Language-Integrated Verification
1.16.
Outline
1.17.
Outline
1.18.
Outline
1.19.
Outline
1.20.
Outline
1.21.
Outline
2.
Simple Refinement Types
2.1.
Types
2.2.
Predicates
2.3.
Predicates
2.4.
Predicates
2.5.
Predicates
2.6.
Predicates
2.7.
Example: Singletons
2.8.
Example: Natural Numbers
2.9.
A Term Can Have
Many
Types
2.10.
1. Predicate Subtyping
[NUPRL, PVS]
2.11.
1. Predicate Subtyping
[NUPRL, PVS]
2.12.
1. Predicate Subtyping
[NUPRL, PVS]
2.13.
Example: Natural Numbers
2.14.
Example: Natural Numbers
2.15.
2. Typing Applications (Function Calls)
2.16.
2. Typing Applications (Function Calls)
2.17.
2. Typing Applications (Function Calls)
2.18.
2. Typing Applications (Function Calls)
2.19.
Recap: Refinement Types 101
2.20.
Recap: Refinement Types 101
2.21.
Recap: Refinement Types 101
2.22.
Outline
2.23.
Outline
3.
Refinement Types by Example
3.1.
Refinement Types by Example
3.2.
Refinement Types by Example
3.3.
Refinement Types by Example
3.4.
Specifications: Pre-Conditions
3.5.
Specifications: Post-Conditions
3.6.
Refinement Types by Example
3.7.
Verification: Vector Sum
3.8.
Verification: Vector Sum
3.9.
Verification: Vector Sum
3.10.
Refinement Types by Example
3.11.
Inference
3.12.
Inference: Vector Sum
3.13.
Inference: Vector Sum
3.14.
Inference: Vector Sum
3.15.
Inference: Vector Sum
3.16.
Inference: Vector Sum
3.17.
Inference: Vector Sum
3.18.
Refinement Types by Example
3.19.
Collections & Higher-Order Functions
3.20.
Collections & Higher-Order Functions
3.21.
Collections & Higher-Order Functions
3.22.
Collections & Higher-Order Functions
3.23.
Refinement Types by Example
3.24.
Example: List
average
3.25.
Refinements for Datatypes
3.26.
Measures Yield Refined Constructors
3.27.
Example:
map
over Lists
3.28.
Refinements for Datatypes
3.29.
Refinements for Datatypes
3.30.
Refinements for Datatypes
3.31.
Refinement Types by Example
3.32.
Outline
3.33.
Outline
4.
Invariants In Constructors
4.1.
Invariants In Constructors
4.2.
Invariants In Constructors
4.3.
Invariants In Constructors
4.4.
Abstracting Refinements
4.5.
Abstracting Refinements
4.6.
Abstracting Refinements
4.7.
Using Abstract Refinements
4.8.
Recap
4.9.
Recap
4.10.
Bounded Refinements: Induction as a Type
4.11.
Bounded Refinements: Induction as a Type
4.12.
Bounded Refinements: Induction as a Type
4.13.
Bounded Refinements: Induction as a Type
5.
Avoiding Infinite Loops
5.1.
Example: Proving Termination of
sum
5.2.
Proving Termination
5.3.
Proving Termination
5.4.
Proving Termination
5.5.
Proving Termination
5.6.
Example: Proving Termination of
sum
5.7.
User Specified Termination Metrics
5.8.
User Specified Termination Metrics
5.9.
User Specified Termination Metrics
5.10.
Proving Termination
5.11.
Lexicographic Termination
5.12.
How About Data Types?
5.13.
User specified metrics on Data Types
5.14.
Termination Can be Tricky
5.15.
Avoiding Infinite Loops
5.16.
Avoiding Infinite Loops
5.17.
Avoiding Infinite Loops
5.18.
Avoiding Infinite Loops
5.19.
Avoiding Infinite Loops is Easy (in Practice)
5.20.
Avoiding Infinite Loops is Easy (in Practice)
5.21.
Avoiding Infinite Loops is Easy (in Practice)
5.22.
Avoiding Infinite Loops is Easy (in Practice)
5.23.
Outline
5.24.
Outline
6.
Types as Theorems, Programs as Proofs
6.1.
Types As Theorems
6.2.
Types as Theorems: Example
6.3.
Programs As Proofs: Example
6.4.
Types As Theorems
6.5.
Types as Theorems: Example
6.6.
Programs As Proofs: Example
6.7.
Types as Theorems, Programs as Proofs
6.8.
Those Proofs were Boring
6.9.
Those Proofs were Boring
6.10.
Theorems about Functions
6.11.
Refinement Reflection
6.12.
Reflect Function into Output Type
6.13.
Reflect Function into Output Type
6.14.
Reflection at Result Type
6.15.
Structuring Proofs as Calculations
6.16.
Types as Theorems, Programs as Proofs
6.17.
Reusing Proofs: Functions as Lemmas
6.18.
Reusing Proofs: Functions as Lemmas
6.19.
Reusing Proofs: Functions as Lemmas
6.20.
Types as Theorems, Programs as Proofs
6.21.
Types as Theorems, Programs as Proofs
6.22.
Proof by Logical Evaluation
6.23.
Proof by Logical Evaluation
6.24.
Proof by Logical Evaluation
6.25.
Proof by Induction
6.26.
Proof by Induction
6.27.
Proof by Induction
6.28.
Types as Theorems, Programs as Proofs
6.29.
Types as Theorems, Programs as Proofs
6.30.
Types as Theorems, Programs as Proofs
6.31.
Theorems about Data
6.32.
Theorems about Data: Associativity of
append
6.33.
Case Study: MapReduce
6.34.
Case Study: MapReduce
6.35.
Reduce Theorem
6.36.
Types as Theorems, Programs as Proofs
6.37.
Outline
6.38.
Outline
7.
LiquidHaskell
7.1.
LiquidHaskell
7.2.
LiquidHaskell
7.3.
Evaluation
7.4.
Recap: Refinement Types
7.5.
Recap: Refinement Types
7.6.
Recap: Refinement Types
7.7.
Recap: Refinement Types
7.8.
Many Friends, Many Directions
7.9.
Thank You!