Verification with Refinement Types

Ranjit Jhala

UC San Diego & AWS/ARG

AWS/ARG

Follow Along at This URL

http://ranjitjhala.github.io/CAV2019-tutorial/01-intro.html

Zoom in to see nav arrows

Program Analysis & Verification

Why limited broader impact and adoption?

Program Analysis & Verification

Why limited broader impact and adoption?

Program Analysis & Verification

Why limited broader impact and adoption?

Programmer's Analysis & Verification

Analysis Influences Program's Design

Analysis Influences Program's Design

Analysis Influences Program's Design

Uber NullAway Sridharan et al.

Analysis Influences Program's Design

Static Analysis at Google Sadowski et al. 2018

Analysis Influences Program's Design

Infer Analysis at Facebook Calcagno et al. 2018

Programmer's Analysis & Verification

Program Influences Analysis' Abilities

Program Influences Analysis' Abilities

Language Integrated Verification (LIVE)

This tutorial: LIVE with Refinement Types

LIVE with Refinement Types

Tutorial Goals

Why and how to use Refinement Types

How to implement Refinement Types

Plan

Part I: Refinements 101

Case Study: Vector Bounds

Part II: Properties of Structures

Case Study: Sorting, Interpreter

Part III: Invariants of Data Structures

Case Study: Sorting actually Sorts Lists

Part IV: Termination and Correctness Proofs

Case Study: Optimizing Expressions, Search Trees

Language Integrated Verification