Liquid Types: SMT Solver-based Types

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

Ranjit Jhala, University of California, San Diego, USA

Ranjit Jhala is an Associate Professor in the Department of Computer Science and Engineering at UC San Diego. He is interested in applying techniques from Programming Languages and Software Engineering to solve computing problems, in particular, to build reliable computer systems. His work draws from, combines and contributes to methods the areas of Model Checking, Program Analysis, Type Systems and Automated
Deduction. Presently, he is madly in love with typeclasses.