\( \require{color} \definecolor{kvcol}{RGB}{203,23,206} \definecolor{tycol}{RGB}{5,177,93} \definecolor{refcol}{RGB}{18,110,213} \newcommand{\quals}{\mathbb{Q}} \newcommand{\defeq}{\ \doteq\ } \newcommand{\subty}{\preceq} \newcommand{\True}{\mathit{True}} \newcommand{\Int}{\mathtt{Int}} \newcommand{\Nat}{\mathtt{Nat}} \newcommand{\Zero}{\mathtt{Zero}} \newcommand{\foo}[4]{{#1}^{#4} + {#2}^{#4} = {#3}^{#4}} \newcommand{\reft}[3]{\{\bindx{#1}{#2} \mid {#3}\}} \newcommand{\ereft}[3]{\bindx{#1}{\{#2 \mid #3\}}} \newcommand{\bindx}[2]{{#1}\!:\!{#2}} \newcommand{\reftx}[2]{\{{#1}\mid{#2}\}} \newcommand{\inferrule}[3][]{\frac{#2}{#3}\;{#1}} \newcommand{\kvar}[1]{\color{kvcol}{\mathbf{\kappa_{#1}}}} \newcommand{\llen}[1]{\mathtt{llen}(#1)} \)

Algorithmic Verification

Goal

Proving program properties without writing proofs!

21: {x2 : (IO ()) | (x2 == Main.main)}main = [Char] -> (IO ())putStrLn {x2 : [Char] | ((len x2) >= 0)}"Easter Egg: to force Makefile"

Algorithmic Verification

Tension

Automation vs. Expressiveness

Tension

Extremes: Hindley-Milner vs. CoC

Tension

Trading off Automation for Expressiveness

Tension

Goal: Find a sweet spot?

Program Logics

Floyd-Hoare (ESC, Dafny, SLAM/BLAST,...)

Properties: Assertions & Pre- and Post-conditions
Proofs: Verification Conditions proved by SMT
Inference: Abstract Interpretation

Automatic but not Expressive

Program Logics

Automatic but not Expressive

Rich Data Types ?
Higher-order functions ?
Polymorphism ?

Liquid Types

Generalize Floyd-Hoare Logic with Types

Properties: Types + Predicates
Proofs: Subtyping + Verification Conditions
Inference: Hindley-Milner + Abstract Interpretation

Towards reconciling Automation and Expressiveness

Liquid Types

Plan