##
Software Verification via Liquid Types

### Ranjit Jhala

We describe Liquid Types, a new static program verification
technique which combines the complementary strengths of automated
deduction (SMT solvers), model checking (Predicate Abstraction),
and type systems (Hindley-Milner inference).
We show how in a high-level functional setting (e.g. Ocaml),
liquid types can be used to statically verify a variety of
invariants like array-bound-safety, sortedness, balancedness,
binary-search-ordering, variable ordering, set-implementation,
heap-implementation, and acyclicity of data structure libraries
for list-sorting, union-find, splay trees, AVL trees, red-black
trees, heaps, associative maps, extensible vectors, and binary
decision diagrams. If time permits, we will briefly describe
how liquid types can be applied to a low-level imperative
setting (e.g. C).