{#asds} ======== Algorithmic Verification ------------------------

**Goal**
Proving program properties *without* writing proofs! 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 ------------

[[continue]](01_SimpleRefinements.lhs.slides.html) Plan ---- + Refinements +

Measures

Higher-Order Functions

Abstract Refinements: Code, Data,...,...