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).