Liquid Types

We present Logically Qualified Data Types, abbreviated to Liquid Types, a new static verification technique which combines the complementary strengths of automated deduction (SMT solvers), model checking (Predicate Abstraction), and type systems (Hindley-Milner inference). Liquid Types automate static verification of deep invariants by combining local implication checks over simple refinement predicates with global subtyping checks. The former are discharged using SMT solvers, and the latter using standard type-based mechanisms. We have implemented Liquid Types in a tool Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers liquid types for the expressions in the program. To demonstrate the utility of our approach, we describe experiments using Dsolve to statically verify, with minimal annotations, the safety of array accesses on a diverse set of benchmarks, and the key invariants of a variety of data structure libraries including several sorting implementations, AVL trees, red-black trees, finite, balanced binary search maps, and an extensible vector library.

(Joint work with Patrick Rondon and Ming Kawaguchi)