Liquid Types for Array Invariant Synthesis.

Liquid types qualify ordinary Hindley-Milner types by predicates expressing properties. The system infers the types of all the variables and checks that the verification conditions proving correctness hold. These predicates are currently expressed in a quantifier free decidable logic.